:: TREES_9  semantic presentation begin  definitionlet "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 "Tset" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "F")); :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "Tset" ->    ($#m1_subset_1 :::"Element"::: )   "of" "F"; end; registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_finset_1 :::"finite"::: )     ($#v1_trees_1 :::"Tree-like"::: )    ->   ($#v1_trees_2 :::"finite-order"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: TREES_9:1 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "t")))) ; 
 
theorem :: TREES_9:2 (Bool  "for" (Set (Var "t")) "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 (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set (Var "t")))) "holds"  (Bool (Set (Set (Var "t"))  ($#k4_trees_1 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "t"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "p")) ")" )  ($#k4_trees_1 :::"|"::: )  (Set (Var "q")))))) ; 
 
theorem :: TREES_9:3 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "q")))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t"))))) "holds"  (Bool (Set (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set  "(" (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" )  ($#k5_trees_2 :::"|"::: )  (Set (Var "q")))))) ; 
 notationlet "IT" be   ($#m1_hidden :::"DecoratedTree":::); synonym  :::"root"::: "IT" for  :::"trivial"::: ; end; definitionlet "IT" be   ($#m1_hidden :::"DecoratedTree":::); redefine attr "IT" is  :::"trivial":::  means :: TREES_9:def 1 (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  "IT")  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ))); end; 




:: deftheorem    defines :::"root"::: TREES_9:def 1 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_zfmisc_1 :::"root"::: )  ) "iff" (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "IT")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) )))  ")" )); 
 
