:: TREES_2  semantic presentation begin  


















































theorem :: TREES_2:1 (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "v1"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "v"))) & (Bool (Set (Var "v2"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "v")))) "holds"  (Bool (Set (Var "v1")) "," (Set (Var "v2"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )) ; 
 
theorem :: TREES_2:2 (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "v1"))  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set (Var "v"))) & (Bool (Set (Var "v2"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "v")))) "holds"  (Bool (Set (Var "v1")) "," (Set (Var "v2"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )) ; 
 
theorem :: TREES_2:3 (Bool  "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "v1")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "v1")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool  "ex" (Set (Var "v2")) "being"   ($#m1_hidden :::"FinSequence":::)(Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "v1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "v2"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "v2")))  ($#r1_hidden :::"="::: )  (Set (Var "k")))  ")" ))))) ; 
 
theorem :: TREES_2:4 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "v")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"  (Bool (Set   ($#k1_trees_1 :::"ProperPrefixes"::: )  (Set  "(" (Set (Var "v"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_trees_1 :::"ProperPrefixes"::: )  (Set (Var "v")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "v")) ($#k1_tarski :::"}"::: ) ))))) ; 
 scheme  :: TREES_2:sch 1 TreeStructInd{ F1() ->   ($#m1_hidden :::"Tree":::), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) "holds"  (Bool P1[(Set (Var "t"))]))
 provided
(Bool P1[(Set   ($#k1_xboole_0 :::"{}"::: )  )])
 and  
(Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool P1[(Set (Var "t"))]) & (Bool (Set (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool P1[(Set (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))])))
 proof 


end; 
theorem :: TREES_2:5 (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"   ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W1"))) "iff" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W2")))  ")" )  ")" )) "holds"  (Bool (Set (Var "W1"))  ($#r1_hidden :::"="::: )  (Set (Var "W2")))) ; 
 definitionlet "W1", "W2" be   ($#m1_hidden :::"Tree":::); redefine pred "W1" :::"="::: "W2" means :: TREES_2:def 1 (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  "W1") "iff" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  "W2")  ")" )); end; 





:: deftheorem    defines :::"="::: TREES_2:def 1 :  (Bool  "for" (Set (Var "W1")) "," (Set (Var "W2")) "being"   ($#m1_hidden :::"Tree":::) "holds"   (Bool  "("  (Bool (Set (Var "W1"))  ($#r1_hidden :::"="::: )  (Set (Var "W2"))) "iff" (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W1"))) "iff" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W2")))  ")" ))  ")" )); 
 
theorem :: TREES_2:6 (Bool  "for" (Set (Var "W")) "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 (Var "W")))) "holds"  (Bool (Set (Var "W"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "W"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set  "(" (Set (Var "W"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "p")) ")" ) ")" )))) ; 
 
theorem :: TREES_2:7 (Bool  "for" (Set (Var "W")) "," (Set (Var "W1")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Bool  "not" (Set (Var "p"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "W"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "W1")) ")" )))) ; 
 
theorem :: TREES_2:8 (Bool  "for" (Set (Var "W")) "," (Set (Var "W1")) "," (Set (Var "W2")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) & (Bool (Bool  "not" (Set (Var "p")) "," (Set (Var "q"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "W"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "W1")) ")"  ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "q")) "," (Set (Var "W2")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "W"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "q")) "," (Set (Var "W2")) ")"  ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "W1")) ")" )))) ; 
 definitionlet "IT" be   ($#m1_hidden :::"Tree":::); attr "IT" is  :::"finite-order":::  means :: TREES_2:def 2 (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" "IT"  "holds" (Bool (Bool  "not" (Set (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  "IT")))); end; 




:: deftheorem    defines :::"finite-order"::: TREES_2:def 2 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"Tree":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_trees_2 :::"finite-order"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "IT"))  "holds" (Bool (Bool  "not" (Set (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))))))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_trees_1 :::"Tree-like"::: )     ($#v1_trees_2 :::"finite-order"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "W" be   ($#m1_hidden :::"Tree":::); mode  :::"Chain":::  "of" "W" ->   ($#m1_subset_1 :::"Subset":::) "of" "W" means :: TREES_2:def 3 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  it) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  it)) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  )); mode  :::"Level":::  "of" "W" ->   ($#m1_subset_1 :::"Subset":::) "of" "W" means :: TREES_2:def 4 (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool it  ($#r1_hidden :::"="::: )   "{"  (Set (Var "w")) where w "is"    ($#m1_trees_1 :::"Element"::: )   "of" "W" : (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  "}"  )); let "w" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Const "W")); func  :::"succ"::: "w" ->   ($#m1_subset_1 :::"Subset":::) "of" "W" equals :: TREES_2:def 5  "{"  (Set  "(" "w"  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) where n "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set "w"  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  "W")  "}"  ; end; 
















:: deftheorem    defines :::"Chain"::: TREES_2:def 3 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W"))) "iff" (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2")))) "holds"  (Bool (Set (Var "p")) "," (Set (Var "q"))  ($#r3_xboole_0 :::"are_c=-comparable"::: )  ))  ")" ))); 
 
:: deftheorem    defines :::"Level"::: TREES_2:def 4 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m2_trees_2 :::"Level"::: )   "of" (Set (Var "W"))) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st" (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "w")) where w "is"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W")) : (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  "}"  ))  ")" ))); 
 
