:: PRE_POLY semantic presentation begin definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "p", "q" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); :: original: :::"^"::: redefine func "p" :::"^"::: "q" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_xboole_0 :::"empty"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v4_card_3 :::"countable"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; :: original: :::"<*>"::: redefine func :::"<*>"::: "D" -> ($#v1_xboole_0 :::"empty"::: ) ($#m2_finseq_2 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"d":::"*>"::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); let "e" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"<*"::: redefine func :::"<*":::"d" "," "e":::"*>"::: -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "X" ($#k3_finseq_2 :::"*"::: ) ); end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); func :::"FlattenSeq"::: "F" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ) means :: PRE_POLY:def 1 (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" "D" ($#k3_finseq_2 :::"*"::: ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_pre_poly :::"^"::: ) (Set (Var "q")))) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) "F")) ")" )); end; :: deftheorem defines :::"FlattenSeq"::: PRE_POLY:def 1 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_pre_poly :::"^"::: ) (Set (Var "q")))) ")" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_finsop_1 :::""**""::: ) (Set (Var "F")))) ")" )) ")" )))); theorem :: PRE_POLY:1 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set (Var "d")) ($#k3_pre_poly :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ; theorem :: PRE_POLY:2 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set "(" ($#k2_pre_poly :::"<*>"::: ) (Set "(" (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_pre_poly :::"<*>"::: ) (Set (Var "D"))))) ; theorem :: PRE_POLY:3 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set "(" (Set (Var "F")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")) ")" ) ($#k1_pre_poly :::"^"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "G")) ")" ))))) ; theorem :: PRE_POLY:4 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_pre_poly :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_pre_poly :::"^"::: ) (Set (Var "q")))))) ; theorem :: PRE_POLY:5 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k1_pre_poly :::"^"::: ) (Set (Var "q")) ")" ) ($#k1_pre_poly :::"^"::: ) (Set (Var "r")))))) ; theorem :: PRE_POLY:6 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set (Var "F")) ($#r1_relset_1 :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F"))) ($#r1_relset_1 :::"c="::: ) (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "G")))))) ; begin scheme :: PRE_POLY:sch 1 Regr1{ F1() -> ($#m1_hidden :::"Nat":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "k"))])) provided (Bool P1[(Set F1 "(" ")" )]) and (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1))])) "holds" (Bool P1[(Set (Var "k"))])) proof end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_finseq_1 :::"Seg"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: PRE_POLY:7 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k2_wellord1 :::"|_2"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "X" ")" )); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "X" ")" )); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X")) ")" ); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" "F"; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v2_setfam_1 :::"with_non-empty_element"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "X" ")" )); end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Order":::) "of" (Set (Const "X")); let "A" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); :: original: :::"|_2"::: redefine func "R" :::"|_2"::: "A" -> ($#m1_subset_1 :::"Order":::) "of" "A"; end; scheme :: PRE_POLY:sch 2 SubFinite{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool P1[(Set F2 "(" ")" )]) provided (Bool (Set F2 "(" ")" ) "is" ($#v1_finset_1 :::"finite"::: ) ) and (Bool P1[(Set ($#k1_subset_1 :::"{}"::: ) (Set F1 "(" ")" ))]) and (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "B"))])) "holds" (Bool P1[(Set (Set (Var "B")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))]))) proof end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v2_setfam_1 :::"with_non-empty_element"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X")) ")" ); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "F"; end; theorem :: PRE_POLY:8 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "R" be ($#m1_subset_1 :::"Order":::) "of" (Set (Const "X")); assume (Bool (Set (Const "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Const "A"))) ; func :::"SgmX"::: "(" "R" "," "A" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "X" means :: PRE_POLY:def 2 (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) it) ($#r1_hidden :::"="::: ) "A") & (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it)) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it)) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set it ($#k7_partfun1 :::"/."::: ) (Set (Var "m")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) "," (Set "(" it ($#k7_partfun1 :::"/."::: ) (Set (Var "m")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" ) ")" ) ")" ); end; :: deftheorem defines :::"SgmX"::: PRE_POLY:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "A")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" )) "iff" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "m")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "b4")) ($#k7_partfun1 :::"/."::: ) (Set (Var "m")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" ) ")" ) ")" ))))); theorem :: PRE_POLY:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "m")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "m")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" ) ")" )) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" )))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X")) ")" ); cluster -> ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "F"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X")) ")" ); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "F" -> ($#m1_subset_1 :::"Subset":::) "of" "X"; end; theorem :: PRE_POLY:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; theorem :: PRE_POLY:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))))) ; begin theorem :: PRE_POLY:12 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "M")) "," (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: PRE_POLY:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "M")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "M"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool (Set (Var "M")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_finseq_3 :::"Del"::: ) "(" (Set (Var "M")) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ")" ")" ) ($#k7_finseq_1 :::"^"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "M")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "M")) ")" ) ")" ) ($#k9_finseq_1 :::"*>"::: ) ))))) ; definitionlet "IT" be ($#m1_hidden :::"Function":::); attr "IT" is :::"FinSequence-yielding"::: means :: PRE_POLY:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "IT"))) "holds" (Bool (Set "IT" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"FinSequence":::))); end; :: deftheorem defines :::"FinSequence-yielding"::: PRE_POLY:def 3 : (Bool "for" (Set (Var "IT")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v1_pre_poly :::"FinSequence-yielding"::: ) ) "iff" (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 "IT"))))) "holds" (Bool (Set (Set (Var "IT")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"FinSequence":::))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "F", "G" be ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"Function":::); func "F" :::"^^"::: "G" -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"Function":::) means :: PRE_POLY:def 4 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "F" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "G" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set "G" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "g"))))) ")" ) ")" ); end; :: deftheorem defines :::"^^"::: PRE_POLY:def 4 : (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "," (Set (Var "b3")) "being" ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_pre_poly :::"^^"::: ) (Set (Var "G")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "G")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "g"))))) ")" ) ")" ) ")" )); begin theorem :: PRE_POLY:14 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "st" (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: PRE_POLY:15 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ))))) ; theorem :: PRE_POLY:16 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_setfam_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "V")) "," (Set (Var "C")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: PRE_POLY:17 (Bool "for" (Set (Var "V")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "V")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "C")) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V")) "," (Set (Var "C")) ")" ) "is" ($#v1_finset_1 :::"finite"::: ) )) ; registration cluster ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; begin registrationlet "D" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "D" ($#k3_finseq_2 :::"*"::: ) ); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_pre_poly :::"FinSequence-yielding"::: ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; begin theorem :: PRE_POLY:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k1_relat_1 :::"field"::: ) (Set (Var "R"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "R")) "is" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X"))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "y" ")" ) -> "X" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "y" ")" ) -> "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"X" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; theorem :: PRE_POLY:19 (Bool "for" (Set (Var "f")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" )))) ; definitionlet "A", "X" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_finseq_2 :::"FinSequenceSet"::: ) "of" (Set (Const "A")); let "p" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "D")); let "i" be ($#m1_hidden :::"set"::: ) ; :: original: :::"/."::: redefine func "p" :::"/."::: "i" -> ($#m2_finseq_2 :::"Element"::: ) "of" "D"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v2_wellord1 :::"well-ordering"::: ) ($#v3_orders_1 :::"being_linear-order"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: PRE_POLY:20 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) "holds" (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))) ; theorem :: PRE_POLY:21 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "R")) ($#r3_orders_1 :::"linearly_orders"::: ) (Set (Var "A"))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) "holds" (Bool (Set (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k7_pre_poly :::"SgmX"::: ) "(" (Set (Var "R")) "," (Set (Var "A")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "R" be ($#v3_orders_1 :::"being_linear-order"::: ) ($#m1_subset_1 :::"Order":::) "of" (Set (Const "X")); cluster (Set ($#k7_pre_poly :::"SgmX"::: ) "(" "R" "," "A" ")" ) -> ($#v2_funct_1 :::"one-to-one"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_xboole_0 :::"empty"::: ) -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "F", "G" be ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "F" ($#k8_pre_poly :::"^^"::: ) "G") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v1_pre_poly :::"FinSequence-yielding"::: ) ; end; registrationlet "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m1_hidden :::"FinSequence":::); cluster (Set "i" ($#k2_finseq_2 :::"|->"::: ) "f") -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) ; end; registrationlet "F" be ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "F" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registrationlet "F" be ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k1_card_3 :::"Card"::: ) "F") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_card_3 :::"Cardinal-yielding"::: ) ($#v4_card_3 :::"countable"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: PRE_POLY:22 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_card_3 :::"Cardinal-yielding"::: ) ) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "y")) "is" ($#m1_hidden :::"Cardinal":::))) ")" )) ; registrationlet "F", "G" be ($#v1_card_3 :::"Cardinal-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "F" ($#k7_finseq_1 :::"^"::: ) "G") -> ($#v1_card_3 :::"Cardinal-yielding"::: ) ; end; registration cluster -> ($#v1_card_3 :::"Cardinal-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_card_3 :::"Cardinal-yielding"::: ) ($#v4_card_3 :::"countable"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); :: original: :::"Card"::: redefine func :::"Card"::: "F" -> ($#v1_card_3 :::"Cardinal-yielding"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "F" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set "F" ($#k16_finseq_1 :::"|"::: ) "i") -> ($#v1_card_3 :::"Cardinal-yielding"::: ) ; end; theorem :: PRE_POLY:23 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_3 :::"Card"::: ) (Set "(" (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_card_3 :::"Card"::: ) (Set (Var "F")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))))) ; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k1_card_3 :::"Card"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: PRE_POLY:24 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_card_3 :::"Card"::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "p")) ($#k9_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set "(" ($#k1_card_1 :::"card"::: ) (Set (Var "p")) ")" ) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: PRE_POLY:25 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k1_card_3 :::"Card"::: ) (Set "(" (Set (Var "F")) ($#k7_finseq_1 :::"^"::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_card_3 :::"Card"::: ) (Set (Var "F")) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" ($#k1_card_3 :::"Card"::: ) (Set (Var "G")) ")" )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k6_finseq_1 :::"<*>"::: ) "X") -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) ; end; registrationlet "f" be ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "f" ($#k5_finseq_1 :::"*>"::: ) ) -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) ; end; theorem :: PRE_POLY:26 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_pre_poly :::"FinSequence-yielding"::: ) ) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "y")) "is" ($#m1_hidden :::"FinSequence":::))) ")" )) ; registrationlet "F", "G" be ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "F" ($#k7_finseq_1 :::"^"::: ) "G") -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) ; end; registrationlet "D" be ($#m1_hidden :::"set"::: ) ; let "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "D")) ($#k3_finseq_2 :::"*"::: ) ); cluster (Set ($#k5_pre_poly :::"FlattenSeq"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: PRE_POLY:27 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_pre_poly :::"Card"::: ) (Set (Var "F")) ")" ))))) ; theorem :: PRE_POLY:28 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "E")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k10_pre_poly :::"Card"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k10_pre_poly :::"Card"::: ) (Set (Var "G"))))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "G")) ")" )))))) ; theorem :: PRE_POLY:29 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")) ")" )))) "holds" (Bool "ex" (Set (Var "i")) "," (Set (Var "j")) "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 "F")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ))) & (Bool (Set (Var "k")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_pre_poly :::"Card"::: ) (Set "(" (Set (Var "F")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" ))))) ; theorem :: PRE_POLY:30 (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "D")) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "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 "F")))) & (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_pre_poly :::"Card"::: ) (Set "(" (Set (Var "F")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "j"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k2_wsierp_1 :::"Sum"::: ) (Set "(" ($#k10_pre_poly :::"Card"::: ) (Set "(" (Set (Var "F")) ($#k17_finseq_1 :::"|"::: ) (Set "(" (Set (Var "i")) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" ))) ")" )))) ; theorem :: PRE_POLY:31 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "v")) ")" ) ($#k8_pboole :::"**"::: ) (Set (Var "f"))) "is" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "Y")) ($#k3_finseq_2 :::"*"::: ) ))))) ; theorem :: PRE_POLY:32 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "ex" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Var "Y")) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "v")) ")" ) ($#k8_pboole :::"**"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "v")) ($#k4_finseqop :::"*"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "F")))) ")" ))))) ; begin registrationlet "f" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "n" ")" ) -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; let "n" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "n" ")" ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); :: original: :::"+"::: redefine func "b1" :::"+"::: "b2" -> ($#m1_hidden :::"ManySortedSet":::) "of" "X" means :: PRE_POLY:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "b1" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" "b2" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"+"::: PRE_POLY:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); func "b1" :::"-'"::: "b2" -> ($#m1_hidden :::"ManySortedSet":::) "of" "X" means :: PRE_POLY:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "b1" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" "b2" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))); end; :: deftheorem defines :::"-'"::: PRE_POLY:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b2")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))) ")" )))); theorem :: PRE_POLY:33 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool (Set (Var "b")) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")))))) ; theorem :: PRE_POLY:34 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_nat_d :::"-'"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" )) "holds" (Bool (Set (Var "b")) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b2")))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "X")); cluster (Set "b1" ($#k1_valued_1 :::"+"::: ) "b2") -> ($#v4_valued_0 :::"natural-valued"::: ) ; cluster (Set "b1" ($#k12_pre_poly :::"-'"::: ) "b2") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; theorem :: PRE_POLY:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set (Var "b3"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set "(" (Set (Var "b2")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b3")) ")" ))))) ; theorem :: PRE_POLY:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "b")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "c")) ")" ) ($#k12_pre_poly :::"-'"::: ) (Set (Var "d"))) ($#r6_pboole :::"="::: ) (Set (Set (Var "b")) ($#k12_pre_poly :::"-'"::: ) (Set "(" (Set (Var "c")) ($#k11_pre_poly :::"+"::: ) (Set (Var "d")) ")" ))))) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"support"::: "f" -> ($#m1_hidden :::"set"::: ) means :: PRE_POLY:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )); end; :: deftheorem defines :::"support"::: PRE_POLY:def 7 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ")" ))); theorem :: PRE_POLY:37 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"finite-support"::: means :: PRE_POLY:def 8 (Bool (Set ($#k13_pre_poly :::"support"::: ) "f") "is" ($#v1_finset_1 :::"finite"::: ) ); end; :: deftheorem defines :::"finite-support"::: PRE_POLY:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_pre_poly :::"finite-support"::: ) ) "iff" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "f"))) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) -> ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k13_pre_poly :::"support"::: ) "f") -> ($#v1_finset_1 :::"finite"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," (Set ($#k5_numbers :::"NAT"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "f" be ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "y" ")" ) -> ($#v2_pre_poly :::"finite-support"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: PRE_POLY:38 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b2")) ")" ))))) ; theorem :: PRE_POLY:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "b1")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b2")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b1")))))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode bag of "X" is ($#v4_valued_0 :::"natural-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" "X"; end; registrationlet "X" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) -> ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "b1", "b2" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); cluster (Set "b1" ($#k1_valued_1 :::"+"::: ) "b2") -> ($#v2_pre_poly :::"finite-support"::: ) ; cluster (Set "b1" ($#k12_pre_poly :::"-'"::: ) "b2") -> ($#v2_pre_poly :::"finite-support"::: ) ; end; theorem :: PRE_POLY:40 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "X")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) "is" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "p", "q" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); pred "p" :::"<"::: "q" means :: PRE_POLY:def 9 (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set "q" ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool "(" "for" (Set (Var "l")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Var "k")))) "holds" (Bool (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set "q" ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) ")" ) ")" )); asymmetry (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Const "n")) "st" (Bool (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool "(" "for" (Set (Var "l")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) ")" ) ")" ))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) "or" (Bool "ex" (Set (Var "l")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Var "k"))) & (Bool (Bool "not" (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))))) ")" )) ")" ))) ; end; :: deftheorem defines :::"<"::: PRE_POLY:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_pre_poly :::"<"::: ) (Set (Var "q"))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) & (Bool "(" "for" (Set (Var "l")) "being" ($#m1_hidden :::"Ordinal":::) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) ")" ) ")" )) ")" ))); theorem :: PRE_POLY:41 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "p")) ($#r1_pre_poly :::"<"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r1_pre_poly :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r1_pre_poly :::"<"::: ) (Set (Var "r"))))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "p", "q" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); pred "p" :::"<='"::: "q" means :: PRE_POLY:def 10 (Bool "(" (Bool "p" ($#r1_pre_poly :::"<"::: ) "q") "or" (Bool "p" ($#r6_pboole :::"="::: ) "q") ")" ); reflexivity (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Const "n")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r1_pre_poly :::"<"::: ) (Set (Var "p"))) "or" (Bool (Set (Var "p")) ($#r6_pboole :::"="::: ) (Set (Var "p"))) ")" )) ; end; :: deftheorem defines :::"<='"::: PRE_POLY:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "q"))) "iff" (Bool "(" (Bool (Set (Var "p")) ($#r1_pre_poly :::"<"::: ) (Set (Var "q"))) "or" (Bool (Set (Var "p")) ($#r6_pboole :::"="::: ) (Set (Var "q"))) ")" ) ")" ))); theorem :: PRE_POLY:42 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "p")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "r"))))) ; theorem :: PRE_POLY:43 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "p")) ($#r1_pre_poly :::"<"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r1_pre_poly :::"<"::: ) (Set (Var "r"))))) ; theorem :: PRE_POLY:44 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "p")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "q"))) & (Bool (Set (Var "q")) ($#r1_pre_poly :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "p")) ($#r1_pre_poly :::"<"::: ) (Set (Var "r"))))) ; theorem :: PRE_POLY:45 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "q"))) "or" (Bool (Set (Var "q")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "p"))) ")" ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "d", "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "X")); pred "d" :::"divides"::: "b" means :: PRE_POLY:def 11 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "d" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set "b" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))); reflexivity (Bool "for" (Set (Var "d")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Const "X")) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "d")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "d")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))))) ; end; :: deftheorem defines :::"divides"::: PRE_POLY:def 11 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) "iff" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "d")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))))) ")" ))); theorem :: PRE_POLY:46 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "d")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "b")) ($#k1_funct_1 :::"."::: ) (Set (Var "k")))) ")" )) "holds" (Bool (Set (Var "d")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))))) ; theorem :: PRE_POLY:47 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b2")))) "holds" (Bool (Set (Set "(" (Set (Var "b2")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b1")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set (Var "b1"))) ($#r6_pboole :::"="::: ) (Set (Var "b2"))))) ; theorem :: PRE_POLY:48 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" (Set (Var "b2")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b1")) ")" ) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b1"))) ($#r6_pboole :::"="::: ) (Set (Var "b2"))))) ; theorem :: PRE_POLY:49 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "d")) "," (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "d")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b")))) "holds" (Bool (Set (Var "d")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "b"))))) ; theorem :: PRE_POLY:50 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"Bags"::: "X" -> ($#m1_hidden :::"set"::: ) means :: PRE_POLY:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"bag":::) "of" "X") ")" )); end; :: deftheorem defines :::"Bags"::: PRE_POLY:def 12 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k14_pre_poly :::"Bags"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "x")) "is" ($#m1_hidden :::"bag":::) "of" (Set (Var "X"))) ")" )) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"Bags"::: redefine func :::"Bags"::: "X" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_pre_poly :::"Bags"::: ) "X" ")" ); end; theorem :: PRE_POLY:51 (Bool (Set ($#k15_pre_poly :::"Bags"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k14_pre_poly :::"Bags"::: ) "X") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_funct_1 :::"functional"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "X" ")" )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Const "X")) ")" ); cluster -> "X" ($#v4_relat_1 :::"-defined"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "B"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Const "X")) ")" ); cluster -> ($#v1_partfun1 :::"total"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "B"; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"EmptyBag"::: "X" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) "X") equals :: PRE_POLY:def 13 (Set "X" ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )); end; :: deftheorem defines :::"EmptyBag"::: PRE_POLY:def 13 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))); theorem :: PRE_POLY:52 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: PRE_POLY:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b")) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "b"))))) ; theorem :: PRE_POLY:54 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b")) ($#k12_pre_poly :::"-'"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "b"))))) ; theorem :: PRE_POLY:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b"))) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))))) ; theorem :: PRE_POLY:56 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b"))) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")))))) ; theorem :: PRE_POLY:57 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b1")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b2"))) & (Bool (Set (Set (Var "b2")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "b1"))) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n"))))) "holds" (Bool (Set (Var "b2")) ($#r6_pboole :::"="::: ) (Set (Var "b1"))))) ; theorem :: PRE_POLY:58 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r3_pre_poly :::"divides"::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n"))) ($#r6_pboole :::"="::: ) (Set (Var "b"))))) ; theorem :: PRE_POLY:59 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n"))) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))))) ; theorem :: PRE_POLY:60 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n"))) ($#r2_pre_poly :::"<='"::: ) (Set (Var "b"))))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); func :::"BagOrder"::: "n" -> ($#m1_subset_1 :::"Order":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) means :: PRE_POLY:def 14 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" "n" "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "p")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "q"))) ")" )); end; :: deftheorem defines :::"BagOrder"::: PRE_POLY:def 14 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Order":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k17_pre_poly :::"BagOrder"::: ) (Set (Var "n")))) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "p")) ($#r2_pre_poly :::"<='"::: ) (Set (Var "q"))) ")" )) ")" ))); registrationlet "n" be ($#m1_hidden :::"Ordinal":::); cluster (Set ($#k17_pre_poly :::"BagOrder"::: ) "n") -> ($#v3_orders_1 :::"being_linear-order"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ); func :::"NatMinor"::: "f" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "X" "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ) means :: PRE_POLY:def 15 (Bool "for" (Set (Var "g")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" "X" "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" )); end; :: deftheorem defines :::"NatMinor"::: PRE_POLY:def 15 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k18_pre_poly :::"NatMinor"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "g")) "being" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" )) ")" )))); theorem :: PRE_POLY:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k18_pre_poly :::"NatMinor"::: ) (Set (Var "f")))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k18_pre_poly :::"NatMinor"::: ) "f") -> ($#v4_funct_1 :::"functional"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ); cluster -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k18_pre_poly :::"NatMinor"::: ) "f"); end; theorem :: PRE_POLY:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_pre_poly :::"finite-support"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k18_pre_poly :::"NatMinor"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "X")))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_pre_poly :::"finite-support"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"support"::: redefine func :::"support"::: "f" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X"); end; theorem :: PRE_POLY:63 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_pre_poly :::"finite-support"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k18_pre_poly :::"NatMinor"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k48_binop_2 :::"multnat"::: ) ) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k19_pre_poly :::"support"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set ($#k47_binop_2 :::"addnat"::: ) ) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Num 1) ")" ")" ) ")" )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_pre_poly :::"finite-support"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set ($#k18_pre_poly :::"NatMinor"::: ) "f") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); func :::"divisors"::: "b" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) "n") means :: PRE_POLY:def 16 (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k17_pre_poly :::"BagOrder"::: ) "n" ")" ) "," (Set (Var "S")) ")" )) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" "n" "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) "iff" (Bool (Set (Var "p")) ($#r3_pre_poly :::"divides"::: ) "b") ")" ) ")" ) ")" )); end; :: deftheorem defines :::"divisors"::: PRE_POLY:def 16 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k7_pre_poly :::"SgmX"::: ) "(" (Set "(" ($#k17_pre_poly :::"BagOrder"::: ) (Set (Var "n")) ")" ) "," (Set (Var "S")) ")" )) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))) "iff" (Bool (Set (Var "p")) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b"))) ")" ) ")" ) ")" )) ")" )))); registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); cluster (Set ($#k20_pre_poly :::"divisors"::: ) "b") -> ($#v2_funct_1 :::"one-to-one"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: PRE_POLY:64 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" )))) "holds" (Bool (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r3_pre_poly :::"divides"::: ) (Set (Var "b")))))) ; theorem :: PRE_POLY:65 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r6_pboole :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ) ")" )) ($#r6_pboole :::"="::: ) (Set (Var "b"))) ")" ))) ; theorem :: PRE_POLY:66 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")))) & (Bool (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) ")" )))) ; theorem :: PRE_POLY:67 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k20_pre_poly :::"divisors"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) ($#k3_pre_poly :::"*>"::: ) ))) ; definitionlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); func :::"decomp"::: "b" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) "n" ")" )) means :: PRE_POLY:def 17 (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) "b" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" "n" "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it)) & (Bool (Set (Var "p")) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) "b" ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))) "holds" (Bool (Set it ($#k9_pre_poly :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "p")) "," (Set "(" "b" ($#k12_pre_poly :::"-'"::: ) (Set (Var "p")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) ")" ) ")" ); end; :: deftheorem defines :::"decomp"::: PRE_POLY:def 17 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")))) "iff" (Bool "(" (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3")))) & (Bool (Set (Var "p")) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k9_pre_poly :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "p")) "," (Set "(" (Set (Var "b")) ($#k12_pre_poly :::"-'"::: ) (Set (Var "p")) ")" ) ($#k10_finseq_1 :::"*>"::: ) ))) ")" ) ")" ) ")" )))); theorem :: PRE_POLY:68 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" )))) "holds" (Bool "ex" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool "(" (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Var "b")) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")))) ")" ))))) ; theorem :: PRE_POLY:69 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "b")) ($#r6_pboole :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2"))))) "holds" (Bool "ex" (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 "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k10_finseq_1 :::"*>"::: ) )) ")" )))) ; theorem :: PRE_POLY:70 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool (Set (Var "b1")) ($#r6_pboole :::"="::: ) (Set (Set "(" ($#k20_pre_poly :::"divisors"::: ) (Set (Var "b")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))))))) ; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "n")); cluster (Set ($#k21_pre_poly :::"decomp"::: ) "b") -> ($#v2_funct_1 :::"one-to-one"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_pre_poly :::"FinSequence-yielding"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Ordinal":::); let "b" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) (Set (Const "n"))); cluster (Set ($#k21_pre_poly :::"decomp"::: ) "b") -> ($#v2_funct_1 :::"one-to-one"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_pre_poly :::"FinSequence-yielding"::: ) ; end; theorem :: PRE_POLY:71 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) "," (Set (Var "b")) ($#k10_finseq_1 :::"*>"::: ) )) & (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b")) "," (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) ($#k10_finseq_1 :::"*>"::: ) )) ")" ))) ; theorem :: PRE_POLY:72 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">"::: ) (Num 1)) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b1")) "," (Set (Var "b2")) ($#k10_finseq_1 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"<>"::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"<>"::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")))) ")" )))) ; theorem :: PRE_POLY:73 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) "holds" (Bool (Set ($#k21_pre_poly :::"decomp"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "n")) ")" ) ($#k4_pre_poly :::"*>"::: ) ) ($#k3_pre_poly :::"*>"::: ) ))) ; theorem :: PRE_POLY:74 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Ordinal":::) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "n")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "(" (Num 3) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k15_pre_poly :::"Bags"::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) "st" (Bool (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ))) & (Bool (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set "(" (Set "(" (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "k")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k8_pre_poly :::"^^"::: ) (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set "(" (Set "(" (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "k")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" (Set "(" (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "k")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ($#k3_pre_poly :::"*>"::: ) ) ")" ))) ")" ) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set "(" (Set "(" (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "k")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set ($#k3_pre_poly :::"<*"::: ) (Set "(" (Set "(" (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "k")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k3_pre_poly :::"*>"::: ) ) ")" ) ($#k8_pre_poly :::"^^"::: ) (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set "(" (Set "(" (Set "(" ($#k21_pre_poly :::"decomp"::: ) (Set (Var "b")) ")" ) ($#k9_pre_poly :::"/."::: ) (Set (Var "k")) ")" ) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ))) ")" )) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "f")) ")" ) ")" ) "st" (Bool (Set ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "p")))))))) ; theorem :: PRE_POLY:75 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "X")) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b2")) ")" ))))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; registrationlet "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "k")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "D"))); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "M" ($#k7_partfun1 :::"/."::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set (Const "k")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "D"))); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "M" ($#k7_partfun1 :::"/."::: ) "x") -> "D" ($#v5_relat_1 :::"-valued"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end;