(benchmark thm3_WD
:logic LRM

:extrasorts ((OBJECT 0))
:extrafuns ((root OBJECT))
:extrafuns ((tcl (Set ((ind Tuple 2) OBJECT OBJECT)) (Set ((ind Tuple 2) OBJECT OBJECT))))
:extrafuns ((relImage1 (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 (relImage1 r s)) (exists ((a OBJECT)) (and (in a s) (in ((ind tuple 2) a b) r)))))
:extrafuns ((relConverse3 (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) (relConverse3 f)) (in ((ind tuple 2) a b) f)))
:extrafuns ((pfun2Relation4 (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) (pfun2Relation4 f)) (and (in a (domain f)) (= b (apply f a)))))
:extrafuns ((pfunConverse2 ((x (Map OBJECT OBJECT))) (relConverse3 (pfun2Relation4 x))))
:extrafuns ((joinRelations16 (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) (joinRelations16 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 "∀t·t∈objfn∧(∀s·s⊆t∼[s]⇒s=∅)⇒tcl(t)∩(OBJECT ◁ id)=∅"
:assumption (forall ((t (Map OBJECT OBJECT))) (implies (and (forall ((var0 OBJECT)) (implies (in var0 (domain t)) (not (= var0 root)))) (forall ((s (Set OBJECT))) (implies (subset s (relImage1 (pfunConverse2 t) s)) (= s (as emptySet (Set OBJECT)))))) (forall ((var5 ((ind Tuple 2) OBJECT OBJECT))) (= (and (in var5 (tcl (pfun2Relation4 t))) (= ((ind project 2 1) var5) ((ind project 2 2) var5))) (in var5 (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 (relImage1 r s)) (= s (as emptySet (Set OBJECT)))))) (forall ((t (Set OBJECT))) (implies (subset t (relImage1 r2 t)) (= t (as emptySet (Set OBJECT)))))))

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

:notes "objfn⊆objrel"
: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 (joinRelations16 (joinRelations16 (pfunConverse2 c) (pfun2Relation4 f)) (pfun2Relation4 c)) )) true))

: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 (joinRelations16 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 (joinRelations16 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 "∀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 (joinRelations16 r t)  t)) (subset (tcl r) t)))

:notes "∀f,c,t,u,M,N·N⊆OBJECT∧M⊆OBJECT∧t∈M∧f∈M ∖ {t} → M∧(∀s·s⊆f∼[s]⇒s=∅)∧u∈N∧c∈M ⤖ N⇒t∈dom(c)∧c∈OBJECT ⇸ OBJECT"
:formula (not (forall ((f (Map OBJECT OBJECT))(c (Map OBJECT OBJECT))(t OBJECT)(u OBJECT)(M (Set OBJECT))(N (Set OBJECT))) (implies (and true true (in t M) true (forall ((s (Set OBJECT))) (implies (subset s (relImage1 (pfunConverse2 f) s)) (= s (as emptySet (Set OBJECT))))) (in u N) true) (and (in t (domain c)) true))))

)