:: deftheorem    defines :::"succ"::: TREES_2:def 5 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W")) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "w"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) where n "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Set (Var "w"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))  "}"  ))); 
 
theorem :: TREES_2:9 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "L")) "being"    ($#m2_trees_2 :::"Level"::: )   "of" (Set (Var "W")) "holds"  (Bool (Set (Var "L")) "is"    ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: )   "of" (Set (Var "W"))))) ; 
 
theorem :: TREES_2:10 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W")) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w"))) "is"    ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: )   "of" (Set (Var "W"))))) ; 
 
theorem :: TREES_2:11 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "A")) "being"    ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: )   "of" (Set (Var "W"))  (Bool  "for" (Set (Var "C")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W")) (Bool  "ex" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W")) "st" (Bool (Set (Set (Var "A"))  ($#k9_subset_1 :::"/\"::: )  (Set (Var "C")))  ($#r1_tarski :::"c="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "w")) ($#k1_tarski :::"}"::: ) )))))) ; 
 definitionlet "W" be   ($#m1_hidden :::"Tree":::); let "n" be   ($#m1_hidden :::"Nat":::); func "W" :::"-level"::: "n" ->    ($#m2_trees_2 :::"Level"::: )   "of" "W" equals :: TREES_2:def 6  "{"  (Set (Var "w")) where w "is"    ($#m1_trees_1 :::"Element"::: )   "of" "W" : (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  "n")  "}"  ; end; 






:: deftheorem    defines :::"-level"::: TREES_2:def 6 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set (Var "W"))  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "w")) where w "is"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W")) : (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  "}"  ))); 
 
theorem :: TREES_2:12 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W"))  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "w"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))) "iff" (Bool (Set (Set (Var "w"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set (Var "W")))  ")" )))) ; 
 
theorem :: TREES_2:13 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "w"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "W"))  ($#k2_trees_2 :::"-level"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))))) ; 
 
theorem :: TREES_2:14 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::) "holds"  (Bool (Set (Var "W"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "(" (Set (Var "W"))  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n")) ")" ) where n "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool verum)  "}"  ))) ; 
 
theorem :: TREES_2:15 (Bool  "for" (Set (Var "W")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::) "holds"  (Bool (Set (Var "W"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "(" (Set (Var "W"))  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n")) ")" ) where n "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_trees_1 :::"height"::: )  (Set (Var "W"))))  "}"  ))) ; 
 