theorem :: TREES_9:4 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Var "t")) "is"   ($#v1_zfmisc_1 :::"root"::: )  ) "iff" (Bool (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_trees_1 :::"Leaves"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t")) ")" )))  ")" )) ; 
 
theorem :: TREES_9:5 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "t")) "holds"   (Bool  "("  (Bool (Set (Set (Var "t"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_1 :::"elementary_tree"::: )  (Set  ($#k6_numbers :::"0"::: ) ))) "iff" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_trees_1 :::"Leaves"::: )  (Set (Var "t"))))  ")" ))) ; 
 
theorem :: TREES_9:6 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "holds"   (Bool  "("  (Bool (Set (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p"))) "is"   ($#v1_zfmisc_1 :::"root"::: )  ) "iff" (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_trees_1 :::"Leaves"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t")) ")" )))  ")" ))) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_zfmisc_1 :::"root"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_relat_1 :::"Relation-like"::: )    ($#~v1_zfmisc_1  "non"   ($#v1_zfmisc_1 :::"root"::: )   )    ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "x" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k1_trees_4 :::"root-tree"::: )  "x") ->   ($#v1_zfmisc_1 :::"root"::: )     ($#v1_finset_1 :::"finite"::: )   ; 
end; definitionlet "IT" be   ($#m1_hidden :::"Tree":::); attr "IT" is  :::"finite-branching":::  means :: TREES_9:def 2 (Bool  "for" (Set (Var "x")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" "IT" "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "x"))) "is"   ($#v1_finset_1 :::"finite"::: )  )); end; 




:: deftheorem    defines :::"finite-branching"::: TREES_9:def 2 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"Tree":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_trees_9 :::"finite-branching"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "IT")) "holds"  (Bool (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "x"))) "is"   ($#v1_finset_1 :::"finite"::: )  ))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_trees_1 :::"Tree-like"::: )     ($#v1_trees_2 :::"finite-order"::: )    ->   ($#v1_trees_9 :::"finite-branching"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; definitionlet "IT" be   ($#m1_hidden :::"DecoratedTree":::); attr "IT" is  :::"finite-order":::  means :: TREES_9:def 3 (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  "IT") "is"   ($#v1_trees_2 :::"finite-order"::: )  ); attr "IT" is  :::"finite-branching":::  means :: TREES_9:def 4 (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  "IT") "is"   ($#v1_trees_9 :::"finite-branching"::: )  ); end; 








:: deftheorem    defines :::"finite-order"::: TREES_9:def 3 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_trees_9 :::"finite-order"::: )  ) "iff" (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "IT"))) "is"   ($#v1_trees_2 :::"finite-order"::: )  )  ")" )); 
 
:: deftheorem    defines :::"finite-branching"::: TREES_9:def 4 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_trees_9 :::"finite-branching"::: )  ) "iff" (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "IT"))) "is"   ($#v1_trees_9 :::"finite-branching"::: )  )  ")" )); 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )    ->   ($#v2_trees_9 :::"finite-order"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_trees_2 :::"DecoratedTree-like"::: )     ($#v2_trees_9 :::"finite-order"::: )    ->   ($#v3_trees_9 :::"finite-branching"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; registrationlet "t" be   ($#v2_trees_9 :::"finite-order"::: )    ($#m1_hidden :::"DecoratedTree":::); 
cluster (Set   ($#k9_xtuple_0 :::"proj1"::: )  "t") ->   ($#v1_trees_2 :::"finite-order"::: )   ; 
end; registrationlet "t" be   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::); 
cluster (Set   ($#k9_xtuple_0 :::"proj1"::: )  "t") ->   ($#v1_trees_9 :::"finite-branching"::: )   ; 
end; registrationlet "t" be   ($#v1_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"Tree":::); let "p" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Const "t")); 
cluster (Set   ($#k1_trees_2 :::"succ"::: )  "p") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; scheme  :: TREES_9:sch 1 FinOrdSet{ F1(   ($#m1_hidden :::"set"::: )  ) ->    ($#m1_hidden :::"set"::: )  , F2() ->   ($#v1_finset_1 :::"finite"::: )     ($#m1_hidden :::"set"::: )   } : 
(Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set F1 "(" (Set (Var "n")) ")" )  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" )) "iff" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set F2 "("  ")" )))  ")" ))
 provided
(Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" ))) "holds"  (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set F1 "(" (Set (Var "n")) ")" ))))
 and  
(Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "j"))) & (Bool (Set F1 "(" (Set (Var "j")) ")" )  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" ))) "holds"  (Bool (Set F1 "(" (Set (Var "i")) ")" )  ($#r2_hidden :::"in"::: )  (Set F2 "("  ")" )))
 and  
(Bool  "for" (Set (Var "i")) "," (Set (Var "j")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set F1 "(" (Set (Var "i")) ")" )  ($#r1_hidden :::"="::: )  (Set F1 "(" (Set (Var "j")) ")" ))) "holds"  (Bool (Set (Var "i"))  ($#r1_hidden :::"="::: )  (Set (Var "j"))))
 proof 


end; 
theorem :: TREES_9:7 (Bool  "for" (Set (Var "t")) "being"   ($#v1_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "t"))  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "p")))) "iff" (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_trees_2 :::"succ"::: )  (Set (Var "p")) ")" )))  ")" )))) ; 
 definitionlet "t" be   ($#v1_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"Tree":::); let "p" be    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Const "t")); func "p" :::"succ":::  ->   ($#v2_funct_1 :::"one-to-one"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" "t" means :: TREES_9:def 5 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_trees_2 :::"succ"::: )  "p" ")" ))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_trees_2 :::"succ"::: )  "p")) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set "p"  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) )))  ")" )  ")" ); end; 






:: deftheorem    defines :::"succ"::: TREES_9:def 5 :  (Bool  "for" (Set (Var "t")) "being"   ($#v1_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "t"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v2_funct_1 :::"one-to-one"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "t")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_trees_9 :::"succ"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_trees_2 :::"succ"::: )  (Set (Var "p")) ")" ))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "p")))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "i")) ($#k12_finseq_1 :::"*>"::: ) )))  ")" )  ")" )  ")" )))); 
 definitionlet "t" be   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::); let "p" be   ($#m1_hidden :::"FinSequence":::); assume 
(Bool (Set (Const "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Const "t"))))
 ; func  :::"succ":::  "(" "t" "," "p" ")"  ->   ($#m1_hidden :::"FinSequence":::) means :: TREES_9:def 6 (Bool  "ex" (Set (Var "q")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  "t") "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  "p") & (Bool it  ($#r1_hidden :::"="::: )  (Set "t"  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k1_trees_9 :::"succ"::: )  ")" )))  ")" )); end; 







:: deftheorem    defines :::"succ"::: TREES_9:def 6 :  (Bool  "for" (Set (Var "t")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "t")) "," (Set (Var "p")) ")" )) "iff" (Bool  "ex" (Set (Var "q")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t"))) "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Var "p"))) & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "t"))  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set (Var "q"))  ($#k1_trees_9 :::"succ"::: )  ")" )))  ")" ))  ")" )))); 
 
theorem :: TREES_9:8 (Bool  "for" (Set (Var "t")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::) (Bool  "ex" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )  (Bool  "ex" (Set (Var "p")) "being"   ($#v6_trees_3 :::"DTree-yielding"::: )    ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p"))))))) ; 
 registrationlet "t" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::); let "p" be   ($#m1_trees_1 :::"Node":::) "of" (Set (Const "t")); 
cluster (Set "t"  ($#k5_trees_2 :::"|"::: )  "p") ->   ($#v1_finset_1 :::"finite"::: )   ; 
end; 
theorem :: TREES_9:9 (Bool  "for" (Set (Var "t")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "t"))  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "t"))  ($#k4_trees_1 :::"|"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set (Const "D")) ")" ); 
cluster   ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "S"; 
end; begin  definitionlet "t" be   ($#m1_hidden :::"DecoratedTree":::); func  :::"Subtrees"::: "t" ->    ($#m1_hidden :::"set"::: )   equals :: TREES_9:def 7  "{"  (Set  "(" "t"  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) where p "is"   ($#m1_trees_1 :::"Node":::) "of" "t" : (Bool verum)  "}"  ; end; 





:: deftheorem    defines :::"Subtrees"::: TREES_9:def 7 :  (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) where p "is"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) : (Bool verum)  "}"  )); 
 registrationlet "t" be   ($#m1_hidden :::"DecoratedTree":::); 
cluster (Set   ($#k3_trees_9 :::"Subtrees"::: )  "t") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )   ; 
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")); :: original: :::"Subtrees"::: redefine func  :::"Subtrees"::: "t" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_trees_3 :::"Trees"::: )  "D" ")" ); end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "t" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::) "of" (Set (Const "D")); :: original: :::"Subtrees"::: redefine func  :::"Subtrees"::: "t" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  "D" ")" ); end; registrationlet "t" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::); 
cluster   ->   ($#v1_finset_1 :::"finite"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_trees_9 :::"Subtrees"::: )  "t"); 
end; 








theorem :: TREES_9:10 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t")))) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "n")))))  ")" ))) ; 
 
theorem :: TREES_9:11 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t"))))) ; 
 
theorem :: TREES_9:12 (Bool  "for" (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (Bool (Bool (Set (Var "t1")) "is"   ($#v1_finset_1 :::"finite"::: )  ) & (Bool (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t1")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t2"))))) "holds"  (Bool (Set (Var "t1"))  ($#r1_hidden :::"="::: )  (Set (Var "t2")))) ; 
 
theorem :: TREES_9:13 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "n")) "being"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "holds"  (Bool (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "n")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t")))))) ; 
 definitionlet "t" be   ($#m1_hidden :::"DecoratedTree":::); func  :::"FixedSubtrees"::: "t" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "t" ")" ) "," (Set  "("  ($#k3_trees_9 :::"Subtrees"::: )  "t" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) equals :: TREES_9:def 8  "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set  "(" "t"  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) ($#k4_tarski :::"]"::: ) ) where p "is"   ($#m1_trees_1 :::"Node":::) "of" "t" : (Bool verum)  "}"  ; end; 





:: deftheorem    defines :::"FixedSubtrees"::: TREES_9:def 8 :  (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set   ($#k6_trees_9 :::"FixedSubtrees"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )   "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) ($#k4_tarski :::"]"::: ) ) where p "is"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) : (Bool verum)  "}"  )); 
 registrationlet "t" be   ($#m1_hidden :::"DecoratedTree":::); 
cluster (Set   ($#k6_trees_9 :::"FixedSubtrees"::: )  "t") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 
theorem :: TREES_9:14 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_trees_9 :::"FixedSubtrees"::: )  (Set (Var "t")))) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set (Var "n")) "," (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "n")) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" ))) ; 
 
theorem :: TREES_9:15 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k6_trees_9 :::"FixedSubtrees"::: )  (Set (Var "t"))))) ; 
 
theorem :: TREES_9:16 (Bool  "for" (Set (Var "t1")) "," (Set (Var "t2")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (Bool (Bool (Set   ($#k6_trees_9 :::"FixedSubtrees"::: )  (Set (Var "t1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_trees_9 :::"FixedSubtrees"::: )  (Set (Var "t2"))))) "holds"  (Bool (Set (Var "t1"))  ($#r1_hidden :::"="::: )  (Set (Var "t2")))) ; 
 definitionlet "t" be   ($#m1_hidden :::"DecoratedTree":::); let "C" be    ($#m1_hidden :::"set"::: )  ; func "C" :::"-Subtrees"::: "t" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k3_trees_9 :::"Subtrees"::: )  "t" ")" ) equals :: TREES_9:def 9  "{"  (Set  "(" "t"  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) where p "is"   ($#m1_trees_1 :::"Node":::) "of" "t" : (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")))  ($#r2_hidden :::"in"::: )  "C")  ")" )  "}"  ; end; 






:: deftheorem    defines :::"-Subtrees"::: TREES_9:def 9 :  (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "C"))  ($#k7_trees_9 :::"-Subtrees"::: )  (Set (Var "t")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) where p "is"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) : (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")))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))  ")" )  "}"  ))); 
 



theorem :: TREES_9:17 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k7_trees_9 :::"-Subtrees"::: )  (Set (Var "t")))) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "n")))) & (Bool  "("   "not" (Bool (Set (Var "n"))  ($#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 "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))  ")" )  ")" ))  ")" )))) ; 
 
theorem :: TREES_9:18 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "C"))  ($#k7_trees_9 :::"-Subtrees"::: )  (Set (Var "t"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "t")) "is"   ($#v1_zfmisc_1 :::"root"::: )  ) & (Bool (Bool  "not" (Set (Set (Var "t"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))))  ")" )  ")" ))) ; 
 definitionlet "t" be   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::); let "C" be    ($#m1_hidden :::"set"::: )  ; func "C" :::"-ImmediateSubtrees"::: "t" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" "C"  ($#k7_trees_9 :::"-Subtrees"::: )  "t" ")" ) "," (Set  "(" (Set  "("  ($#k3_trees_9 :::"Subtrees"::: )  "t" ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) means :: TREES_9:def 10 (Bool  "for" (Set (Var "d")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set "C"  ($#k7_trees_9 :::"-Subtrees"::: )  "t"))) "holds"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_trees_9 :::"Subtrees"::: )  "t")  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "d"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p")))))); end; 






:: deftheorem    defines :::"-ImmediateSubtrees"::: TREES_9:def 10 :  (Bool  "for" (Set (Var "t")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "C"))  ($#k7_trees_9 :::"-Subtrees"::: )  (Set (Var "t")) ")" ) "," (Set  "(" (Set  "("  ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t")) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k8_trees_9 :::"-ImmediateSubtrees"::: )  (Set (Var "t")))) "iff" (Bool  "for" (Set (Var "d")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k7_trees_9 :::"-Subtrees"::: )  (Set (Var "t"))))) "holds"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t")))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "d"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p"))))))  ")" )))); 
 begin  definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"Subtrees"::: "X" ->    ($#m1_hidden :::"set"::: )   equals :: TREES_9:def 11  "{"  (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) where t "is"    ($#m1_subset_1 :::"Element"::: )   "of" "X", p "is"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) : (Bool verum)  "}"  ; end; 





:: deftheorem    defines :::"Subtrees"::: TREES_9:def 11 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k9_trees_9 :::"Subtrees"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) where t "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")), p "is"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) : (Bool verum)  "}"  )); 
 registrationlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k9_trees_9 :::"Subtrees"::: )  "X") ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )   ; 
end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_trees_3 :::"Trees"::: )  (Set (Const "D")) ")" ); :: original: :::"Subtrees"::: redefine func  :::"Subtrees"::: "X" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_trees_3 :::"Trees"::: )  "D" ")" ); end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  (Set (Const "D")) ")" ); :: original: :::"Subtrees"::: redefine func  :::"Subtrees"::: "X" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k5_trees_3 :::"FinTrees"::: )  "D" ")" ); end; 




theorem :: TREES_9:19 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_trees_9 :::"Subtrees"::: )  (Set (Var "X")))) "iff" (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))(Bool  "ex" (Set (Var "n")) "being"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "st" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "n"))))))  ")" ))) ; 
 
