(benchmark INITIALISATION_inv1_INV :logic LRM :extrasorts ((OBJECT 0)) :extrafuns ((root OBJECT)) :extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((|parent'| (Set ((ind Tuple 2) OBJECT OBJECT)))) :extrafuns ((|files'| (Set OBJECT))) :extrafuns ((|objects'| (Set OBJECT))) :extrafuns ((|directories'| (Set OBJECT))) :extrafuns ((relImage2 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set OBJECT) (Set OBJECT))) :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT))) (s (Set OBJECT)) (b OBJECT)) (= (in b (relImage2 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r))))) :extrafuns ((relConverse4 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :assumption (forall ((f (Set ((ind Tuple 2) OBJECT OBJECT))) (a OBJECT) (b OBJECT)) (= (in ((ind tuple 2) b a) (relConverse4 f)) (in ((ind tuple 2) a b) f))) :extrafuns ((pfun2Relation5 (Map OBJECT OBJECT) (Set ((ind Tuple 2) OBJECT OBJECT)))) :assumption (forall ((f (Map OBJECT OBJECT)) (a OBJECT) (b OBJECT)) (= (in ((ind tuple 2) a b) (pfun2Relation5 f)) (and (in a (domain f)) (= b (apply f a))))) :extrafuns ((pfunConverse3 ((x (Map OBJECT OBJECT))) (relConverse4 (pfun2Relation5 x)))) :extrafuns ((joinRelations14 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT)))) :assumption (forall ((r1 (Set ((ind Tuple 2) OBJECT OBJECT))) (r2 (Set ((ind Tuple 2) OBJECT OBJECT))) (a OBJECT) (c OBJECT)) (= (in ((ind tuple 2) a c) (joinRelations14 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2))))) :extrafuns ((relRange36 (Set ((ind Tuple 2) OBJECT OBJECT)) (Set OBJECT))) :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT))) (b OBJECT)) (= (in b (relRange36 r)) (exists ((a OBJECT)) (in ((ind tuple 2) a b) r)))) :notes "objfn=OBJECT ∖ {root} ⇸ OBJECT" :assumption true :notes "∀f,g,t,u,x,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧g∈N ∖ {u} → N∧x∈M∧(∀A·A⊆f∼[A]⇒A=∅)∧(∀B·B⊆g∼[B]⇒B=∅)∧f∪g∪{u ↦ x}∈(M∪N) ∖ {t} → M∪N⇒(∀C·C⊆(f∪g∪{u ↦ x})∼[C]⇒C=∅)" :assumption (forall ((f (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(x OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (in x M) (forall ((A (Set OBJECT))) (implies (subset A (relImage2 (pfunConverse3 f) A)) (= A (as emptySet (Set OBJECT))))) (forall ((B (Set OBJECT))) (implies (subset B (relImage2 (pfunConverse3 g) B)) (= B (as emptySet (Set OBJECT))))) false) (forall ((C (Set OBJECT))) (implies (subset C (relImage2 (relConverse4 (union (pfun2Relation5 f) (pfun2Relation5 g) (insert ((ind tuple 2) u x) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))) C)) (= C (as emptySet (Set OBJECT))))))) :notes "∀t·t∈objfn∧(∀s·s⊆t∼[s]⇒s=∅)⇒tcl(t)∩(OBJECT ◁ id)=∅" :assumption (forall ((t (Map OBJECT OBJECT))) (implies (and (forall ((var6 OBJECT)) (implies (in var6 (domain t)) (not (= var6 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var7 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var7 (tcl (pfun2Relation5 t))) (= ((ind project 2 1) var7) ((ind project 2 2) var7))) (in var7 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))))))) :notes "∀r,r2·r∈objrel∧r2∈objrel∧r2⊆r∧(∀s·s⊆r[s]⇒s=∅)⇒(∀t·t⊆r2[t]⇒t=∅)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))(r2 (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies (and true true (subset r2 r) (forall ((s (Set OBJECT))) (implies (subset s (relImage2 r s)) (= s (as emptySet (Set OBJECT)))))) (forall ((t (Set OBJECT))) (implies (subset t (relImage2 r2 t)) (= t (as emptySet (Set OBJECT))))))) :notes "objrel=OBJECT ↔ OBJECT" :assumption true :notes "∀f,c,g,t,u,M,N·N⊆OBJECT∧M⊆OBJECT∧t∈M∧f∈M ∖ {t} → M∧(∀s·s⊆f∼[s]⇒s=∅)∧u∈N∧c∈M ⤖ N∧u=c(t)∧g=c∼;f;c∧g∈N ∖ {u} → N⇒(∀w·w⊆g∼[w]⇒w=∅)" :assumption (forall ((f (Map OBJECT OBJECT))(c (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (in t M) false (forall ((s (Set OBJECT))) (implies (subset s (relImage2 (pfunConverse3 f) s)) (= s (as emptySet (Set OBJECT))))) (in u N) false (= u (apply c t)) (= (pfun2Relation5 g) (joinRelations14 (joinRelations14 (pfunConverse3 c) (pfun2Relation5 f)) (pfun2Relation5 c)) ) false) (forall ((w (Set OBJECT))) (implies (subset w (relImage2 (pfunConverse3 g) w)) (= w (as emptySet (Set OBJECT))))))) :notes "objfn⊆objrel" :assumption true :notes "root∈OBJECT" :assumption true :notes "∀f,g,c,t,u,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧c∈M ⤖ N∧u=c(t)∧g=c∼;f;c⇒g∈N ∖ {u} → N" :assumption (forall ((f (Map OBJECT OBJECT))(g (Set ((ind Tuple 2) OBJECT OBJECT)))(c (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (= u (apply c t)) (= g (joinRelations14 (joinRelations14 (pfunConverse3 c) (pfun2Relation5 f)) (pfun2Relation5 c)) )) true)) :notes "∀r·r∈objrel⇒r;tcl(r)⊆tcl(r)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset (joinRelations14 r (tcl r)) (tcl r)))) :notes "tcl(∅)=∅" :assumption (= (tcl (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) :notes "∀r·r∈objrel⇒tcl(r)=r∪(r;tcl(r))" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (= (tcl r) (union r (joinRelations14 r (tcl r)) )))) :notes "tcl∈objrel → objrel" :assumption true :notes "⊤" :assumption true :notes "∀r·r∈objrel⇒r⊆tcl(r)" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset r (tcl r)))) :notes "∀f,g,t,u,x,M,N·N⊆OBJECT∧M⊆OBJECT∧N∩M=∅∧t∈M∧f∈M ∖ {t} → M∧u∈N∧g∈N ∖ {u} → N∧x∈M⇒f∪g∪{u ↦ x}∈(M∪N) ∖ {t} → M∪N" :assumption (forall ((f (Map OBJECT OBJECT))(g (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(x OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (= (inter N M) (as emptySet (Set OBJECT))) (in t M) false (in u N) false (in x M)) true)) :notes "∀r,t·r∈objrel∧r⊆t∧r;t⊆t⇒tcl(r)⊆t" :assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))(t (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies (and true (subset r t) (subset (joinRelations14 r t) t)) (subset (tcl r) t))) :notes "ran(∅)⊆{root}" :formula (not (subset (relRange36(as emptySet (Set ((ind Tuple 2) OBJECT OBJECT)))) (insert root (as emptySet (Set OBJECT))))) )