theorem :: TREES_2:16 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "L")) "being"    ($#m2_trees_2 :::"Level"::: )   "of" (Set (Var "W")) (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "L"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "W"))  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n"))))))) ; 
 scheme  :: TREES_2:sch 2 FraenkelCard{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_hidden :::"set"::: )  , F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set   ($#k1_card_1 :::"card"::: )   "{"  (Set F3 "(" (Set (Var "w")) ")" ) where w "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) : (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" ))  "}"  )  ($#r1_ordinal1 :::"c="::: )  (Set   ($#k1_card_1 :::"card"::: )  (Set F2 "("  ")" )))
 proof 


end; scheme  :: TREES_2:sch 3 FraenkelFinCard{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  , F3() ->   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )  , F4(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool (Set   ($#k5_card_1 :::"card"::: )  (Set F3 "("  ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set F2 "("  ")" )))
 provided
(Bool (Set F3 "("  ")" )  ($#r1_hidden :::"="::: )   "{"  (Set F4 "(" (Set (Var "w")) ")" ) where w "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ) : (Bool (Set (Var "w"))  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" ))  "}"  )
 proof 


end; 
theorem :: TREES_2:17 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool (Set (Var "W")) "is"   ($#v1_trees_2 :::"finite-order"::: )  )) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W")) (Bool  "ex" (Set (Var "B")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))) & (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "B")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))  ")" ))))) ; 
 
theorem :: TREES_2:18 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "W")) "is"   ($#v1_trees_2 :::"finite-order"::: )  )) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w"))) "is"   ($#v1_finset_1 :::"finite"::: )  ))) ; 
 registrationlet "W" be   ($#v1_trees_2 :::"finite-order"::: )    ($#m1_hidden :::"Tree":::); let "w" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Const "W")); 
cluster (Set   ($#k1_trees_2 :::"succ"::: )  "w") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: TREES_2:19 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  ) "is"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W")))) ; 
 
theorem :: TREES_2:20 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::) "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W")))) ; 
 registrationlet "W" be   ($#m1_hidden :::"Tree":::); 
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_trees_2 :::"Chain"::: )   "of" "W"; 
end; definitionlet "W" be   ($#m1_hidden :::"Tree":::); let "IT" be    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Const "W")); attr "IT" is  :::"Branch-like":::  means :: TREES_2:def 7 (Bool  "("  (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  "IT")) "holds"  (Bool (Set   ($#k1_trees_1 :::"ProperPrefixes"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  "IT")  ")" ) & (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  "W") "or" (Bool  "ex" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  "IT") & (Bool (Bool  "not" (Set (Var "q"))  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set (Var "p"))))  ")" ))  ")" )  ")" )  ")" ); end; 





:: deftheorem    defines :::"Branch-like"::: TREES_2:def 7 :  (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_trees_2 :::"Branch-like"::: )  ) "iff" (Bool  "("  (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 (Var "IT")))) "holds"  (Bool (Set   ($#k1_trees_1 :::"ProperPrefixes"::: )  (Set (Var "p")))  ($#r1_tarski :::"c="::: )  (Set (Var "IT")))  ")" ) & (Bool  "("   "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "W"))) "or" (Bool  "ex" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "IT"))) & (Bool (Bool  "not" (Set (Var "q"))  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set (Var "p"))))  ")" ))  ")" )  ")" )  ")" )  ")" ))); 
 registrationlet "W" be   ($#m1_hidden :::"Tree":::); 
cluster   ($#v2_trees_2 :::"Branch-like"::: )    for    ($#m1_trees_2 :::"Chain"::: )   "of" "W"; 
end; definitionlet "W" be   ($#m1_hidden :::"Tree":::); mode Branch of "W" is   ($#v2_trees_2 :::"Branch-like"::: )     ($#m1_trees_2 :::"Chain"::: )   "of" "W"; end; registrationlet "W" be   ($#m1_hidden :::"Tree":::); 
cluster   ($#v2_trees_2 :::"Branch-like"::: )    ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_trees_2 :::"Chain"::: )   "of" "W"; 
end; 






theorem :: TREES_2:21 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "v1"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "v2"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Bool  "not" (Set (Var "v1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_trees_1 :::"ProperPrefixes"::: )  (Set (Var "v2")))))) "holds"  (Bool (Set (Var "v2"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "v1")))))) ; 
 
theorem :: TREES_2:22 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "v1")) "," (Set (Var "v2")) "," (Set (Var "v")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "v1"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "v2"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "v"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "v2"))) & (Bool (Bool  "not" (Set (Var "v1"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_trees_1 :::"ProperPrefixes"::: )  (Set (Var "v")))))) "holds"  (Bool (Set (Var "v"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "v1")))))) ; 
 registrationlet "W" be   ($#m1_hidden :::"Tree":::); 
cluster   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_trees_2 :::"Chain"::: )   "of" "W"; 
end; 
theorem :: TREES_2:23 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W"))  "st" (Bool (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_xxreal_0 :::">"::: )  (Set (Var "n")))) "holds"  (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "n")))  ")" ))))) ; 
 
theorem :: TREES_2:24 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W")) "holds"  (Bool  "{"  (Set (Var "w")) where w "is"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "W")) : (Bool  "ex" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "w"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "p")))  ")" ))  "}"   "is"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W"))))) ; 
 