theorem :: TREES_9:20 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_trees_9 :::"Subtrees"::: )  (Set (Var "X")))))) ; 
 
theorem :: TREES_9:21 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set   ($#k9_trees_9 :::"Subtrees"::: )  (Set (Var "X")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_trees_9 :::"Subtrees"::: )  (Set (Var "Y"))))) ; 
 registrationlet "t" be   ($#m1_hidden :::"DecoratedTree":::); 
cluster (Set  ($#k1_tarski :::"{"::: ) "t" ($#k1_tarski :::"}"::: ) ) ->   ($#v3_trees_3 :::"constituted-DTrees"::: )   ; 
end; 
theorem :: TREES_9:22 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::) "holds"  (Bool (Set   ($#k9_trees_9 :::"Subtrees"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "t")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t"))))) ; 
 
theorem :: TREES_9:23 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k9_trees_9 :::"Subtrees"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k3_trees_9 :::"Subtrees"::: )  (Set (Var "t")) ")" ) where t "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) : (Bool verum)  "}"  ))) ; 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )  ; let "C" be    ($#m1_hidden :::"set"::: )  ; func "C" :::"-Subtrees"::: "X" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k9_trees_9 :::"Subtrees"::: )  "X" ")" ) equals :: TREES_9:def 12  "{"  (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) where t "is"    ($#m1_subset_1 :::"Element"::: )   "of" "X", p "is"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) : (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")))  ($#r2_hidden :::"in"::: )  "C")  ")" )  "}"  ; end; 






:: deftheorem    defines :::"-Subtrees"::: TREES_9:def 12 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "C"))  ($#k12_trees_9 :::"-Subtrees"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )   "{"  (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) where t "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")), p "is"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) : (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")))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))  ")" )  "}"  ))); 
 
theorem :: TREES_9:24 (Bool  "for" (Set (Var "x")) "," (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k12_trees_9 :::"-Subtrees"::: )  (Set (Var "X")))) "iff" (Bool  "ex" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X"))(Bool  "ex" (Set (Var "n")) "being"   ($#m1_trees_1 :::"Node":::) "of" (Set (Var "t")) "st"  (Bool  "("  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "n")))) & (Bool  "("   "not" (Bool (Set (Var "n"))  ($#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 "n")))  ($#r2_hidden :::"in"::: )  (Set (Var "C")))  ")" )  ")" )))  ")" ))) ; 
 
