:: TREES_1 semantic presentation begin notationlet "p", "q" be ($#m1_hidden :::"FinSequence":::); synonym "p" :::"is_a_prefix_of"::: "q" for "p" :::"c="::: "q"; end; definitionlet "p", "q" be ($#m1_hidden :::"FinSequence":::); redefine pred "p" :::"c="::: "q" means :: TREES_1:def 1 (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "p" ($#r1_hidden :::"="::: ) (Set "q" ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"is_a_prefix_of"::: TREES_1:def 1 : (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )))) ")" )); theorem :: TREES_1:1 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "r"))))) ")" )) ; theorem :: TREES_1:2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: TREES_1:3 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k9_finseq_1 :::"*>"::: ) )) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )) ; notationlet "p", "q" be ($#m1_hidden :::"FinSequence":::); synonym "p" :::"is_a_proper_prefix_of"::: "q" for "p" :::"c<"::: "q"; end; theorem :: TREES_1:4 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) "," (Set (Var "q")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) ) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))) ; theorem :: TREES_1:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ) "," (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k9_finseq_1 :::"*>"::: ) ) ($#r3_xboole_0 :::"are_c=-comparable"::: ) )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) ; theorem :: TREES_1:6 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "p")) ($#r2_xboole_0 :::"c<"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "q"))))) ; theorem :: TREES_1:7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p2")))) "holds" (Bool (Set (Var "p1")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "p2"))))) ; theorem :: TREES_1:8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p2")))) "holds" (Bool (Set (Var "p1")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Set (Var "p2")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) ))))) ; theorem :: TREES_1:9 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p1")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Set (Var "p2")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )))) "holds" (Bool (Set (Var "p1")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p2"))))) ; theorem :: TREES_1:10 (Bool "for" (Set (Var "p2")) "," (Set (Var "p1")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool "(" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "p2"))) "or" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_hidden :::"<>"::: ) (Set (Var "p2"))) ")" )) "holds" (Bool (Set (Var "p1")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Set (Var "p1")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "p2"))))) ; definitionlet "p" be ($#m1_hidden :::"FinSequence":::); func :::"ProperPrefixes"::: "p" -> ($#m1_hidden :::"set"::: ) means :: TREES_1:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) "p") ")" )) ")" )); end; :: deftheorem defines :::"ProperPrefixes"::: TREES_1:def 2 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "ex" (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "p"))) ")" )) ")" )) ")" ))); theorem :: TREES_1:11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"FinSequence":::)))) ; theorem :: TREES_1:12 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "q")))) "iff" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "q"))) ")" )) ; theorem :: TREES_1:13 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) ; theorem :: TREES_1:14 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p"))))) ; theorem :: TREES_1:15 (Bool (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: TREES_1:16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "x")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: TREES_1:17 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "q")))) "holds" (Bool (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "q"))))) ; theorem :: TREES_1:18 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p")))) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Var "q")) "," (Set (Var "r")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) )) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"Tree-like"::: means :: TREES_1:def 3 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) "X") ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) "X")) ")" ) ")" ); end; :: deftheorem defines :::"Tree-like"::: TREES_1:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_trees_1 :::"Tree-like"::: ) ) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Set ($#k5_numbers :::"NAT"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (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 "X")))) "holds" (Bool (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) ")" ) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" ) ")" ) ")" )); registration cluster (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) -> ($#v1_trees_1 :::"Tree-like"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode Tree is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) ($#m1_hidden :::"set"::: ) ; end; theorem :: TREES_1:19 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "x")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )))) ; definitionlet "T" be ($#m1_hidden :::"Tree":::); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "T" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: TREES_1:20 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set (Var "q")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))))) ; theorem :: TREES_1:21 (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "r")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "q")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "r"))) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))))) ; theorem :: TREES_1:22 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" )) ; theorem :: TREES_1:23 (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_hidden :::"Tree":::)) ; registrationlet "T", "T1" be ($#m1_hidden :::"Tree":::); cluster (Set "T" ($#k2_xboole_0 :::"\/"::: ) "T1") -> ($#v1_trees_1 :::"Tree-like"::: ) ; cluster (Set "T" ($#k3_xboole_0 :::"/\"::: ) "T1") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) ; end; theorem :: TREES_1:24 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set (Var "T")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "T1"))) "is" ($#m1_hidden :::"Tree":::))) ; theorem :: TREES_1:25 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set (Var "T")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "T1"))) "is" ($#m1_hidden :::"Tree":::))) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#v1_trees_1 :::"Tree-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: TREES_1:26 (Bool "for" (Set (Var "fT")) "," (Set (Var "fT1")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set (Var "fT")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "fT1"))) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::))) ; theorem :: TREES_1:27 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "fT")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set (Var "fT")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "T"))) "is" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::)))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"elementary_tree"::: "n" -> ($#m1_hidden :::"Tree":::) equals :: TREES_1:def 4 (Set "{" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) "n") "}" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); end; :: deftheorem defines :::"elementary_tree"::: TREES_1:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set "{" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) "}" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k2_trees_1 :::"elementary_tree"::: ) "n") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: TREES_1:28 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n")))) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "n"))))) ; theorem :: TREES_1:29 (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; theorem :: TREES_1:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (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 ($#k2_trees_1 :::"elementary_tree"::: ) (Set (Var "n")))) "or" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool "ex" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "n"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) )) ")" )) ")" ))) ; definitionlet "T" be ($#m1_hidden :::"Tree":::); func :::"Leaves"::: "T" -> ($#m1_subset_1 :::"Subset":::) "of" "T" means :: TREES_1:def 5 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T") & (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"::: ) "T") "or" "not" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "q"))) ")" ) ")" ) ")" ) ")" )); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); assume (Bool (Set (Const "p")) ($#r2_hidden :::"in"::: ) (Set (Const "T"))) ; func "T" :::"|"::: "p" -> ($#m1_hidden :::"Tree":::) means :: TREES_1:def 6 (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set "p" ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) "T") ")" )); end; :: deftheorem defines :::"Leaves"::: TREES_1:def 5 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T")))) "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 "b2"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (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 (Var "T"))) "or" "not" (Bool (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "q"))) ")" ) ")" ) ")" ) ")" )) ")" ))); :: deftheorem defines :::"|"::: TREES_1:def 6 : (Bool "for" (Set (Var "T")) "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 "T")))) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p")))) "iff" (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q"))) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) ")" )) ")" )))); theorem :: TREES_1:31 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set (Var "T")) ($#k4_trees_1 :::"|"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "T")))) ; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); let "p" be ($#m1_trees_1 :::"Element"::: ) "of" (Set (Const "T")); cluster (Set "T" ($#k4_trees_1 :::"|"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "T" be ($#m1_hidden :::"Tree":::); assume (Bool (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Const "T"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; mode :::"Leaf"::: "of" "T" -> ($#m1_trees_1 :::"Element"::: ) "of" "T" means :: TREES_1:def 7 (Bool it ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) "T")); end; :: deftheorem defines :::"Leaf"::: TREES_1:def 7 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "b2")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_trees_1 :::"Leaf"::: ) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "b2")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T")))) ")" ))); definitionlet "T" be ($#m1_hidden :::"Tree":::); mode :::"Subtree"::: "of" "T" -> ($#m1_hidden :::"Tree":::) means :: TREES_1:def 8 (Bool "ex" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" "T" "st" (Bool it ($#r1_hidden :::"="::: ) (Set "T" ($#k4_trees_1 :::"|"::: ) (Set (Var "p"))))); end; :: deftheorem defines :::"Subtree"::: TREES_1:def 8 : (Bool "for" (Set (Var "T")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m3_trees_1 :::"Subtree"::: ) "of" (Set (Var "T"))) "iff" (Bool "ex" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "st" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p"))))) ")" )); definitionlet "T" be ($#m1_hidden :::"Tree":::); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T1" be ($#m1_hidden :::"Tree":::); assume (Bool (Set (Const "p")) ($#r2_hidden :::"in"::: ) (Set (Const "T"))) ; func "T" :::"with-replacement"::: "(" "p" "," "T1" ")" -> ($#m1_hidden :::"Tree":::) means :: TREES_1:def 9 (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) "T") & (Bool (Bool "not" "p" ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (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"::: ) "T1") & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set "p" ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) ")" )) ")" ) ")" )); end; :: deftheorem defines :::"with-replacement"::: TREES_1:def 9 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" )) "iff" (Bool "for" (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "(" (Bool "(" (Bool (Set (Var "q")) ($#r2_hidden :::"in"::: ) (Set (Var "T"))) & (Bool (Bool "not" (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (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 (Var "T1"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) ")" )) ")" ) ")" )) ")" ))))); theorem :: TREES_1:32 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set (Set (Var "T")) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ) ($#r1_hidden :::"="::: ) (Set "{" (Set (Var "t1")) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool (Bool "not" (Set (Var "p")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "t1")))) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "s")) ")" ) where s "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T1")) : (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "s"))) "}" )))) ; theorem :: TREES_1:33 (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) "holds" (Bool (Set (Var "T1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "T")) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ) ($#k4_trees_1 :::"|"::: ) (Set (Var "p")))))) ; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); let "t" be ($#m1_trees_1 :::"Element"::: ) "of" (Set (Const "T")); let "T1" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster (Set "T" ($#k5_trees_1 :::"with-replacement"::: ) "(" "t" "," "T1" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: TREES_1:34 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p"))) "," (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))) ($#r2_tarski :::"are_equipotent"::: ) )) ; registrationlet "p" be ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k1_trees_1 :::"ProperPrefixes"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: TREES_1:35 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_trees_1 :::"ProperPrefixes"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) ; definitionlet "IT" be ($#m1_hidden :::"set"::: ) ; attr "IT" is :::"AntiChain_of_Prefixes-like"::: means :: TREES_1:def 10 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "IT")) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"FinSequence":::)) ")" ) & (Bool "(" "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) "IT") & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool "not" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"AntiChain_of_Prefixes-like"::: TREES_1:def 10 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_trees_1 :::"AntiChain_of_Prefixes-like"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "IT")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"FinSequence":::)) ")" ) & (Bool "(" "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "p1")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "p2")) ($#r2_hidden :::"in"::: ) (Set (Var "IT"))) & (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set (Var "p2")))) "holds" (Bool "not" (Bool (Set (Var "p1")) "," (Set (Var "p2")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) )) ")" ) ")" ) ")" )); registration cluster ($#v2_trees_1 :::"AntiChain_of_Prefixes-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionmode AntiChain_of_Prefixes is ($#v2_trees_1 :::"AntiChain_of_Prefixes-like"::: ) ($#m1_hidden :::"set"::: ) ; end; theorem :: TREES_1:36 (Bool "for" (Set (Var "w")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "w")) ($#k1_tarski :::"}"::: ) ) "is" ($#v2_trees_1 :::"AntiChain_of_Prefixes-like"::: ) )) ; theorem :: TREES_1:37 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Bool "not" (Set (Var "p1")) "," (Set (Var "p2")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) ))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "p1")) "," (Set (Var "p2")) ($#k2_tarski :::"}"::: ) ) "is" ($#v2_trees_1 :::"AntiChain_of_Prefixes-like"::: ) )) ; definitionlet "T" be ($#m1_hidden :::"Tree":::); mode :::"AntiChain_of_Prefixes"::: "of" "T" -> ($#m1_hidden :::"AntiChain_of_Prefixes":::) means :: TREES_1:def 11 (Bool it ($#r1_tarski :::"c="::: ) "T"); end; :: deftheorem defines :::"AntiChain_of_Prefixes"::: TREES_1:def 11 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"AntiChain_of_Prefixes":::) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T"))) "iff" (Bool (Set (Var "b2")) ($#r1_tarski :::"c="::: ) (Set (Var "T"))) ")" ))); theorem :: TREES_1:38 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) "is" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T"))) & (Bool (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "is" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T"))) ")" )) ; theorem :: TREES_1:39 (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_tarski :::"{"::: ) (Set (Var "t")) ($#k1_tarski :::"}"::: ) ) "is" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T"))))) ; theorem :: TREES_1:40 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Bool "not" (Set (Var "t1")) "," (Set (Var "t2")) ($#r3_xboole_0 :::"are_c=-comparable"::: ) ))) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "t1")) "," (Set (Var "t2")) ($#k2_tarski :::"}"::: ) ) "is" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T"))))) ; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" "T"; end; definitionlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::); func :::"height"::: "T" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: TREES_1:def 12 (Bool "(" (Bool "ex" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T") & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) it) ")" )) & (Bool "(" "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) "T")) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) it) ")" ) ")" ); func :::"width"::: "T" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: TREES_1:def 13 (Bool "ex" (Set (Var "X")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" "T" "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" "T" "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) ")" ) ")" )); end; :: deftheorem defines :::"height"::: TREES_1:def 12 : (Bool "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "T")))) "iff" (Bool "(" (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 "T"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) ")" )) & (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 "T")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"width"::: TREES_1:def 13 : (Bool "for" (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_trees_1 :::"width"::: ) (Set (Var "T")))) "iff" (Bool "ex" (Set (Var "X")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "Y")) "being" ($#m4_trees_1 :::"AntiChain_of_Prefixes"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "X")))) ")" ) ")" )) ")" ))); theorem :: TREES_1:41 (Bool "for" (Set (Var "fT")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "holds" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_trees_1 :::"width"::: ) (Set (Var "fT"))))) ; theorem :: TREES_1:42 (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ; theorem :: TREES_1:43 (Bool "for" (Set (Var "fT")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "fT"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "fT")) ($#r1_hidden :::"="::: ) (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: TREES_1:44 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; theorem :: TREES_1:45 (Bool (Set ($#k7_trees_1 :::"width"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ; theorem :: TREES_1:46 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k7_trees_1 :::"width"::: ) (Set "(" ($#k2_trees_1 :::"elementary_tree"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) ; theorem :: TREES_1:47 (Bool "for" (Set (Var "fT")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "fT")) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" (Set (Var "fT")) ($#k4_trees_1 :::"|"::: ) (Set (Var "t")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "fT")))))) ; theorem :: TREES_1:48 (Bool "for" (Set (Var "fT")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "fT")) "st" (Bool (Bool (Set (Var "t")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k6_trees_1 :::"height"::: ) (Set "(" (Set (Var "fT")) ($#k4_trees_1 :::"|"::: ) (Set (Var "t")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_trees_1 :::"height"::: ) (Set (Var "fT")))))) ; scheme :: TREES_1:sch 1 TreeInd{ P1[ ($#m1_hidden :::"Tree":::)] } : (Bool "for" (Set (Var "fT")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "holds" (Bool P1[(Set (Var "fT"))])) provided (Bool "for" (Set (Var "fT")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) "st" (Bool (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "fT")))) "holds" (Bool P1[(Set (Set (Var "fT")) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ))]) ")" )) "holds" (Bool P1[(Set (Var "fT"))])) proof end; begin theorem :: TREES_1:49 (Bool "for" (Set (Var "w")) "," (Set (Var "t")) "," (Set (Var "s")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Set (Var "w")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "t"))) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Set (Var "w")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Var "t")) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set (Var "s")))) ; theorem :: TREES_1:50 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set (Var "m")))) "holds" (Bool "not" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set (Var "s"))))))) ; theorem :: TREES_1:51 (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) ($#k2_tarski :::"}"::: ) )) ; theorem :: TREES_1:52 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Bool "not" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "n")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_xboole_0 :::"is_a_proper_prefix_of"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "m")) ($#k12_finseq_1 :::"*>"::: ) )))) ; theorem :: TREES_1:53 (Bool (Set ($#k2_trees_1 :::"elementary_tree"::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set ($#k12_finseq_1 :::"<*"::: ) (Num 1) ($#k12_finseq_1 :::"*>"::: ) ) ($#k1_enumset1 :::"}"::: ) )) ; theorem :: TREES_1:54 (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 "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T")))) "iff" (Bool (Bool "not" (Set (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k12_finseq_1 :::"*>"::: ) )) ($#r2_hidden :::"in"::: ) (Set (Var "T")))) ")" ))) ; theorem :: TREES_1:55 (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 "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "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 "T"))))) ")" ))) ; definitionfunc :::"TrivialInfiniteTree"::: -> ($#m1_hidden :::"set"::: ) equals :: TREES_1:def 14 "{" (Set "(" (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ; end; :: deftheorem defines :::"TrivialInfiniteTree"::: TREES_1:def 14 : (Bool (Set ($#k8_trees_1 :::"TrivialInfiniteTree"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "k")) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ); registration cluster (Set ($#k8_trees_1 :::"TrivialInfiniteTree"::: ) ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) ; end; theorem :: TREES_1:56 (Bool (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k8_trees_1 :::"TrivialInfiniteTree"::: ) ) ($#r2_tarski :::"are_equipotent"::: ) ) ; registration cluster (Set ($#k8_trees_1 :::"TrivialInfiniteTree"::: ) ) -> ($#v1_finset_1 :::"infinite"::: ) ; end;