theorem :: TREES_2:25 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "B")) "being"   ($#m1_trees_2 :::"Branch":::) "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "q"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))) "holds"  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "B")))))) ; 
 
theorem :: TREES_2:26 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_trees_2 :::"Branch":::) "of" (Set (Var "W")) "holds"  (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set (Var "B"))))) ; 
 
theorem :: TREES_2:27 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "C")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W"))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "p"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "q")))))) ; 
 
theorem :: TREES_2:28 (Bool  "for" (Set (Var "W")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "W")) (Bool  "ex" (Set (Var "B")) "being"   ($#m1_trees_2 :::"Branch":::) "of" (Set (Var "W")) "st" (Bool (Set (Var "C"))  ($#r1_tarski :::"c="::: )  (Set (Var "B")))))) ; 
 scheme  :: TREES_2:sch 4 FuncExOfMinNat{ P1[   ($#m1_hidden :::"set"::: )   ","   ($#m1_hidden :::"Nat":::)], F1() ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool P1[(Set (Var "x")) "," (Set (Var "n"))]) & (Bool  "("   "for" (Set (Var "m")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool P1[(Set (Var "x")) "," (Set (Var "m"))])) "holds"  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))  ")" )  ")" ))  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "n"))])))
 proof 


end; scheme  :: TREES_2:sch 5 InfiniteChain{ F1() ->    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_hidden :::"set"::: )  , P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_numbers :::"NAT"::: )  )) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set F1 "("  ")" )) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "k")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool P2[(Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))) "," (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))]) & (Bool P1[(Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))])  ")" )  ")" )  ")" ))
 provided
(Bool  "("  (Bool (Set F2 "("  ")" )  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P1[(Set F2 "("  ")" )])  ")" )
 and  
(Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P1[(Set (Var "x"))])) "holds"  (Bool  "ex" (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "st"  (Bool  "("  (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set F1 "("  ")" )) & (Bool P2[(Set (Var "x")) "," (Set (Var "y"))]) & (Bool P1[(Set (Var "y"))])  ")" )))
 proof 


end; 
theorem :: TREES_2:29 (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "T")) "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))  ")" ) & (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "t"))) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )) "holds"  (Bool  "ex" (Set (Var "B")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "T")) "st" (Bool (Bool  "not" (Set (Var "B")) "is"   ($#v1_finset_1 :::"finite"::: )  )))) ; 
 