theorem :: TREES_9:25 (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "C"))  ($#k12_trees_9 :::"-Subtrees"::: )  (Set (Var "X"))) "is"   ($#v1_xboole_0 :::"empty"::: )  ) "iff" (Bool  "for" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"   (Bool  "("  (Bool (Set (Var "t")) "is"   ($#v1_zfmisc_1 :::"root"::: )  ) & (Bool (Bool  "not" (Set (Set (Var "t"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))))  ")" ))  ")" ))) ; 
 
theorem :: TREES_9:26 (Bool  "for" (Set (Var "t")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "C"))  ($#k12_trees_9 :::"-Subtrees"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "t")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k7_trees_9 :::"-Subtrees"::: )  (Set (Var "t")))))) ; 
 
theorem :: TREES_9:27 (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "C"))  ($#k12_trees_9 :::"-Subtrees"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "(" (Set (Var "C"))  ($#k7_trees_9 :::"-Subtrees"::: )  (Set (Var "t")) ")" ) where t "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) : (Bool verum)  "}"  )))) ; 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )  ; assume 
(Bool  "for" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "X")) "holds"  (Bool (Set (Var "t")) "is"   ($#v1_finset_1 :::"finite"::: )  ))
 ; let "C" be    ($#m1_hidden :::"set"::: )  ; func "C" :::"-ImmediateSubtrees"::: "X" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" "C"  ($#k12_trees_9 :::"-Subtrees"::: )  "X" ")" ) "," (Set  "(" (Set  "("  ($#k9_trees_9 :::"Subtrees"::: )  "X" ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) means :: TREES_9:def 13 (Bool  "for" (Set (Var "d")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set "C"  ($#k12_trees_9 :::"-Subtrees"::: )  "X"))) "holds"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k9_trees_9 :::"Subtrees"::: )  "X")  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "d"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p")))))); end; 







:: deftheorem    defines :::"-ImmediateSubtrees"::: TREES_9:def 13 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v3_trees_3 :::"constituted-DTrees"::: )     ($#m1_hidden :::"set"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "t")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Var "t")) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )) "holds"  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "C"))  ($#k12_trees_9 :::"-Subtrees"::: )  (Set (Var "X")) ")" ) "," (Set  "(" (Set  "("  ($#k9_trees_9 :::"Subtrees"::: )  (Set (Var "X")) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "C"))  ($#k13_trees_9 :::"-ImmediateSubtrees"::: )  (Set (Var "X")))) "iff" (Bool  "for" (Set (Var "d")) "being"   ($#m1_hidden :::"DecoratedTree":::)  "st" (Bool (Bool (Set (Var "d"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k12_trees_9 :::"-Subtrees"::: )  (Set (Var "X"))))) "holds"  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k9_trees_9 :::"Subtrees"::: )  (Set (Var "X")))  "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "d"))))) "holds"  (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "d"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ) ")" )  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p"))))))  ")" )))); 
 registrationlet "t" be   ($#m1_hidden :::"Tree":::); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_xboole_0 :::"empty"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v1_finset_1 :::"finite"::: )     ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "t"; 
end; 
theorem :: TREES_9:28 (Bool  "for" (Set (Var "t")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t"))) "holds"   (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "("  ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "t")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "(" (Set (Var "p"))  ($#k1_trees_9 :::"succ"::: )  ")" ))) & (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "t")) "," (Set (Var "p")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "p"))  ($#k1_trees_9 :::"succ"::: )  ")" )))  ")" ))) ; 
 
theorem :: TREES_9:29 (Bool  "for" (Set (Var "p")) "being"   ($#v5_trees_3 :::"FinTree-yielding"::: )    ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "n")) "being"   ($#v1_xboole_0 :::"empty"::: )     ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k11_trees_3 :::"tree"::: )  (Set (Var "p"))) "holds"  (Bool (Set   ($#k5_card_1 :::"card"::: )  (Set  "("  ($#k1_trees_2 :::"succ"::: )  (Set (Var "n")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))))) ; 
 
theorem :: TREES_9:30 (Bool  "for" (Set (Var "t")) "being"   ($#v1_finset_1 :::"finite"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#v6_trees_3 :::"DTree-yielding"::: )    ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Set (Var "t"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k4_trees_4 :::"-tree"::: )  (Set (Var "p"))))) "holds"  (Bool  "for" (Set (Var "n")) "being"   ($#v1_xboole_0 :::"empty"::: )     ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "t"))) "holds"  (Bool (Set   ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "t")) "," (Set (Var "n")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k14_trees_3 :::"roots"::: )  (Set (Var "p")))))))) ; 
 registrationlet "T" be   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::); let "t" be   ($#m1_trees_1 :::"Node":::) "of" (Set (Const "T")); 
cluster (Set "T"  ($#k5_trees_2 :::"|"::: )  "t") ->   ($#v3_trees_9 :::"finite-branching"::: )   ; 
end; 
theorem :: TREES_9:31 (Bool  "for" (Set (Var "t")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (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  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) "holds"  (Bool (Set   ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "t")) "," (Set  "(" (Set (Var "p"))  ($#k8_finseq_1 :::"^"::: )  (Set (Var "q")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k2_trees_9 :::"succ"::: )   "(" (Set  "(" (Set (Var "t"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" ) "," (Set (Var "q")) ")" ))))) ; 
 begin  
theorem :: TREES_9:32 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_hidden :::"FinSequence":::) (Bool  "ex" (Set (Var "q")) "being"   ($#m1_hidden :::"FinSequence":::) "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "n")) ")" ))) & (Bool (Set (Var "q"))  ($#r1_tarski :::"is_a_prefix_of"::: )  (Set (Var "r")))  ")" )))) ; 
 
theorem :: TREES_9:33 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "r1")) "," (Set (Var "r2")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "k")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "r")))) & (Bool (Set (Var "r1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k5_relset_1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set  "(" (Set (Var "k"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ))) & (Bool (Set (Var "r2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k5_relset_1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Set (Var "k")) ")" )))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) "st" (Bool (Set (Var "r1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r2"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )))))))) ; 
 
theorem :: TREES_9:34 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "r1")) "being"   ($#m1_hidden :::"FinSequence":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "r")))) & (Bool (Set (Var "r1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k5_relset_1 :::"|"::: )  (Set  "("  ($#k2_finseq_1 :::"Seg"::: )  (Num 1) ")" )))) "holds"  (Bool  "ex" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) "st" (Bool (Set (Var "r1"))  ($#r1_hidden :::"="::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k12_finseq_1 :::"*>"::: ) )))))) ; 
 






theorem :: TREES_9:35 (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "T"))  ($#k5_trees_2 :::"|"::: )  (Set (Var "p")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))))) ; 
 













theorem :: TREES_9:36 (Bool  "for" (Set (Var "T")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))) "holds"  (Bool (Set   ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "T")) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k1_trees_9 :::"succ"::: )  ")" ))))) ; 
 
