:: PRE_CIRC semantic presentation begin scheme :: PRE_CIRC:sch 1 FraenkelFinIm{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "{" (Set F2 "(" (Set (Var "x")) ")" ) where x "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) : (Bool P1[(Set (Var "x"))]) "}" "is" ($#v1_finset_1 :::"finite"::: ) ) proof end; theorem :: PRE_CIRC:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; begin theorem :: PRE_CIRC:2 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "MSS")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" (Set (Var "MSS")) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; scheme :: PRE_CIRC:sch 2 MSSLambda2Part{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "i"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "i")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "i"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "i")) ")" )) ")" ")" ))) proof end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV2_FINSET_1() for ($#m1_hidden :::"set"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); cluster (Set "M" ($#k5_relat_1 :::"|"::: ) "A") -> "A" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"A" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "I")); cluster (Set "M" ($#k5_relat_1 :::"|"::: ) "A") -> ($#v1_partfun1 :::"total"::: ) ; end; registrationlet "M" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::); let "A" be ($#m1_hidden :::"set"::: ) ; cluster (Set "M" ($#k5_relat_1 :::"|"::: ) "A") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; theorem :: PRE_CIRC:3 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool (Bool "not" (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "B")) ")" )) "is" ($#v1_xboole_0 :::"empty"::: ) )))) ; theorem :: PRE_CIRC:4 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set "(" (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PRE_CIRC:5 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "A"))) "," (Set (Var "B")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))))))) ; scheme :: PRE_CIRC:sch 3 LambdaRecCorrD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F3( ($#m1_hidden :::"Nat":::) "," ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) } : (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "i")) "," (Set "(" (Set (Var "f")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) ")" )) & (Bool "(" "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Set (Var "f1")) ($#k8_nat_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f1")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "i")) "," (Set "(" (Set (Var "f1")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" ) & (Bool (Set (Set (Var "f2")) ($#k8_nat_1 :::"."::: ) (Set ($#k1_xboole_0 :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set F2 "(" ")" )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "f2")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "i")) "," (Set "(" (Set (Var "f2")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) ")" ) ")" ) proof end; scheme :: PRE_CIRC:sch 4 LambdaMSFD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), F3() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set F2 "(" ")" ), F4() -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set F3 "(" ")" ) "," (Set F4 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "i")) ")" )))) provided (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) "holds" (Bool (Set F5 "(" (Set (Var "i")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set F4 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) proof end; theorem :: PRE_CIRC:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f"))) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f")))))))) ; theorem :: PRE_CIRC:7 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "InpFs")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set (Var "A")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "B"))) "," (Set (Var "C")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) (Bool "ex" (Set (Var "c")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "A")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "InpFs")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b")))) & (Bool (Set (Var "c")) ($#r3_pboole :::"in"::: ) (Set (Var "C"))) ")" )))))) ; theorem :: PRE_CIRC:8 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "n")) ($#k2_finseq_2 :::"|->"::: ) (Set (Var "a")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; begin registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_trees_3 :::"FinTrees"::: ) "D"); end; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::); let "t" be ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "T"))); cluster (Set "T" ($#k5_trees_2 :::"|"::: ) "t") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: PRE_CIRC: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")) "holds" (Bool (Set (Set (Var "T")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p"))) "," "{" (Set (Var "t")) where t "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t"))) "}" ($#r2_tarski :::"are_equipotent"::: ) ))) ; registrationlet "T" be ($#v1_finset_1 :::"finite"::: ) ($#v3_trees_2 :::"DecoratedTree-like"::: ) ($#m1_hidden :::"Function":::); let "t" be ($#m1_trees_1 :::"Element"::: ) "of" (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "T"))); let "T1" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::); cluster (Set "T" ($#k7_trees_2 :::"with-replacement"::: ) "(" "t" "," "T1" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: PRE_CIRC:10 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (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 "t")) where t "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) : (Bool (Bool "not" (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "t")))) "}" ($#k2_xboole_0 :::"\/"::: ) "{" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "t1")) ")" ) where t1 "is" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T1")) : (Bool verum) "}" )))) ; theorem :: PRE_CIRC:11 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "T")) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" )) & (Bool (Set (Var "p")) ($#r1_tarski :::"is_a_prefix_of"::: ) (Set (Var "f")))) "holds" (Bool "ex" (Set (Var "t1")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T1")) "st" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "t1")))))))) ; theorem :: PRE_CIRC:12 (Bool "for" (Set (Var "p")) "being" ($#v4_trees_3 :::"Tree-yielding"::: ) ($#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)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "p")) ")" ) ($#k4_trees_1 :::"|"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))))) ; theorem :: PRE_CIRC:13 (Bool "for" (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#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)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k11_trees_3 :::"tree"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "q")) ")" ))))) ; theorem :: PRE_CIRC:14 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v4_trees_3 :::"Tree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" )) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"Tree":::) "st" (Bool (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "t")))) "holds" (Bool (Set ($#k11_trees_3 :::"tree"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_trees_3 :::"tree"::: ) (Set (Var "p")) ")" ) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "t")) ")" ))))) ; theorem :: PRE_CIRC:15 (Bool "for" (Set (Var "e1")) "," (Set (Var "e2")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"DecoratedTree":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "e1")))) & (Bool (Set (Var "e1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "p"))))) "holds" (Bool "ex" (Set (Var "q")) "being" ($#v6_trees_3 :::"DTree-yielding"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool "(" (Bool (Set (Set (Var "e1")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "k")) ($#k12_finseq_1 :::"*>"::: ) ) "," (Set (Var "e2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k4_trees_4 :::"-tree"::: ) (Set (Var "q")))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "e2"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" )))))) ; theorem :: PRE_CIRC:16 (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 "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "T")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "T")))))) ; theorem :: PRE_CIRC:17 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Tree":::) (Bool "for" (Set (Var "p")) "being" ($#m1_trees_1 :::"Element"::: ) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "T")) ($#k5_trees_1 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "T")) ($#k4_trees_1 :::"|"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "T")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "T1")) ")" ))))) ; theorem :: PRE_CIRC:18 (Bool "for" (Set (Var "T")) "," (Set (Var "T1")) "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 (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "T")) ($#k7_trees_2 :::"with-replacement"::: ) "(" (Set (Var "p")) "," (Set (Var "T1")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "T")) ($#k5_trees_2 :::"|"::: ) (Set (Var "p")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "T")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "T1")) ")" ))))) ; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_trees_4 :::"root-tree"::: ) "x") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: PRE_CIRC:19 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; begin theorem :: PRE_CIRC:20 (Bool "for" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k1_xreal_0 :::"-'"::: ) (Num 1)))) ; theorem :: PRE_CIRC:21 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) "," (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r2_tarski :::"are_equipotent"::: ) ) "iff" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_tarski :::"are_equipotent"::: ) ) ")" )) ; theorem :: PRE_CIRC:22 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "f")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "g")) ")" )))) ; theorem :: PRE_CIRC:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "{" (Set (Var "k")) where k "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set (Var "n"))) "}" "is" ($#v1_finset_1 :::"infinite"::: ) )) ;