theorem :: TREES_2:30 (Bool  "for" (Set (Var "T")) "being"   ($#v1_trees_2 :::"finite-order"::: )    ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) (Bool  "ex" (Set (Var "C")) "being"   ($#v1_finset_1 :::"finite"::: )     ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "T")) "st" (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set (Var "C")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool  "ex" (Set (Var "B")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "T")) "st" (Bool (Bool  "not" (Set (Var "B")) "is"   ($#v1_finset_1 :::"finite"::: )  )))) ; 
 definitionlet "IT" be   ($#m1_hidden :::"Relation":::); attr "IT" is  :::"DecoratedTree-like":::  means :: TREES_2:def 8 (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  "IT") "is"   ($#m1_hidden :::"Tree":::)); end; 




:: deftheorem    defines :::"DecoratedTree-like"::: TREES_2:def 8 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_trees_2 :::"DecoratedTree-like"::: )  ) "iff" (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "IT"))) "is"   ($#m1_hidden :::"Tree":::))  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionmode DecoratedTree is   ($#v3_trees_2 :::"DecoratedTree-like"::: )    ($#m1_hidden :::"Function":::); end; 




registrationlet "T" be   ($#m1_hidden :::"DecoratedTree":::); 
cluster (Set   ($#k9_xtuple_0 :::"dom"::: )  "T") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_trees_1 :::"Tree-like"::: )   ; 
end; registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "D"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; mode DecoratedTree of "D" is "D"  ($#v5_relat_1 :::"-valued"::: )    ($#m1_hidden :::"DecoratedTree":::); end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); let "t" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Const "T"))); :: original: :::"."::: redefine func "T" :::"."::: "t" ->    ($#m1_subset_1 :::"Element"::: )   "of" "D"; end; 
theorem :: TREES_2:31 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (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"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (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"))))  ")" )) "holds"  (Bool (Set (Var "T1"))  ($#r1_hidden :::"="::: )  (Set (Var "T2")))) ; 
 scheme  :: TREES_2:sch 6 DTreeEx{ F1() ->   ($#m1_hidden :::"Tree":::), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (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 F1 "("  ")" ))) "holds"  (Bool P1[(Set (Var "p")) "," (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))])  ")" )  ")" ))
 provided
(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 F1 "("  ")" ))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "st" (Bool P1[(Set (Var "p")) "," (Set (Var "x"))])))
 proof 


end; scheme  :: TREES_2:sch 7 DTreeLambda{ F1() ->   ($#m1_hidden :::"Tree":::), F2(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )   } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::) "st"  (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set F1 "("  ")" )) & (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 F1 "("  ")" ))) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set F2 "(" (Set (Var "p")) ")" ))  ")" )  ")" ))
 proof 


end; definitionlet "T" be   ($#m1_hidden :::"DecoratedTree":::); func  :::"Leaves"::: "T" ->    ($#m1_hidden :::"set"::: )   equals :: TREES_2:def 9 (Set "T"  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k3_trees_1 :::"Leaves"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "T" ")" ) ")" )); let "p" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); func "T" :::"|"::: "p" ->   ($#m1_hidden :::"DecoratedTree":::) means :: TREES_2:def 10 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "T" ")" )  ($#k4_trees_1 :::"|"::: )  "p")) & (Bool  "("   "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "T" ")" )  ($#k4_trees_1 :::"|"::: )  "p"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set "T"  ($#k1_funct_1 :::"."::: )  (Set  "(" "p"  ($#k8_finseq_1 :::"^"::: )  (Set (Var "q")) ")" )))  ")" )  ")" ); end; 











:: deftheorem    defines :::"Leaves"::: TREES_2:def 9 :  (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set   ($#k4_trees_2 :::"Leaves"::: )  (Set (Var "T")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k3_trees_1 :::"Leaves"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")) ")" ) ")" )))); 
 
:: deftheorem    defines :::"|"::: TREES_2:def 10 :  (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")) ")" )  ($#k4_trees_1 :::"|"::: )  (Set (Var "p")))) & (Bool  "("   "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")) ")" )  ($#k4_trees_1 :::"|"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "q")) ")" )))  ")" )  ")" )  ")" )))); 
 
theorem :: TREES_2:32 (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))))) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "T"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "T")))))) ; 
 definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); :: original: :::"Leaves"::: redefine func  :::"Leaves"::: "T" ->   ($#m1_subset_1 :::"Subset":::) "of" "D"; end; registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "T" be   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); let "p" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Const "T"))); 
cluster (Set "T"  ($#k5_trees_2 :::"|"::: )  "p") -> "D"  ($#v5_relat_1 :::"-valued"::: )   ; 
end; definitionlet "T" be   ($#m1_hidden :::"DecoratedTree":::); let "p" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "T1" be   ($#m1_hidden :::"DecoratedTree":::); assume 
(Bool (Set (Const "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Const "T"))))
 ; func "T" :::"with-replacement":::  "(" "p" "," "T1" ")"  ->   ($#m1_hidden :::"DecoratedTree":::) means :: TREES_2:def 11 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "T" ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" "p" "," (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "T1" ")" ) ")" )) & (Bool  "("   "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "T" ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" "p" "," (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "T1" ")" ) ")" )) "or" (Bool  "("  (Bool (Bool  "not" "p"  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "q")))) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set "T"  ($#k1_funct_1 :::"."::: )  (Set (Var "q"))))  ")" ) "or" (Bool  "ex" (Set (Var "r")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "T1")) & (Bool (Set (Var "q"))  ($#r2_relset_1 :::"="::: )  (Set "p"  ($#k8_finseq_1 :::"^"::: )  (Set (Var "r")))) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set "T1"  ($#k1_funct_1 :::"."::: )  (Set (Var "r"))))  ")" ))  ")" )  ")" )  ")" ); end; 








:: deftheorem    defines :::"with-replacement"::: TREES_2:def 11 :  (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "T1")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k7_trees_2 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "T1")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")) ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T1")) ")" ) ")" )) & (Bool  "("   "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "holds"  (Bool  "("   "not" (Bool (Set (Var "q"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")) ")" )  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T1")) ")" ) ")" )) "or" (Bool  "("  (Bool (Bool  "not" (Set (Var "p"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "q")))) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q"))))  ")" ) "or" (Bool  "ex" (Set (Var "r")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T1")))) & (Bool (Set (Var "q"))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "r")))) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "r"))))  ")" ))  ")" )  ")" )  ")" )  ")" ))))); 
 registrationlet "W" be   ($#m1_hidden :::"Tree":::); let "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "W"  ($#k2_funcop_1 :::"-->"::: )  "x") ->   ($#v3_trees_2 :::"DecoratedTree-like"::: )   ; 
end; 
theorem :: TREES_2:33 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Tree":::))  ")" )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "D"))) "is"   ($#m1_hidden :::"Tree":::))) ; 
 
