:: TREES_3 semantic presentation begin begin definitionfunc :::"Trees"::: -> ($#m1_hidden :::"set"::: ) means :: TREES_3:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::)) ")" )); end; :: deftheorem defines :::"Trees"::: TREES_3:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_3 :::"Trees"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::)) ")" )) ")" )); registration cluster (Set ($#k1_trees_3 :::"Trees"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionfunc :::"FinTrees"::: -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_trees_3 :::"Trees"::: ) ) means :: TREES_3:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) ")" )); end; :: deftheorem defines :::"FinTrees"::: TREES_3:def 2 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_trees_3 :::"Trees"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_3 :::"FinTrees"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b1"))) "iff" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) ")" )) ")" )); registration cluster (Set ($#k2_trees_3 :::"FinTrees"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"constituted-Trees"::: means :: TREES_3:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::))); attr "IT" is :::"constituted-FinTrees"::: means :: TREES_3:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::))); attr "IT" is :::"constituted-DTrees"::: means :: TREES_3:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::))); end; :: deftheorem defines :::"constituted-Trees"::: TREES_3:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::))) ")" )); :: deftheorem defines :::"constituted-FinTrees"::: TREES_3:def 4 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::))) ")" )); :: deftheorem defines :::"constituted-DTrees"::: TREES_3:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::))) ")" )); theorem :: TREES_3:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) "iff" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_trees_3 :::"Trees"::: ) )) ")" )) ; theorem :: TREES_3:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) "iff" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k2_trees_3 :::"FinTrees"::: ) )) ")" )) ; theorem :: TREES_3:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y"))) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) ")" )) ; theorem :: TREES_3:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y"))) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) )) ; theorem :: TREES_3:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) & (Bool (Set (Set (Var "Y")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X"))) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) & (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y"))) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) ")" )) ; theorem :: TREES_3:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y"))) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) ")" )) ; theorem :: TREES_3:7 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y"))) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) )) ; theorem :: TREES_3:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) & (Bool (Set (Set (Var "Y")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X"))) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) & (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y"))) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) ")" )) ; theorem :: TREES_3:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y"))) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) ")" )) ; theorem :: TREES_3:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) & (Bool (Set (Var "Y")) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) )) "holds" (Bool (Set (Set (Var "X")) ($#k5_xboole_0 :::"\+\"::: ) (Set (Var "Y"))) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) )) ; theorem :: TREES_3:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) & (Bool (Set (Set (Var "Y")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X"))) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) & (Bool (Set (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y"))) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) ")" )) ; registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_trees_3 :::"constituted-Trees"::: ) ($#v2_trees_3 :::"constituted-FinTrees"::: ) ($#v3_trees_3 :::"constituted-DTrees"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: TREES_3:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::)) ")" )) ; theorem :: TREES_3:13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) ")" )) ; theorem :: TREES_3:14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::)) ")" )) ; theorem :: TREES_3:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::)) & (Bool (Set (Var "y")) "is" ($#m1_hidden :::"Tree":::)) ")" ) ")" )) ; theorem :: TREES_3:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) & (Bool (Set (Var "y")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) ")" ) ")" )) ; theorem :: TREES_3:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::)) & (Bool (Set (Var "y")) "is" ($#m1_hidden :::"DecoratedTree":::)) ")" ) ")" )) ; theorem :: TREES_3:18 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "Y")) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) )) ; theorem :: TREES_3:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "Y")) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) )) ; theorem :: TREES_3:20 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "Y")) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) )) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_trees_3 :::"constituted-Trees"::: ) ($#v2_trees_3 :::"constituted-FinTrees"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_3 :::"constituted-DTrees"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v2_trees_3 :::"constituted-FinTrees"::: ) -> ($#v1_trees_3 :::"constituted-Trees"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v1_trees_3 :::"constituted-Trees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_trees_3 :::"constituted-Trees"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "X" be ($#v2_trees_3 :::"constituted-FinTrees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_trees_3 :::"constituted-FinTrees"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "X" be ($#v3_trees_3 :::"constituted-DTrees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_trees_3 :::"constituted-DTrees"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) "X"); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_3 :::"constituted-Trees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_trees_3 :::"constituted-FinTrees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; registration cluster ($#v3_trees_3 :::"constituted-DTrees"::: ) -> ($#v4_funct_1 :::"functional"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_trees_3 :::"constituted-DTrees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_trees_2 :::"DecoratedTree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; registration cluster (Set ($#k1_trees_3 :::"Trees"::: ) ) -> ($#v1_trees_3 :::"constituted-Trees"::: ) ; end; registration cluster (Set ($#k2_trees_3 :::"FinTrees"::: ) ) -> ($#v2_trees_3 :::"constituted-FinTrees"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_3 :::"constituted-Trees"::: ) ($#v2_trees_3 :::"constituted-FinTrees"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k1_trees_3 :::"Trees"::: ) )); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode :::"DTree-set"::: "of" "D" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: TREES_3:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it)) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::) "of" "D")); end; :: deftheorem defines :::"DTree-set"::: TREES_3:def 6 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_trees_3 :::"DTree-set"::: ) "of" (Set (Var "D"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")))) ")" )); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_trees_3 :::"constituted-DTrees"::: ) for ($#m1_trees_3 :::"DTree-set"::: ) "of" "D"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_3 :::"constituted-DTrees"::: ) for ($#m1_trees_3 :::"DTree-set"::: ) "of" "D"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set"::: ) "of" (Set (Const "D")); cluster -> "D" ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "E"; end; definitionlet "T" be ($#m1_hidden :::"Tree":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"Funcs"::: redefine func :::"Funcs"::: "(" "T" "," "D" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set"::: ) "of" "D"; end; registrationlet "T" be ($#m1_hidden :::"Tree":::); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v3_trees_2 :::"DecoratedTree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "T" "," "D" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"Trees"::: "D" -> ($#m1_trees_3 :::"DTree-set"::: ) "of" "D" means :: TREES_3:def 7 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" "D" "holds" (Bool (Set (Var "T")) ($#r2_hidden :::"in"::: ) it)); end; :: deftheorem defines :::"Trees"::: TREES_3:def 7 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_trees_3 :::"DTree-set"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_trees_3 :::"Trees"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")) "holds" (Bool (Set (Var "T")) ($#r2_hidden :::"in"::: ) (Set (Var "b2")))) ")" ))); registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_trees_3 :::"Trees"::: ) "D") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"FinTrees"::: "D" -> ($#m1_trees_3 :::"DTree-set"::: ) "of" "D" means :: TREES_3:def 8 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" "D" "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "is" ($#v1_finset_1 :::"finite"::: ) ) "iff" (Bool (Set (Var "T")) ($#r2_hidden :::"in"::: ) it) ")" )); end; :: deftheorem defines :::"FinTrees"::: TREES_3:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_trees_3 :::"DTree-set"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "is" ($#v1_finset_1 :::"finite"::: ) ) "iff" (Bool (Set (Var "T")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) ")" )) ")" ))); theorem :: TREES_3:21 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set (Var "D"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_trees_3 :::"Trees"::: ) (Set (Var "D"))))) ; begin definitionlet "IT" be ($#m1_hidden :::"Function":::); attr "IT" is :::"Tree-yielding"::: means :: TREES_3:def 9 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "IT") "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ); attr "IT" is :::"FinTree-yielding"::: means :: TREES_3:def 10 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "IT") "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ); attr "IT" is :::"DTree-yielding"::: means :: TREES_3:def 11 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "IT") "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ); end; :: deftheorem defines :::"Tree-yielding"::: TREES_3:def 9 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "IT"))) "is" ($#v1_trees_3 :::"constituted-Trees"::: ) ) ")" )); :: deftheorem defines :::"FinTree-yielding"::: TREES_3:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v5_trees_3 :::"FinTree-yielding"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "IT"))) "is" ($#v2_trees_3 :::"constituted-FinTrees"::: ) ) ")" )); :: deftheorem defines :::"DTree-yielding"::: TREES_3:def 11 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "IT"))) "is" ($#v3_trees_3 :::"constituted-DTrees"::: ) ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_xboole_0 :::"empty"::: ) -> ($#v4_trees_3 :::"Tree-yielding"::: ) ($#v5_trees_3 :::"FinTree-yielding"::: ) ($#v6_trees_3 :::"DTree-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: TREES_3:22 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Tree":::))) ")" )) ; theorem :: TREES_3:23 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v5_trees_3 :::"FinTree-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::))) ")" )) ; theorem :: TREES_3:24 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"DecoratedTree":::))) ")" )) ; theorem :: TREES_3:25 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) & (Bool (Set (Var "q")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) ")" )) ; theorem :: TREES_3:26 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) "is" ($#v5_trees_3 :::"FinTree-yielding"::: ) ) & (Bool (Set (Var "q")) "is" ($#v5_trees_3 :::"FinTree-yielding"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v5_trees_3 :::"FinTree-yielding"::: ) ) ")" )) ; theorem :: TREES_3:27 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "p")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) & (Bool (Set (Var "q")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) ")" ) "iff" (Bool (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) ")" )) ; theorem :: TREES_3:28 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::)) ")" )) ; theorem :: TREES_3:29 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v5_trees_3 :::"FinTree-yielding"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) ")" )) ; theorem :: TREES_3:30 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::)) ")" )) ; theorem :: TREES_3:31 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::)) & (Bool (Set (Var "y")) "is" ($#m1_hidden :::"Tree":::)) ")" ) ")" )) ; theorem :: TREES_3:32 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v5_trees_3 :::"FinTree-yielding"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) & (Bool (Set (Var "y")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) ")" ) ")" )) ; theorem :: TREES_3:33 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k10_finseq_1 :::"*>"::: ) ) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::)) & (Bool (Set (Var "y")) "is" ($#m1_hidden :::"DecoratedTree":::)) ")" ) ")" )) ; theorem :: TREES_3:34 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "x"))) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Tree":::)) ")" ))) ; theorem :: TREES_3:35 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "x"))) "is" ($#v5_trees_3 :::"FinTree-yielding"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)) ")" ))) ; theorem :: TREES_3:36 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "x"))) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"DecoratedTree":::)) ")" ))) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v4_trees_3 :::"Tree-yielding"::: ) ($#v5_trees_3 :::"FinTree-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v6_trees_3 :::"DTree-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_trees_3 :::"Tree-yielding"::: ) ($#v5_trees_3 :::"FinTree-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_trees_3 :::"DTree-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v5_trees_3 :::"FinTree-yielding"::: ) -> ($#v4_trees_3 :::"Tree-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_3 :::"constituted-Trees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_trees_3 :::"Tree-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "D"; end; registrationlet "p", "q" be ($#v4_trees_3 :::"Tree-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k7_finseq_1 :::"^"::: ) "q") -> ($#v4_trees_3 :::"Tree-yielding"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_trees_3 :::"constituted-FinTrees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v5_trees_3 :::"FinTree-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "D"; end; registrationlet "p", "q" be ($#v5_trees_3 :::"FinTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k7_finseq_1 :::"^"::: ) "q") -> ($#v5_trees_3 :::"FinTree-yielding"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_trees_3 :::"constituted-DTrees"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v6_trees_3 :::"DTree-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "D"; end; registrationlet "p", "q" be ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "p" ($#k7_finseq_1 :::"^"::: ) "q") -> ($#v6_trees_3 :::"DTree-yielding"::: ) ; end; registrationlet "T" be ($#m1_hidden :::"Tree":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "T" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_trees_3 :::"Tree-yielding"::: ) ; let "S" be ($#m1_hidden :::"Tree":::); cluster (Set ($#k10_finseq_1 :::"<*"::: ) "T" "," "S" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_trees_3 :::"Tree-yielding"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#m1_hidden :::"Tree":::); cluster (Set "n" ($#k2_finseq_2 :::"|->"::: ) "T") -> ($#v4_trees_3 :::"Tree-yielding"::: ) ; end; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "T" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v5_trees_3 :::"FinTree-yielding"::: ) ; let "S" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster (Set ($#k10_finseq_1 :::"<*"::: ) "T" "," "S" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#v5_trees_3 :::"FinTree-yielding"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster (Set "n" ($#k2_finseq_2 :::"|->"::: ) "T") -> ($#v5_trees_3 :::"FinTree-yielding"::: ) ; end; registrationlet "T" be ($#m1_hidden :::"DecoratedTree":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "T" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_trees_3 :::"DTree-yielding"::: ) ; let "S" be ($#m1_hidden :::"DecoratedTree":::); cluster (Set ($#k10_finseq_1 :::"<*"::: ) "T" "," "S" ($#k10_finseq_1 :::"*>"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_trees_3 :::"DTree-yielding"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#m1_hidden :::"DecoratedTree":::); cluster (Set "n" ($#k2_finseq_2 :::"|->"::: ) "T") -> ($#v6_trees_3 :::"DTree-yielding"::: ) ; end; theorem :: TREES_3:37 (Bool "for" (Set (Var "f")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "f"))) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) ")" )) ; registrationlet "p" be ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k2_funct_6 :::"doms"::: ) "p") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v4_trees_3 :::"Tree-yielding"::: ) ; end; theorem :: TREES_3:38 (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) ; begin definitionlet "D", "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; mode DecoratedTree of "D" "," "E" is ($#m1_hidden :::"DecoratedTree":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "D" "," "E" ($#k2_zfmisc_1 :::":]"::: ) ); mode DTree-set of "D" "," "E" is ($#m1_trees_3 :::"DTree-set"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "D" "," "E" ($#k2_zfmisc_1 :::":]"::: ) ); end; registrationlet "T1", "T2" be ($#m1_hidden :::"DecoratedTree":::); cluster (Set ($#k13_funct_3 :::"<:"::: ) "T1" "," "T2" ($#k13_funct_3 :::":>"::: ) ) -> ($#v3_trees_2 :::"DecoratedTree-like"::: ) ; end; registrationlet "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T1" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D1")); let "T2" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D2")); cluster (Set ($#k13_funct_3 :::"<:"::: ) "T1" "," "T2" ($#k13_funct_3 :::":>"::: ) ) -> (Set ($#k2_zfmisc_1 :::"[:"::: ) "D1" "," "D2" ($#k2_zfmisc_1 :::":]"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "D", "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set (Const "E")); cluster (Set "T" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v3_trees_2 :::"DecoratedTree-like"::: ) ; end; definitionlet "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"pr1"::: redefine func :::"pr1"::: "(" "D1" "," "D2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "D1" "," "D2" ($#k2_zfmisc_1 :::":]"::: ) ) "," "D1"; :: original: :::"pr2"::: redefine func :::"pr2"::: "(" "D1" "," "D2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "D1" "," "D2" ($#k2_zfmisc_1 :::":]"::: ) ) "," "D2"; end; definitionlet "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D1")) "," (Set (Const "D2")); func "T" :::"`1"::: -> ($#m1_hidden :::"DecoratedTree":::) "of" "D1" equals :: TREES_3:def 12 (Set (Set "(" ($#k6_trees_3 :::"pr1"::: ) "(" "D1" "," "D2" ")" ")" ) ($#k3_relat_1 :::"*"::: ) "T"); func "T" :::"`2"::: -> ($#m1_hidden :::"DecoratedTree":::) "of" "D2" equals :: TREES_3:def 13 (Set (Set "(" ($#k7_trees_3 :::"pr2"::: ) "(" "D1" "," "D2" ")" ")" ) ($#k3_relat_1 :::"*"::: ) "T"); end; :: deftheorem defines :::"`1"::: TREES_3:def 12 : (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) "holds" (Bool (Set (Set (Var "T")) ($#k8_trees_3 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_trees_3 :::"pr1"::: ) "(" (Set (Var "D1")) "," (Set (Var "D2")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "T")))))); :: deftheorem defines :::"`2"::: TREES_3:def 13 : (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) "holds" (Bool (Set (Set (Var "T")) ($#k9_trees_3 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_trees_3 :::"pr2"::: ) "(" (Set (Var "D1")) "," (Set (Var "D2")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "T")))))); theorem :: TREES_3:39 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "T")) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k2_domain_1 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k8_trees_3 :::"`1"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t")))) & (Bool (Set (Set "(" (Set (Var "T")) ($#k9_trees_3 :::"`2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k3_trees_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k3_domain_1 :::"`2"::: ) )) ")" )))) ; theorem :: TREES_3:40 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) "holds" (Bool (Set ($#k13_funct_3 :::"<:"::: ) (Set "(" (Set (Var "T")) ($#k8_trees_3 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "T")) ($#k9_trees_3 :::"`2"::: ) ")" ) ($#k13_funct_3 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "T"))))) ; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster (Set ($#k3_trees_1 :::"Leaves"::: ) "T") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "T" be ($#m1_hidden :::"Tree":::); let "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "S" -> ($#m1_trees_1 :::"Element"::: ) "of" "T"; end; definitionlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); :: original: :::"Leaf"::: redefine mode :::"Leaf"::: "of" "T" -> ($#m2_trees_3 :::"Element"::: ) "of" (Set ($#k3_trees_1 :::"Leaves"::: ) "T"); end; definitionlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); mode :::"T-Substitution"::: "of" "T" -> ($#m1_hidden :::"Tree":::) means :: TREES_3:def 14 (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" it "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) "T") "or" (Bool "ex" (Set (Var "l")) "being" ($#m3_trees_3 :::"Leaf"::: ) "of" "T" "st" (Bool (Set (Var "l")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t")))) ")" )); end; :: deftheorem defines :::"T-Substitution"::: TREES_3:def 14 : (Bool "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m4_trees_3 :::"T-Substitution"::: ) "of" (Set (Var "T"))) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "b2")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) "or" (Bool "ex" (Set (Var "l")) "being" ($#m3_trees_3 :::"Leaf"::: ) "of" (Set (Var "T")) "st" (Bool (Set (Var "l")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t")))) ")" )) ")" ))); definitionlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); let "t" be ($#m3_trees_3 :::"Leaf"::: ) "of" (Set (Const "T")); let "S" be ($#m1_hidden :::"Tree":::); :: original: :::"with-replacement"::: redefine func "T" :::"with-replacement"::: "(" "t" "," "S" ")" -> ($#m4_trees_3 :::"T-Substitution"::: ) "of" "T"; end; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_trees_1 :::"Tree-like"::: ) for ($#m4_trees_3 :::"T-Substitution"::: ) "of" "T"; end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode T-Substitution of "n" is ($#m4_trees_3 :::"T-Substitution"::: ) "of" (Set ($#k2_trees_1 :::"elementary_tree"::: ) "n"); end; theorem :: TREES_3:41 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Var "T")) "is" ($#m4_trees_3 :::"T-Substitution":::) "of" (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: TREES_3:42 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Set (Var "T1")) ($#k2_trees_2 :::"-level"::: ) (Num 1)) ($#r1_tarski :::"c="::: ) (Set (Set (Var "T2")) ($#k2_trees_2 :::"-level"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T1")))) "holds" (Bool (Set (Set (Var "T1")) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "T2")) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))) ")" )) "holds" (Bool (Set (Var "T1")) ($#r1_tarski :::"c="::: ) (Set (Var "T2")))) ; begin theorem :: TREES_3:43 (Bool "for" (Set (Var "T")) "," (Set (Var "T9")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T"))))) "holds" (Bool (Set (Var "T")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "T")) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T9")) ")" )))) ; theorem :: TREES_3:44 (Bool "for" (Set (Var "T")) "," (Set (Var "T9")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T9")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T9")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: TREES_3:45 (Bool "for" (Set (Var "T")) "," (Set (Var "T9")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) "st" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T9")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "q")))))) ; theorem :: TREES_3:46 (Bool "for" (Set (Var "T")) "," (Set (Var "T9")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) (Bool "for" (Set (Var "q")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T9"))) "holds" (Bool (Set (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T9")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "T9")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))))))) ; registrationlet "T1", "T2" be ($#m1_hidden :::"Tree":::); cluster (Set "T1" ($#k2_xboole_0 :::"\/"::: ) "T2") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) ; end; theorem :: TREES_3:47 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Set (Var "T1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "T2"))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T1"))) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T2")))) "implies" (Bool (Set (Set "(" (Set (Var "T1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "T2")) ")" ) ($#k4_trees_1 :::"|"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T1")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "T2")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p")) ")" ))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T1"))))) "implies" (Bool (Set (Set "(" (Set (Var "T1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "T2")) ")" ) ($#k4_trees_1 :::"|"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T2")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T2"))))) "implies" (Bool (Set (Set "(" (Set (Var "T1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "T2")) ")" ) ($#k4_trees_1 :::"|"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T1")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p")))) ")" ")" ))) ; definitionlet "p" be ($#m1_hidden :::"FinSequence":::); assume (Bool (Set (Const "p")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) ) ; func :::"tree"::: "p" -> ($#m1_hidden :::"Tree":::) means :: TREES_3:def 15 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "p")) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"tree"::: TREES_3:def 15 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" ))) ")" ) ")" )) ")" ))); definitionlet "T" be ($#m1_hidden :::"Tree":::); func :::"^"::: "T" -> ($#m1_hidden :::"Tree":::) equals :: TREES_3:def 16 (Set ($#k11_trees_3 :::"tree"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) "T" ($#k9_finseq_1 :::"*>"::: ) )); end; :: deftheorem defines :::"^"::: TREES_3:def 16 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "T")) ($#k9_finseq_1 :::"*>"::: ) )))); definitionlet "T1", "T2" be ($#m1_hidden :::"Tree":::); func :::"tree"::: "(" "T1" "," "T2" ")" -> ($#m1_hidden :::"Tree":::) equals :: TREES_3:def 17 (Set ($#k11_trees_3 :::"tree"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "T1" "," "T2" ($#k10_finseq_1 :::"*>"::: ) )); end; :: deftheorem defines :::"tree"::: TREES_3:def 17 : (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k10_finseq_1 :::"*>"::: ) )))); theorem :: TREES_3:48 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) )) "holds" (Bool "(" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ))) ; theorem :: TREES_3:49 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "p")) ")" ) ($#k2_trees_2 :::"-level"::: ) (Num 1)) ($#r1_hidden :::"="::: ) "{" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) where n "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) "}" ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "p")) ")" ) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" )) ; theorem :: TREES_3:50 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v4_trees_3 :::"Tree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k11_trees_3 :::"tree"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: TREES_3:51 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#v4_trees_3 :::"Tree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) "iff" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p1")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" (Set "(" (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "T")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2")) ")" ))) ")" )))) ; theorem :: TREES_3:52 (Bool (Set ($#k11_trees_3 :::"tree"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: TREES_3:53 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v4_trees_3 :::"Tree-yielding"::: ) )) "holds" (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set (Var "p"))))) ; theorem :: TREES_3:54 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" (Set (Var "i")) ($#k2_finseq_2 :::"|->"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" )))) ; theorem :: TREES_3:55 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#v4_trees_3 :::"Tree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "T")) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T")) ")" )))) ; theorem :: TREES_3:56 (Bool "for" (Set (Var "p")) "being" ($#v4_trees_3 :::"Tree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k9_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "p")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))) ; theorem :: TREES_3:57 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v4_trees_3 :::"Tree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "T1")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "T2")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T1")) ")" )))) ; theorem :: TREES_3:58 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Num 1) ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T")) ")" ))) ; theorem :: TREES_3:59 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Num 2) ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T1")) ")" ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T2")) ")" ))) ; registrationlet "p" be ($#v5_trees_3 :::"FinTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k11_trees_3 :::"tree"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster (Set ($#k12_trees_3 :::"^"::: ) "T") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "T1", "T2" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster (Set ($#k13_trees_3 :::"tree"::: ) "(" "T1" "," "T2" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: TREES_3:60 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")))) ")" )) ")" ) ")" ))) ; theorem :: TREES_3:61 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) "iff" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T")))) ")" ))) ; theorem :: TREES_3:62 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Num 1)) ($#r1_tarski :::"c="::: ) (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T"))))) ; theorem :: TREES_3:63 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "T1")) ($#r1_tarski :::"c="::: ) (Set (Var "T2")))) "holds" (Bool (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T1"))) ($#r1_tarski :::"c="::: ) (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T2"))))) ; theorem :: TREES_3:64 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T1"))) ($#r1_hidden :::"="::: ) (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T2"))))) "holds" (Bool (Set (Var "T1")) ($#r1_hidden :::"="::: ) (Set (Var "T2")))) ; theorem :: TREES_3:65 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set "(" ($#k12_trees_3 :::"^"::: ) (Set (Var "T")) ")" ) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "T")))) ; theorem :: TREES_3:66 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set "(" ($#k12_trees_3 :::"^"::: ) (Set (Var "T1")) ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_trees_3 :::"^"::: ) (Set (Var "T2"))))) ; theorem :: TREES_3:67 (Bool (Set ($#k12_trees_3 :::"^"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Num 1))) ; theorem :: TREES_3:68 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" )) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "ex" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T1"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")))) ")" ) "or" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T2"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p")))) ")" ) ")" )) ")" ) ")" ))) ; theorem :: TREES_3:69 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T1"))) "iff" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" )) ")" ))) ; theorem :: TREES_3:70 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T2"))) "iff" (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" )) ")" ))) ; theorem :: TREES_3:71 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Num 2)) ($#r1_tarski :::"c="::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ))) ; theorem :: TREES_3:72 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "T1")) ($#r1_tarski :::"c="::: ) (Set (Var "W1"))) & (Bool (Set (Var "T2")) ($#r1_tarski :::"c="::: ) (Set (Var "W2")))) "holds" (Bool (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ))) ; theorem :: TREES_3:73 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "W1")) "," (Set (Var "W2")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "W1")) "," (Set (Var "W2")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "T1")) ($#r1_hidden :::"="::: ) (Set (Var "W1"))) & (Bool (Set (Var "T2")) ($#r1_hidden :::"="::: ) (Set (Var "W2"))) ")" )) ; theorem :: TREES_3:74 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" ) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "T1"))) & (Bool (Set (Set "(" ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" ) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "T2"))) ")" )) ; theorem :: TREES_3:75 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T")) "," (Set (Var "T2")) ")" )) & (Bool (Set (Set "(" ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T")) ")" )) ")" )) ; theorem :: TREES_3:76 (Bool (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "," (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Num 2))) ; theorem :: TREES_3:77 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "w")) "being" ($#v5_trees_3 :::"FinTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "w"))))) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "t"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "w")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: TREES_3:78 (Bool "for" (Set (Var "w")) "being" ($#v5_trees_3 :::"FinTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "t")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "w"))))) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "w")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "t")))))) ; theorem :: TREES_3:79 (Bool "for" (Set (Var "w")) "being" ($#v5_trees_3 :::"FinTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "t")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "w")))) & (Bool "(" "for" (Set (Var "t9")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "t9")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "w"))))) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "t9"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "t")))) ")" )) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "w")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_trees_1 :::"height"::: ) (Set (Var "t")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ; theorem :: TREES_3:80 (Bool "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k12_trees_3 :::"^"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_trees_1 :::"height"::: ) (Set (Var "T")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) ; theorem :: TREES_3:81 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k13_trees_3 :::"tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k6_trees_1 :::"height"::: ) (Set (Var "T1")) ")" ) "," (Set "(" ($#k6_trees_1 :::"height"::: ) (Set (Var "T2")) ")" ) ")" ")" ) ($#k1_nat_1 :::"+"::: ) (Num 1)))) ; begin registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "t" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set (Const "D"))); cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "t") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "p" be ($#m1_hidden :::"FinSequence":::); assume (Bool (Set (Const "p")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) ; func :::"roots"::: "p" -> ($#m1_hidden :::"FinSequence":::) means :: TREES_3:def 18 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "p"))) "holds" (Bool "ex" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"roots"::: TREES_3:def 18 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) )) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_trees_3 :::"roots"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" )) ")" ) ")" ) ")" )));