theorem :: TREES_9:37 (Bool  "for" (Set (Var "T")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))) "holds"  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set  "(" (Set (Var "T"))  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set (Var "t"))  ($#k1_trees_9 :::"succ"::: )  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "t"))  ($#k1_trees_9 :::"succ"::: )  ")" ))))) ; 
 
theorem :: TREES_9:38 (Bool  "for" (Set (Var "T")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))) "holds"  (Bool (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "("  ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "T")) "," (Set (Var "t")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "t"))  ($#k1_trees_9 :::"succ"::: )  ")" ))))) ; 
 
theorem :: TREES_9:39 (Bool  "for" (Set (Var "T")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")))  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Set (Var "t"))  ($#k8_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")))) "iff" (Bool (Set (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "(" (Set (Var "t"))  ($#k1_trees_9 :::"succ"::: )  ")" )))  ")" )))) ; 
 
theorem :: TREES_9:40 (Bool  "for" (Set (Var "T")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "x")) "being"   ($#m1_hidden :::"FinSequence":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Set (Var "x"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))))) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "x"))  ($#k7_finseq_1 :::"^"::: )  (Set  ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "T")) "," (Set (Var "x")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" )))))) ; 
 







theorem :: TREES_9:41 (Bool  "for" (Set (Var "T")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "x9")) "," (Set (Var "x")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")))  "st" (Bool (Bool (Set (Var "x9"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "x"))))) "holds"  (Bool (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x9")))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "T")) "," (Set (Var "x")) ")"  ")" ))))) ; 
 