theorem :: TREES_2:34 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Function":::))  ")" ) & (Bool (Set (Var "X")) "is"   ($#v6_ordinal1 :::"c=-linear"::: )  )) "holds"  (Bool  "("  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) "is"   ($#v1_relat_1 :::"Relation-like"::: )  ) & (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "X"))) "is"   ($#v1_funct_1 :::"Function-like"::: )  )  ")" )) ; 
 
theorem :: TREES_2:35 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "D")))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"DecoratedTree":::))  ")" ) & (Bool (Set (Var "D")) "is"   ($#v6_ordinal1 :::"c=-linear"::: )  )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "D"))) "is"   ($#m1_hidden :::"DecoratedTree":::))) ; 
 
theorem :: TREES_2:36 (Bool  "for" (Set (Var "D9")) "," (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "D9")))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")))  ")" ) & (Bool (Set (Var "D9")) "is"   ($#v6_ordinal1 :::"c=-linear"::: )  )) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "D9"))) "is"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Var "D")))) ; 
 scheme  :: TREES_2:sch 8 DTreeStructEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F4() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))) "holds"   (Bool  "("  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set F3 "(" (Set  "(" (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ))  "}"  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set F3 "(" (Set  "(" (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ))) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set F4 "("  ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) "," (Set (Var "n")) ")" ))  ")" )  ")" )  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k2"))) & (Bool (Set (Var "k2"))  ($#r2_hidden :::"in"::: )  (Set F3 "(" (Set (Var "d")) ")" ))) "holds"  (Bool (Set (Var "k1"))  ($#r2_hidden :::"in"::: )  (Set F3 "(" (Set (Var "d")) ")" ))))
 proof 


