(benchmark thm2_THM
:logic LRM

:extrasorts ((OBJECT 0))
:extrafuns ((root OBJECT))
:extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT))))
:extrafuns ((joinRelations2 (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) (joinRelations2 r1 r2)) (exists ((b OBJECT)) (and (in ((ind tuple 2) a b) r1) (in ((ind tuple 2) b c) r2)))))
:extrafuns ((relImage9 (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 (relImage9 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r)))))
:extrafuns ((relConverse11 (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) (relConverse11 f)) (in ((ind tuple 2) a b) f)))
:extrafuns ((pfun2Relation12 (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) (pfun2Relation12 f)) (and (in a (domain f)) (= b (apply f a)))))
:extrafuns ((pfunConverse10 ((x (Map OBJECT OBJECT))) (relConverse11 (pfun2Relation12 x))))

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

:notes "objfn=OBJECT ∖ {root} ⇸ OBJECT"
:assumption true

:notes "tcl∈objrel → objrel"
:assumption true

:notes "⊤"
:assumption true

:notes "∀t·t∈objfn∧(∀s·s⊆t∼[s]⇒s=∅)⇒tcl(t)∩(OBJECT ◁ id)=∅"
:assumption (forall ((t (Map OBJECT OBJECT))) (implies (and (forall ((var8 OBJECT)) (implies (in var8 (domain t)) (not (= var8 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage9 (pfunConverse10 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var13 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var13 (tcl (pfun2Relation12 t))) (= ((ind project 2 1) var13) ((ind project 2 2) var13))) (in var13 (as emptySet (Set ((ind Tuple 2) OBJECT OBJECT))))))))

:notes "∀r·r∈objrel⇒r⊆tcl(r)"
:assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset r (tcl r))))

: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 (relImage9 r s)) (= s (as emptySet (Set OBJECT)))))) (forall ((t (Set OBJECT))) (implies (subset t (relImage9 r2 t)) (= t (as emptySet (Set OBJECT)))))))

:notes "objrel=OBJECT ↔ OBJECT"
:assumption true

:notes "objfn⊆objrel"
:assumption 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 (joinRelations2 r t)  t)) (subset (tcl r) t)))

:notes "root∈OBJECT"
:assumption true

:notes "∀r·r∈objrel⇒r;tcl(r)⊆tcl(r)"
:assumption (forall ((r (Set ((ind Tuple 2) OBJECT OBJECT)))) (implies true (subset (joinRelations2 r (tcl r))  (tcl r))))

: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"
:formula (not (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) true (in u N) true (= u (apply c t)) (= g (joinRelations2 (joinRelations2 (pfunConverse10 c) (pfun2Relation12 f)) (pfun2Relation12 c)) )) false)))

)