theorem :: TREES_9:42 (Bool  "for" (Set (Var "T")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T")))  (Bool  "for" (Set (Var "y9")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "y9"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "T")) "," (Set (Var "x")) ")"  ")" )))) "holds"  (Bool  "ex" (Set (Var "x9")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "T"))) "st"  (Bool  "("  (Bool (Set (Var "y9"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x9")))) & (Bool (Set (Var "x9"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "x"))))  ")" ))))) ; 
 











scheme  :: TREES_9:sch 2 ExDecTrees{ 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_finseq_1 :::"FinSequence"::: )   "of" (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "T")) "being"   ($#v3_trees_9 :::"finite-branching"::: )    ($#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")))  (Bool  "for" (Set (Var "w")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "w"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "T"))  ($#k3_trees_2 :::"."::: )  (Set (Var "t"))))) "holds"  (Bool (Set   ($#k2_trees_9 :::"succ"::: )   "(" (Set (Var "T")) "," (Set (Var "t")) ")" )  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "w")) ")" )))  ")" )  ")" ))
 proof 


end; 
theorem :: TREES_9:43 (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "T")) "holds"  (Bool (Set   ($#k1_trees_1 :::"ProperPrefixes"::: )  (Set (Var "t"))) "is"   ($#v1_finset_1 :::"finite"::: )     ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "T"))))) ; 
 
theorem :: TREES_9:44 (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"Tree":::) "holds"  (Bool (Set (Set (Var "T"))  ($#k2_trees_2 :::"-level"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: TREES_9:45 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"Tree":::) "holds"  (Bool (Set (Set (Var "T"))  ($#k2_trees_2 :::"-level"::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  "("  ($#k1_trees_2 :::"succ"::: )  (Set (Var "w")) ")" ) where w "is"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "T")) : (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "w")))  ($#r1_hidden :::"="::: )  (Set (Var "n")))  "}"  )))) ; 
 
theorem :: TREES_9:46 (Bool  "for" (Set (Var "T")) "being"   ($#v1_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "T"))  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n"))) "is"   ($#v1_finset_1 :::"finite"::: )  ))) ; 
 
theorem :: TREES_9:47 (Bool  "for" (Set (Var "T")) "being"   ($#v1_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"Tree":::) "holds"   (Bool  "("  (Bool (Set (Var "T")) "is"   ($#v1_finset_1 :::"finite"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st" (Bool (Set (Set (Var "T"))  ($#k2_trees_2 :::"-level"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))  ")" )) ; 
 
theorem :: TREES_9:48 (Bool  "for" (Set (Var "T")) "being"   ($#v1_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "T")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool  "ex" (Set (Var "C")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "T")) "st" (Bool (Bool  "not" (Set (Var "C")) "is"   ($#v1_finset_1 :::"finite"::: )  )))) ; 
 
theorem :: TREES_9:49 (Bool  "for" (Set (Var "T")) "being"   ($#v1_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"Tree":::)  "st" (Bool (Bool (Bool  "not" (Set (Var "T")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool  "ex" (Set (Var "B")) "being"   ($#m1_trees_2 :::"Branch":::) "of" (Set (Var "T")) "st" (Bool (Bool  "not" (Set (Var "B")) "is"   ($#v1_finset_1 :::"finite"::: )  )))) ; 
 
theorem :: TREES_9:50 (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_trees_2 :::"Chain"::: )   "of" (Set (Var "T"))  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Bool  "not" (Set (Var "C")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool  "ex" (Set (Var "t9")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "t9"))  ($#r2_hidden :::"in"::: )  (Set (Var "C"))) & (Bool (Set (Var "t"))  ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: )  (Set (Var "t9")))  ")" ))))) ; 
 
theorem :: TREES_9:51 (Bool  "for" (Set (Var "T")) "being"   ($#m1_hidden :::"Tree":::)  (Bool  "for" (Set (Var "B")) "being"   ($#m1_trees_2 :::"Branch":::) "of" (Set (Var "T"))  (Bool  "for" (Set (Var "t")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "T"))  "st" (Bool (Bool (Set (Var "t"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Bool  "not" (Set (Var "B")) "is"   ($#v1_finset_1 :::"finite"::: )  ))) "holds"  (Bool  "ex" (Set (Var "t9")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set (Var "T")) "st"  (Bool  "("  (Bool (Set (Var "t9"))  ($#r2_hidden :::"in"::: )  (Set (Var "B"))) & (Bool (Set (Var "t9"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "t"))))  ")" ))))) ; 
 
theorem :: TREES_9:52 (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  ($#k5_numbers :::"NAT"::: ) )  "st" (Bool (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set  "(" (Set (Var "n"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n"))))  ")" )) "holds"  (Bool  "ex" (Set (Var "m")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "st"  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "m"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k8_nat_1 :::"."::: )  (Set (Var "m"))))))) ; 
 scheme  :: TREES_9:sch 3 FinDecTree{ F1() ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  , F2() ->   ($#v3_trees_9 :::"finite-branching"::: )    ($#m1_hidden :::"DecoratedTree":::) "of" (Set F1 "("  ")" ), F3(   ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )) ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) } : 
(Bool (Set F2 "("  ")" ) "is"   ($#v1_finset_1 :::"finite"::: )  )
 provided
(Bool  "for" (Set (Var "t")) "," (Set (Var "t9")) "being"    ($#m1_trees_1 :::"Element"::: )   "of" (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set F2 "("  ")" ))  (Bool  "for" (Set (Var "d")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "t9"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_trees_2 :::"succ"::: )  (Set (Var "t")))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Set F2 "("  ")" )  ($#k3_trees_2 :::"."::: )  (Set (Var "t9"))))) "holds"  (Bool (Set F3 "(" (Set (Var "d")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set F3 "(" (Set  "(" (Set F2 "("  ")" )  ($#k3_trees_2 :::"."::: )  (Set (Var "t")) ")" ) ")" ))))
 proof 


end;