:: TREES_4 semantic presentation begin definitionlet "T" be ($#m1_hidden :::"DecoratedTree":::); mode Node of "T" is ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) "T"); end; definitionlet "T1", "T2" be ($#m1_hidden :::"DecoratedTree":::); redefine pred "T1" :::"="::: "T2" means :: TREES_4:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) "T1") ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "T2")) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" "T1" "holds" (Bool (Set "T1" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set "T2" ($#k1_funct_1 :::"."::: ) (Set (Var "p")))) ")" ) ")" ); end; :: deftheorem defines :::"="::: TREES_4:def 1 : (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool "(" (Bool (Set (Var "T1")) ($#r1_hidden :::"="::: ) (Set (Var "T2"))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T2")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "T1")) "holds" (Bool (Set (Set (Var "T1")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T2")) ($#k1_funct_1 :::"."::: ) (Set (Var "p")))) ")" ) ")" ) ")" )); theorem :: TREES_4:1 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "i"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "j"))))) "holds" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j")))) ; theorem :: TREES_4:2 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "j"))))) "holds" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "j")))) ; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; func :::"root-tree"::: "x" -> ($#m1_hidden :::"DecoratedTree":::) equals :: TREES_4:def 2 (Set (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k7_funcop_1 :::"-->"::: ) "x"); end; :: deftheorem defines :::"root-tree"::: TREES_4:def 2 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x"))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"root-tree"::: redefine func :::"root-tree"::: "d" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) "D"); end; theorem :: TREES_4:3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) ; theorem :: TREES_4:4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: TREES_4:5 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "holds" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set "(" (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" )))) ; theorem :: TREES_4:6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); func "x" :::"-flat_tree"::: "p" -> ($#m1_hidden :::"DecoratedTree":::) means :: TREES_4:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) "p" ")" ))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) "x") & (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"::: ) "p"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-flat_tree"::: TREES_4:def 3 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_trees_4 :::"-flat_tree"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")) ")" ))) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (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 (Var "b3")) ($#k1_funct_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_4:7 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_trees_4 :::"-flat_tree"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_trees_4 :::"-flat_tree"::: ) (Set (Var "q"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))) ; theorem :: TREES_4:8 (Bool "for" (Set (Var "j")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "i")) ")" ) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "j")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: TREES_4:9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_trees_4 :::"-flat_tree"::: ) (Set (Var "p")) ")" ) ($#k5_trees_2 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )))))) ; definitionlet "x" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_hidden :::"FinSequence":::); assume (Bool (Set (Const "p")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) ) ; func "x" :::"-tree"::: "p" -> ($#m1_hidden :::"DecoratedTree":::) means :: TREES_4:def 4 (Bool "(" (Bool "ex" (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool "p" ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "q")) ")" ))) ")" )) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) "x") & (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"::: ) "p"))) "holds" (Bool (Set it ($#k5_trees_2 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-tree"::: TREES_4:def 4 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (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 "b3")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool "ex" (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "q")) ")" ))) ")" )) & (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (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 (Var "b3")) ($#k5_trees_2 :::"|"::: ) (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) ")" ))) ")" ) ")" ) ")" )))); definitionlet "x" be ($#m1_hidden :::"set"::: ) ; let "T" be ($#m1_hidden :::"DecoratedTree":::); func "x" :::"-tree"::: "T" -> ($#m1_hidden :::"DecoratedTree":::) equals :: TREES_4:def 5 (Set "x" ($#k4_trees_4 :::"-tree"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) "T" ($#k9_finseq_1 :::"*>"::: ) )); end; :: deftheorem defines :::"-tree"::: TREES_4:def 5 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool (Set (Set (Var "x")) ($#k5_trees_4 :::"-tree"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "T")) ($#k9_finseq_1 :::"*>"::: ) ))))); definitionlet "x" be ($#m1_hidden :::"set"::: ) ; let "T1", "T2" be ($#m1_hidden :::"DecoratedTree":::); func "x" :::"-tree"::: "(" "T1" "," "T2" ")" -> ($#m1_hidden :::"DecoratedTree":::) equals :: TREES_4:def 6 (Set "x" ($#k4_trees_4 :::"-tree"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) "T1" "," "T2" ($#k10_finseq_1 :::"*>"::: ) )); end; :: deftheorem defines :::"-tree"::: TREES_4:def 6 : (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool (Set (Set (Var "x")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "T1")) "," (Set (Var "T2")) ($#k10_finseq_1 :::"*>"::: ) ))))); theorem :: TREES_4:10 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "p")) ")" ))))) ; theorem :: TREES_4:11 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::)(Bool "ex" (Set (Var "q")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")))) ")" )))) ")" ) ")" ))) ; theorem :: TREES_4:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "q")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))))))))) ; theorem :: TREES_4:13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k5_trees_4 :::"-tree"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k12_trees_3 :::"^"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ))))) ; theorem :: TREES_4:14 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k13_trees_3 :::"tree"::: ) "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T1")) ")" ) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T2")) ")" ) ")" )))) ; theorem :: TREES_4:15 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "q"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) ")" ))) ; theorem :: TREES_4:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k3_trees_4 :::"-flat_tree"::: ) (Set (Var "p"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: TREES_4:17 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")))) & (Bool (Set (Var "p")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; theorem :: TREES_4:18 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "x")) ($#k3_trees_4 :::"-flat_tree"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "q")))) & (Bool (Set (Var "q")) "is" ($#v6_trees_3 :::"DTree-yielding"::: ) )) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))) ; theorem :: TREES_4:19 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_funct_6 :::".."::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "q")) ")" )))))) ; theorem :: TREES_4:20 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k3_trees_4 :::"-flat_tree"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x")))) & (Bool (Set (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x")))) ")" )) ; theorem :: TREES_4:21 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k3_trees_4 :::"-flat_tree"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Num 1) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "y")) ")" ) ")" ))) ; theorem :: TREES_4:22 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool (Set (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "T")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Num 1) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "T")) ")" )))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); cluster (Set "d" ($#k3_trees_4 :::"-flat_tree"::: ) "p") -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set"::: ) "of" (Set (Const "D")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "F")); cluster (Set "d" ($#k4_trees_4 :::"-tree"::: ) "p") -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "T" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); cluster (Set "d" ($#k5_trees_4 :::"-tree"::: ) "T") -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "T1", "T2" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); cluster (Set "d" ($#k6_trees_4 :::"-tree"::: ) "(" "T1" "," "T2" ")" ) -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set (Const "D"))); :: original: :::"doms"::: redefine func :::"doms"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k2_trees_3 :::"FinTrees"::: ) ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set (Const "D"))); :: original: :::"-tree"::: redefine func "d" :::"-tree"::: "p" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) "D"); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); :: original: :::"FinSequence"::: redefine mode :::"FinSequence"::: "of" "x" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "D"; end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_trees_3 :::"constituted-DTrees"::: ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); cluster -> ($#v6_trees_3 :::"DTree-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "X"; end; begin scheme :: TREES_4:sch 1 ExpandTree{ F1() -> ($#m1_hidden :::"Tree":::), F2() -> ($#m1_hidden :::"Tree":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) "or" (Bool "ex" (Set (Var "q")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set F1 "(" ")" )(Bool "ex" (Set (Var "r")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool P1[(Set (Var "q"))]) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) ")" ))) ")" ) ")" ))) proof end; definitionlet "T", "T9" be ($#m1_hidden :::"DecoratedTree":::); let "x" be ($#m1_hidden :::"set"::: ) ; func "(" "T" "," "x" ")" :::"<-"::: "T9" -> ($#m1_hidden :::"DecoratedTree":::) means :: TREES_4:def 7 (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it)) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "T")) "or" (Bool "ex" (Set (Var "q")) "being" ($#m1_trees_1 :::"Node":::) "of" "T"(Bool "ex" (Set (Var "r")) "being" ($#m1_trees_1 :::"Node":::) "of" "T9" "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "T" ")" ))) & (Bool (Set "T" ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) "x") & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) ")" ))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" "T" "st" (Bool (Bool "(" "not" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "T" ")" ))) "or" (Bool (Set "T" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) "x") ")" )) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set "T" ($#k1_funct_1 :::"."::: ) (Set (Var "p")))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" "T" (Bool "for" (Set (Var "q")) "being" ($#m1_trees_1 :::"Node":::) "of" "T9" "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "T" ")" ))) & (Bool (Set "T" ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) "x")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set "T9" ($#k1_funct_1 :::"."::: ) (Set (Var "q"))))) ")" ) ")" ); end; :: deftheorem defines :::"<-"::: TREES_4:def 7 : (Bool "for" (Set (Var "T")) "," (Set (Var "T9")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"DecoratedTree":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "T")) "," (Set (Var "x")) ")" ($#k9_trees_4 :::"<-"::: ) (Set (Var "T9")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4")))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")))) "or" (Bool "ex" (Set (Var "q")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "T"))(Bool "ex" (Set (Var "r")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "T9")) "st" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ))) & (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) ")" ))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "T")) "st" (Bool (Bool "(" "not" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ))) "or" (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"<>"::: ) (Set (Var "x"))) ")" )) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "p")))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "q")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "T9")) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")) ")" ))) & (Bool (Set (Set (Var "T")) ($#k1_funct_1 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool (Set (Set (Var "b4")) ($#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 "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "T", "T9" be ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "T" "," "x" ")" ($#k9_trees_4 :::"<-"::: ) "T9") -> "D" ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: TREES_4:23 (Bool "for" (Set (Var "T")) "," (Set (Var "T9")) "being" ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "T")))) "or" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_trees_2 :::"Leaves"::: ) (Set (Var "T")))) ")" )) "holds" (Bool (Set "(" (Set (Var "T")) "," (Set (Var "x")) ")" ($#k9_trees_4 :::"<-"::: ) (Set (Var "T9"))) ($#r1_hidden :::"="::: ) (Set (Var "T"))))) ; begin theorem :: TREES_4:24 (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 "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k8_trees_3 :::"`1"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "T")) ($#k9_trees_3 :::"`2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "T")))) ")" ))) ; theorem :: TREES_4:25 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) (Bool "for" (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D2")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k8_trees_3 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "d1")))) & (Bool (Set (Set "(" ($#k2_trees_4 :::"root-tree"::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) ")" ) ($#k9_trees_3 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_4 :::"root-tree"::: ) (Set (Var "d2")))) ")" )))) ; theorem :: TREES_4:26 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_funct_3 :::"<:"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "y")) ")" ) ($#k13_funct_3 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )))) ; theorem :: TREES_4:27 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) (Bool "for" (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D2")) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) (Bool "for" (Set (Var "F1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set"::: ) "of" (Set (Var "D1")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "p1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "F1")) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k8_trees_3 :::"`1"::: ) ))) ")" )) "holds" (Bool (Set (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k8_trees_3 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p1"))))))))))) ; theorem :: TREES_4:28 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) (Bool "for" (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D2")) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) (Bool "for" (Set (Var "F2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set"::: ) "of" (Set (Var "D2")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "F")) (Bool "for" (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "F2")) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k9_trees_3 :::"`2"::: ) ))) ")" )) "holds" (Bool (Set (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k9_trees_3 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d2")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p2"))))))))))) ; theorem :: TREES_4:29 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) (Bool "for" (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D2")) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "F")) (Bool "ex" (Set (Var "p1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_trees_3 :::"Trees"::: ) (Set (Var "D1"))) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "F")) "st" (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k8_trees_3 :::"`1"::: ) )) ")" )) ")" ) & (Bool (Set (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k8_trees_3 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p1")))) ")" ))))))) ; theorem :: TREES_4:30 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) (Bool "for" (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D2")) (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_trees_3 :::"DTree-set":::) "of" (Set (Var "D1")) "," (Set (Var "D2")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "F")) (Bool "ex" (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_trees_3 :::"Trees"::: ) (Set (Var "D2"))) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "F")) "st" (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k9_trees_3 :::"`2"::: ) )) ")" )) ")" ) & (Bool (Set (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k9_trees_3 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d2")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p2")))) ")" ))))))) ; theorem :: TREES_4:31 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) (Bool "for" (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D2")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k2_zfmisc_1 :::":]"::: ) )) (Bool "ex" (Set (Var "p1")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set (Var "D1"))) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k2_zfmisc_1 :::":]"::: ) )) "st" (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "p1")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k8_trees_3 :::"`1"::: ) )) ")" )) ")" ) & (Bool (Set (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k8_trees_3 :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d1")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p1")))) ")" )))))) ; theorem :: TREES_4:32 (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D1")) (Bool "for" (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D2")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k2_zfmisc_1 :::":]"::: ) )) (Bool "ex" (Set (Var "p2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set (Var "D2"))) "st" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_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 ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "T")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D1")) "," (Set (Var "D2")) ($#k2_zfmisc_1 :::":]"::: ) )) "st" (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "p2")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k9_trees_3 :::"`2"::: ) )) ")" )) ")" ) & (Bool (Set (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "d1")) "," (Set (Var "d2")) ($#k1_domain_1 :::"]"::: ) ) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p")) ")" ) ($#k9_trees_3 :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "d2")) ($#k8_trees_4 :::"-tree"::: ) (Set (Var "p2")))) ")" )))))) ;