(benchmark INITIALISATION_inv3_INV
:logic LRM

:extrasorts ((NAME 0))
:extrasorts ((DATA 0))
:extrasorts ((OBJECT 0))
:extrafuns ((root OBJECT))
:extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT))))
:extrafuns ((|opened_files'| (Set OBJECT)))
:extrafuns ((|fcontent'| (Set ((ind Tuple 2) OBJECT (Set ((ind Tuple 2) Int DATA))))))
:extrafuns ((|directories'| (Set OBJECT)))
:extrafuns ((|fbuffer'| (Set ((ind Tuple 2) OBJECT (Set ((ind Tuple 2) Int DATA))))))
:extrafuns ((|parent'| (Set ((ind Tuple 2) OBJECT OBJECT))))
:extrafuns ((|files'| (Set OBJECT)))
:extrafuns ((rname NAME))
: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 ((joinRelations17 (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) (joinRelations17 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2)))))

: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 "CONTENT=ℕ ⇸ DATA"
:assumption true

: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 "∅∈CONTENT"
:assumption (forall ((var8 Int) (var9 DATA) (var10 DATA)) (implies (and (in ((ind tuple 2) var8 var9) (as emptySet (Set ((ind Tuple 2) Int DATA)))) (in ((ind tuple 2) var8 var10) (as emptySet (Set ((ind Tuple 2) Int DATA))))) (and (= var9 var10) (>= var8 0))))

: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) (joinRelations17 (joinRelations17 (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 (joinRelations17 (joinRelations17 (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 (joinRelations17 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 (joinRelations17 r (tcl r)) ))))

:notes "rname∈NAME"
:assumption true

: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 (joinRelations17 r t)  t)) (subset (tcl r) t)))

:notes "∅∈∅ → CONTENT"
:formula (not false)

)