:: BINTREE2 semantic presentation begin theorem :: BINTREE2:1 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ))))) ; theorem :: BINTREE2:2 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree1 :::"binary"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool (Set (Var "t")) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )))) ; definitionlet "T" be ($#v1_bintree1 :::"binary"::: ) ($#m1_hidden :::"Tree":::); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "T" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ); end; theorem :: BINTREE2:3 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ))) "holds" (Bool (Set (Var "T")) "is" ($#v1_bintree1 :::"binary"::: ) )) ; theorem :: BINTREE2:4 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ))) "holds" (Bool (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: BINTREE2:5 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree1 :::"binary"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m1_bintree2 :::"Element"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "T")) ($#k2_trees_2 :::"-level"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "t")) "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )))))) ; theorem :: BINTREE2:6 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k10_binarith :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Num 1) ($#k10_binarith :::"*>"::: ) ) ")" ) ($#k7_domain_1 :::"}"::: ) )) ")" )) "holds" (Bool (Set ($#k3_trees_1 :::"Leaves"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: BINTREE2:7 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k10_binarith :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Num 1) ($#k10_binarith :::"*>"::: ) ) ")" ) ($#k7_domain_1 :::"}"::: ) )) ")" )) "holds" (Bool (Set (Var "T")) "is" ($#v1_bintree1 :::"binary"::: ) )) ; theorem :: BINTREE2:8 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_trees_2 :::"succ"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k10_binarith :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "t")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Num 1) ($#k10_binarith :::"*>"::: ) ) ")" ) ($#k7_domain_1 :::"}"::: ) ))) ")" )) ; scheme :: BINTREE2:sch 1 DecoratedBinTreeEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "D")) "being" ($#v2_bintree1 :::"binary"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "D")) "holds" (Bool P1[(Set (Set (Var "D")) ($#k3_trees_2 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k10_binarith :::"*>"::: ) ) ")" )) "," (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Num 1) ($#k10_binarith :::"*>"::: ) ) ")" ))]) ")" ) ")" )) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool P1[(Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c"))]))) proof end; scheme :: BINTREE2:sch 2 DecoratedBinTreeEx1{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ], P2[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "D")) "being" ($#v2_bintree1 :::"binary"::: ) ($#m1_hidden :::"DecoratedTree":::) "of" (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) & (Bool (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_trees_1 :::"Node":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool P1[(Set (Set (Var "D")) ($#k3_trees_2 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k10_binarith :::"*>"::: ) ) ")" ))]) & (Bool P2[(Set (Set (Var "D")) ($#k3_trees_2 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "D")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Num 1) ($#k10_binarith :::"*>"::: ) ) ")" ))]) ")" ) ")" ) ")" )) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool P1[(Set (Var "a")) "," (Set (Var "b"))]))) and (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool P2[(Set (Var "a")) "," (Set (Var "b"))]))) proof end; definitionlet "T" be ($#v1_bintree1 :::"binary"::: ) ($#m1_hidden :::"Tree":::); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); func :::"NumberOnLevel"::: "(" "n" "," "T" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "T" ($#k2_trees_2 :::"-level"::: ) "n" ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) means :: BINTREE2:def 1 (Bool "for" (Set (Var "t")) "being" ($#m1_bintree2 :::"Element"::: ) "of" "T" "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set "T" ($#k2_trees_2 :::"-level"::: ) "n"))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "t"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_binarith :::"Absval"::: ) (Set (Var "F")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))); end; :: deftheorem defines :::"NumberOnLevel"::: BINTREE2:def 1 : (Bool "for" (Set (Var "T")) "being" ($#v1_bintree1 :::"binary"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "T")) ($#k2_trees_2 :::"-level"::: ) (Set (Var "n")) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree2 :::"NumberOnLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_bintree2 :::"Element"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "T")) ($#k2_trees_2 :::"-level"::: ) (Set (Var "n"))))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set (Var "t"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_binarith :::"Absval"::: ) (Set (Var "F")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))))) ")" )))); registrationlet "T" be ($#v1_bintree1 :::"binary"::: ) ($#m1_hidden :::"Tree":::); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k1_bintree2 :::"NumberOnLevel"::: ) "(" "n" "," "T" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; begin definitionlet "T" be ($#m1_hidden :::"Tree":::); attr "T" is :::"full"::: means :: BINTREE2:def 2 (Bool "T" ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) )); end; :: deftheorem defines :::"full"::: BINTREE2:def 2 : (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_bintree2 :::"full"::: ) ) "iff" (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) )) ")" )); theorem :: BINTREE2:9 (Bool (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ) "is" ($#m1_hidden :::"Tree":::)) ; theorem :: BINTREE2:10 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "T")) ($#k2_trees_2 :::"-level"::: ) (Set (Var "n")))))) ; theorem :: BINTREE2:11 (Bool "for" (Set (Var "T")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k3_finseq_2 :::"*"::: ) ))) "holds" (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "T")) ($#k2_trees_2 :::"-level"::: ) (Set (Var "n"))))))) ; registrationlet "T" be ($#v1_bintree1 :::"binary"::: ) ($#m1_hidden :::"Tree":::); let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "T" ($#k2_trees_2 :::"-level"::: ) "n") -> ($#v1_finset_1 :::"finite"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) ($#v1_bintree2 :::"full"::: ) -> ($#v1_bintree1 :::"binary"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_trees_1 :::"Tree-like"::: ) ($#v1_bintree2 :::"full"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: BINTREE2:12 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_bintree2 :::"NumberOnLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" ))))) ; definitionlet "T" be ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); func :::"FinSeqLevel"::: "(" "n" "," "T" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set "T" ($#k2_trees_2 :::"-level"::: ) "n") equals :: BINTREE2:def 3 (Set (Set "(" ($#k1_bintree2 :::"NumberOnLevel"::: ) "(" "n" "," "T" ")" ")" ) ($#k2_funct_1 :::"""::: ) ); end; :: deftheorem defines :::"FinSeqLevel"::: BINTREE2:def 3 : (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_bintree2 :::"NumberOnLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" ) ($#k2_funct_1 :::"""::: ) )))); registrationlet "T" be ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" "n" "," "T" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: BINTREE2:13 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_bintree2 :::"NumberOnLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)))) ; theorem :: BINTREE2:14 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k1_bintree2 :::"NumberOnLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_binarith :::"'not'"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n"))))))) ; theorem :: BINTREE2:15 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; theorem :: BINTREE2:16 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "y")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_binarith :::"'not'"::: ) (Set (Var "y"))))))) ; theorem :: BINTREE2:17 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_5 :::"Rev"::: ) (Set "(" (Set (Var "n")) ($#k1_binari_3 :::"-BinarySequence"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )))))) ; theorem :: BINTREE2:18 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "T")) ($#k2_trees_2 :::"-level"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")))))) ; theorem :: BINTREE2:19 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")))))) ; theorem :: BINTREE2:20 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set (Var "n")) ")" ))))) ; theorem :: BINTREE2:21 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "T")) ($#k2_trees_2 :::"-level"::: ) (Set (Var "n")))))) ; theorem :: BINTREE2:22 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Num 1) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k10_binarith :::"<*"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k10_binarith :::"*>"::: ) ))) ; theorem :: BINTREE2:23 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) "holds" (Bool (Set (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Num 1) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Num 2)) ($#r1_hidden :::"="::: ) (Set ($#k10_binarith :::"<*"::: ) (Num 1) ($#k10_binarith :::"*>"::: ) ))) ; theorem :: BINTREE2:24 (Bool "for" (Set (Var "T")) "being" ($#v1_bintree2 :::"full"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Num 2) ($#k5_series_1 :::"to_power"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) "st" (Bool (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set (Var "n")) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k3_nat_d :::"div"::: ) (Num 2) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_bintree2 :::"FinSeqLevel"::: ) "(" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "T")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_finseq_1 :::"^"::: ) (Set ($#k10_binarith :::"<*"::: ) (Set "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_nat_d :::"mod"::: ) (Num 2) ")" ) ($#k10_binarith :::"*>"::: ) )))))) ;