end; scheme  :: TREES_2:sch 9 DTreeStructFinEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), F3(   ($#m1_hidden :::"set"::: )  ) ->    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ), F4() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))) "holds"   (Bool  "("  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set F3 "(" (Set  "(" (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ))  "}"  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set F3 "(" (Set  "(" (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ))) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set F4 "("  ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) "," (Set (Var "n")) ")" ))  ")" )  ")" )  ")" )  ")" ))
 proof 


end; begin  registrationlet "Tr" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::); let "v" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Const "Tr")); 
cluster (Set   ($#k1_trees_2 :::"succ"::: )  "v") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; definitionlet "Tr" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::); let "v" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Const "Tr")); func  :::"branchdeg"::: "v" ->    ($#m1_hidden :::"set"::: )   equals :: TREES_2:def 12 (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_trees_2 :::"succ"::: )  "v" ")" )); end; 






:: deftheorem    defines :::"branchdeg"::: TREES_2:def 12 :  (Bool  "for" (Set (Var "Tr")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "v")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Tr")) "holds"  (Bool (Set   ($#k8_trees_2 :::"branchdeg"::: )  (Set (Var "v")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_trees_2 :::"succ"::: )  (Set (Var "v")) ")" ))))); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "D"  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "a", "b" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   "a"  ($#v4_relat_1 :::"-defined"::: )   "b"  ($#v5_relat_1 :::"-valued"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) "a" "," "b" ($#k2_zfmisc_1 :::":]"::: ) )); 
end; 







theorem :: TREES_2:37 (Bool  "for" (Set (Var "Z1")) "," (Set (Var "Z2")) "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 (Var "Z1")))) "holds"  (Bool  "for" (Set (Var "v")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Set (Var "Z1"))  ($#k5_trees_1 :::"with-replacement"::: )   "(" (Set (Var "p")) "," (Set (Var "Z2")) ")" )  (Bool  "for" (Set (Var "w")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "Z2"))  "st" (Bool (Bool (Set (Var "v"))  ($#r2_relset_1 :::"="::: )  (Set (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "w"))))) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "v"))) "," (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")))  ($#r2_tarski :::"are_equipotent"::: )  ))))) ; 
 scheme  :: TREES_2:sch 10 DTreeStructEx{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )   ","    ($#m1_hidden :::"set"::: )  ], F3() ->   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set F1 "("  ")" ) "," (Set  ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r1_hidden :::"="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))) "holds"   (Bool  "("  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) where k "is"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) : (Bool P1[(Set (Var "k")) "," (Set (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")))])  "}"  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool P1[(Set (Var "n")) "," (Set (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")))])) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set F3 "("  ")" )  ($#k2_binop_1 :::"."::: )   "(" (Set  "(" (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) "," (Set (Var "n")) ")" ))  ")" )  ")" )  ")" )  ")" ))
 provided
(Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "k1")) "," (Set (Var "k2")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "k1"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k2"))) & (Bool P1[(Set (Var "k2")) "," (Set (Var "d"))])) "holds"  (Bool P1[(Set (Var "k1")) "," (Set (Var "d"))])))
 proof 


end; 
theorem :: TREES_2:38 (Bool  "for" (Set (Var "T1")) "," (Set (Var "T2")) "being"   ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "T1"))  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T2"))  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool (Set (Var "T1"))  ($#r1_hidden :::"="::: )  (Set (Var "T2")))) ; 
 
theorem :: TREES_2:39 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set  ($#k8_trees_1 :::"TrivialInfiniteTree"::: ) )  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "(" (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Set  ($#k6_numbers :::"0"::: ) ) ")" ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: TREES_2:40 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "B")) "being"   ($#v6_ordinal1 :::"c=-linear"::: )    ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")"  ")" ) "holds"  (Bool (Set   ($#k3_tarski :::"union"::: )  (Set (Var "B")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_partfun1 :::"PFuncs"::: )   "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )))) ;