:: UPROOTS semantic presentation begin theorem :: UPROOTS:1 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m2_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"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Num 1))) ")" )) ; scheme :: UPROOTS:sch 1 IndFinSeq0{ F1() -> ($#m1_hidden :::"Nat":::), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "i"))])) provided (Bool P1[(Num 1)]) and (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "i"))])) "holds" (Bool P1[(Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1))])) proof end; theorem :: UPROOTS:2 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::">="::: ) (Num 2)) & (Bool "(" "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 2) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Set (Var "r")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ))))) ; begin registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) "A" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v2_pre_poly :::"finite-support"::: ) for ($#m1_finseq_1 :::"FinSequence"::: ) "of" "A"; end; definitionlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; func :::"canFS"::: "A" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "A" equals :: UPROOTS:def 1 "the" ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" "A"; end; :: deftheorem defines :::"canFS"::: UPROOTS:def 1 : (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_uproots :::"canFS"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) "the" ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "A")))); registrationlet "A" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_uproots :::"canFS"::: ) "A") -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ; end; theorem :: UPROOTS:3 (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "A"))))) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_uproots :::"canFS"::: ) "A") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: UPROOTS:4 (Bool "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_uproots :::"canFS"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k9_finseq_1 :::"*>"::: ) ))) ; theorem :: UPROOTS:5 (Bool "for" (Set (Var "A")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k1_uproots :::"canFS"::: ) (Set (Var "A")) ")" ) ($#k2_funct_1 :::"""::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "A")) ")" ) ")" ))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "X")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func "(" "S" "," "n" ")" :::"-bag"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k15_pre_poly :::"Bags"::: ) "X") equals :: UPROOTS:def 2 (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) "X" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "S" ($#k8_funcop_1 :::"-->"::: ) "n" ")" )); end; :: deftheorem defines :::"-bag"::: UPROOTS:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set "(" (Set (Var "S")) "," (Set (Var "n")) ")" ($#k2_uproots :::"-bag"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "S")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "n")) ")" )))))); theorem :: UPROOTS:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set "(" "(" (Set (Var "S")) "," (Set (Var "n")) ")" ($#k2_uproots :::"-bag"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))))) ; theorem :: UPROOTS:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "S")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "S")) "," (Set (Var "n")) ")" ($#k2_uproots :::"-bag"::: ) ")" ) ($#k1_recdef_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))))) ; theorem :: UPROOTS:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set "(" "(" (Set (Var "S")) "," (Set (Var "n")) ")" ($#k2_uproots :::"-bag"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "S")))))) ; theorem :: UPROOTS:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Var "S")) "is" ($#v1_xboole_0 :::"empty"::: ) ) "or" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set "(" (Set (Var "S")) "," (Set (Var "n")) ")" ($#k2_uproots :::"-bag"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "X"))))))) ; theorem :: UPROOTS:10 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "T")))) "holds" (Bool (Set "(" (Set "(" (Set (Var "S")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "T")) ")" ) "," (Set (Var "n")) ")" ($#k2_uproots :::"-bag"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "S")) "," (Set (Var "n")) ")" ($#k2_uproots :::"-bag"::: ) ")" ) ($#k11_pre_poly :::"+"::: ) (Set "(" "(" (Set (Var "T")) "," (Set (Var "n")) ")" ($#k2_uproots :::"-bag"::: ) ")" )))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Rbag of "X" is ($#v3_valued_0 :::"real-valued"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#m1_hidden :::"ManySortedSet":::) "of" "X"; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"Rbag":::) "of" (Set (Const "A")); func :::"Sum"::: "b" -> ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) means :: UPROOTS:def 3 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "b" ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) "b" ")" ) ")" ))) ")" )); end; :: deftheorem defines :::"Sum"::: UPROOTS:def 3 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ) ")" ))) ")" )) ")" )))); notationlet "A" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "A")); synonym :::"degree"::: "b" for :::"Sum"::: "b"; end; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "b" be ($#m1_hidden :::"bag":::) "of" (Set (Const "A")); :: original: :::"Sum"::: redefine func :::"degree"::: "b" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: UPROOTS:def 4 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "b" ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) "b" ")" ) ")" ))) ")" )); end; :: deftheorem defines :::"degree"::: UPROOTS:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b3")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_uproots :::"degree"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k2_wsierp_1 :::"Sum"::: ) (Set (Var "f")))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ) ")" ))) ")" )) ")" )))); theorem :: UPROOTS:11 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "A"))))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: UPROOTS:12 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set ($#k16_pre_poly :::"EmptyBag"::: ) (Set (Var "A")))))) ; theorem :: UPROOTS:13 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set (Var "A")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b")))) & (Bool (Set ($#k4_uproots :::"degree"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "S")))) ")" ) "iff" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "S")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) )) ")" )))) ; theorem :: UPROOTS:14 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set (Var "S")))) "holds" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_uproots :::"canFS"::: ) (Set (Var "S")) ")" ))) & (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set (Var "f")))) ")" ))))) ; theorem :: UPROOTS:15 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Rbag":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2"))))) "holds" (Bool (Set ($#k3_uproots :::"Sum"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_uproots :::"Sum"::: ) (Set (Var "b1")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k3_uproots :::"Sum"::: ) (Set (Var "b2")) ")" ))))) ; theorem :: UPROOTS:16 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#l3_algstr_0 :::"multMagma"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f"))))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); attr "p" is :::"non-zero"::: means :: UPROOTS:def 5 (Bool "p" ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) "L")); end; :: deftheorem defines :::"non-zero"::: UPROOTS:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_uproots :::"non-zero"::: ) ) "iff" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) ")" ))); theorem :: UPROOTS:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_uproots :::"non-zero"::: ) ) "iff" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ))) ; registrationlet "L" be ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v1_algseq_1 :::"finite-Support"::: ) ($#v1_uproots :::"non-zero"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); cluster (Set ($#k4_polynom5 :::"<%"::: ) "x" "," (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" ) ($#k4_polynom5 :::"%>"::: ) ) -> ($#v1_uproots :::"non-zero"::: ) ; end; theorem :: UPROOTS:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))) ; theorem :: UPROOTS:19 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) & (Bool (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ))) ; theorem :: UPROOTS:20 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"unital"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#v2_polynom5 :::"algebraic-closed"::: ) for ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; end; theorem :: UPROOTS:21 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" "not" (Bool (Set (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) "or" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) "or" (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) ")" ))) ; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; cluster (Set ($#k14_polynom3 :::"Polynom-Ring"::: ) "L") -> ($#v1_vectsp_2 :::"domRing-like"::: ) ; end; registrationlet "L" be ($#l6_algstr_0 :::"domRing":::); let "p", "q" be ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set "p" ($#k11_polynom3 :::"*'"::: ) "q") -> ($#v1_uproots :::"non-zero"::: ) ; end; theorem :: UPROOTS:22 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" ($#k6_polynom5 :::"Roots"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_polynom5 :::"Roots"::: ) (Set (Var "q")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k6_polynom5 :::"Roots"::: ) (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ))))) ; theorem :: UPROOTS:23 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_polynom5 :::"Roots"::: ) (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_polynom5 :::"Roots"::: ) (Set (Var "p")) ")" ) ($#k4_subset_1 :::"\/"::: ) (Set "(" ($#k6_polynom5 :::"Roots"::: ) (Set (Var "q")) ")" ))))) ; theorem :: UPROOTS:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "pc")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "pc")))) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "pc"))))))) ; theorem :: UPROOTS:25 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "pc")) "," (Set (Var "qc")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "pc"))) & (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Var "qc")))) "holds" (Bool (Set (Set (Var "p")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "pc")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "qc"))))))) ; theorem :: UPROOTS:26 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "r")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set "(" (Set (Var "q")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "r")) ")" ))))) ; theorem :: UPROOTS:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k3_normsp_1 :::"-"::: ) (Set (Var "q"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Var "q"))))) ; theorem :: UPROOTS:28 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) & (Bool (Set (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "r"))))) "holds" (Bool (Set (Var "q")) ($#r2_funct_2 :::"="::: ) (Set (Var "r"))))) ; theorem :: UPROOTS:29 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set (Var "n"))) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))))) ; theorem :: UPROOTS:30 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set (Var "i")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set (Var "j")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k2_polynom5 :::"`^"::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "j")) ")" )))))) ; theorem :: UPROOTS:31 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) "holds" (Bool (Set ($#k10_polynom3 :::"1_."::: ) (Set (Var "L"))) ($#r2_funct_2 :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k3_algseq_1 :::"%>"::: ) ))) ; theorem :: UPROOTS:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))))) ; theorem :: UPROOTS:33 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool "(" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: UPROOTS:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q"))) "is" ($#v1_uproots :::"non-zero"::: ) )) "holds" (Bool "(" (Bool (Set (Var "p")) "is" ($#v1_uproots :::"non-zero"::: ) ) & (Bool (Set (Var "q")) "is" ($#v1_uproots :::"non-zero"::: ) ) ")" ))) ; theorem :: UPROOTS:35 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set (Var "q")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ))))) ; theorem :: UPROOTS:36 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v1_vectsp_2 :::"domRing-like"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set (Var "p")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ))))) ; theorem :: UPROOTS:37 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Set "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_polynom5 :::"%>"::: ) ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_polynom5 :::"%>"::: ) ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p")) ")" ) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set (Var "p")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ))) ")" ) ")" )))) ; theorem :: UPROOTS:38 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "r")) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; theorem :: UPROOTS:39 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "x")) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k2_polynom5 :::"`^"::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)))))) ; registrationlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set (Set ($#k4_polynom5 :::"<%"::: ) "x" "," (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k2_polynom5 :::"`^"::: ) "n") -> ($#v1_uproots :::"non-zero"::: ) ; end; theorem :: UPROOTS:40 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "q")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" (Set "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "x")) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k2_polynom5 :::"`^"::: ) (Set (Var "i")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ))))))) ; theorem :: UPROOTS:41 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_group_1 :::"associative"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k4_polynom5 :::"<%"::: ) (Set (Var "r")) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "q")))) & (Bool (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Set (Var "q")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L"))))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) ; let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); let "n" be ($#m1_hidden :::"Nat":::); func :::"poly_shift"::: "(" "p" "," "n" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" means :: UPROOTS:def 6 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set "p" ($#k8_nat_1 :::"."::: ) (Set "(" "n" ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"poly_shift"::: UPROOTS:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_uproots :::"poly_shift"::: ) "(" (Set (Var "p")) "," (Set (Var "n")) ")" )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "i")) ")" )))) ")" ))))); theorem :: UPROOTS:42 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_uproots :::"poly_shift"::: ) "(" (Set (Var "p")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))))) ; theorem :: UPROOTS:43 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_struct_0 :::"ZeroStr"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k5_uproots :::"poly_shift"::: ) "(" (Set (Var "p")) "," (Set (Var "n")) ")" ) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))))) ; theorem :: UPROOTS:44 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l5_algstr_0 :::"multLoopStr_0"::: ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k5_uproots :::"poly_shift"::: ) "(" (Set (Var "p")) "," (Set (Var "n")) ")" ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))))))) ; theorem :: UPROOTS:45 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uproots :::"poly_shift"::: ) "(" (Set (Var "p")) "," (Set (Var "n")) ")" ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k8_group_1 :::"*"::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uproots :::"poly_shift"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set (Var "x")) ")" ")" ) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set (Var "n")) ")" ))))))) ; theorem :: UPROOTS:46 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k6_polynom5 :::"Roots"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; definitionlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::); let "r" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "p" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); assume (Bool (Set (Const "r")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Const "p"))) ; func :::"poly_quotient"::: "(" "p" "," "r" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" means :: UPROOTS:def 7 (Bool "(" (Bool (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) it ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) "p")) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uproots :::"poly_shift"::: ) "(" "p" "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," "r" ")" )) ")" ) ")" ) if (Bool (Set ($#k1_algseq_1 :::"len"::: ) "p") ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) otherwise (Bool it ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) "L")); end; :: deftheorem defines :::"poly_quotient"::: UPROOTS:def 7 : (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "r")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_uproots :::"poly_quotient"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" )) "iff" (Bool "(" (Bool (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "b4")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k5_uproots :::"poly_shift"::: ) "(" (Set (Var "p")) "," (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) "," (Set (Var "r")) ")" )) ")" ) ")" ) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_uproots :::"poly_quotient"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" )) "iff" (Bool (Set (Var "b4")) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) ")" ) ")" ")" ))))); theorem :: UPROOTS:47 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "r")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set "(" ($#k6_uproots :::"poly_quotient"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: UPROOTS:48 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k6_polynom5 :::"Roots"::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) )))) ; theorem :: UPROOTS:49 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))))) ; theorem :: UPROOTS:50 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "r")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))) "holds" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k13_polynom3 :::"*'"::: ) (Set "(" ($#k6_uproots :::"poly_quotient"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" )))))) ; theorem :: UPROOTS:51 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Var "r")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))))) ; begin registrationlet "L" be ($#l6_algstr_0 :::"domRing":::); let "p" be ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); cluster (Set ($#k6_polynom5 :::"Roots"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "L" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "p" be ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func :::"multiplicity"::: "(" "p" "," "x" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: UPROOTS:def 8 (Bool "ex" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "L" "st" (Bool "p" ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) "x" ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k2_polynom5 :::"`^"::: ) (Set (Var "k")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q"))))) "}" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "F")))) ")" )); end; :: deftheorem defines :::"multiplicity"::: UPROOTS:def 8 : (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b4")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k7_uproots :::"multiplicity"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" )) "iff" (Bool "ex" (Set (Var "F")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k2_polynom5 :::"`^"::: ) (Set (Var "k")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q"))))) "}" ) & (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set (Var "F")))) ")" )) ")" ))))); theorem :: UPROOTS:52 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "p")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p"))) "iff" (Bool (Set ($#k7_uproots :::"multiplicity"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Num 1)) ")" )))) ; theorem :: UPROOTS:53 (Bool "for" (Set (Var "L")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_uproots :::"multiplicity"::: ) "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)))) ; definitionlet "L" be ($#l6_algstr_0 :::"domRing":::); let "p" be ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func :::"BRoots"::: "p" -> ($#m1_hidden :::"bag":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "L") means :: UPROOTS:def 9 (Bool "(" (Bool (Set ($#k13_pre_poly :::"support"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k6_polynom5 :::"Roots"::: ) "p")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "L" "holds" (Bool (Set it ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_uproots :::"multiplicity"::: ) "(" "p" "," (Set (Var "x")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"BRoots"::: UPROOTS:def 9 : (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "p")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"bag":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_uproots :::"BRoots"::: ) (Set (Var "p")))) "iff" (Bool "(" (Bool (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k6_polynom5 :::"Roots"::: ) (Set (Var "p")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_recdef_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_uproots :::"multiplicity"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" )) ")" ) ")" ) ")" )))); theorem :: UPROOTS:54 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k8_uproots :::"BRoots"::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) )) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x")) ($#k6_domain_1 :::"}"::: ) ) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) )))) ; theorem :: UPROOTS:55 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k7_uproots :::"multiplicity"::: ) "(" (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_uproots :::"multiplicity"::: ) "(" (Set (Var "p")) "," (Set (Var "x")) ")" ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k7_uproots :::"multiplicity"::: ) "(" (Set (Var "q")) "," (Set (Var "x")) ")" ")" )))))) ; theorem :: UPROOTS:56 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k8_uproots :::"BRoots"::: ) (Set "(" (Set (Var "p")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "q")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k8_uproots :::"BRoots"::: ) (Set (Var "p")) ")" ) ($#k11_pre_poly :::"+"::: ) (Set "(" ($#k8_uproots :::"BRoots"::: ) (Set (Var "q")) ")" ))))) ; theorem :: UPROOTS:57 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "p")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k1_algseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1))) "holds" (Bool (Set ($#k4_uproots :::"degree"::: ) (Set "(" ($#k8_uproots :::"BRoots"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: UPROOTS:58 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k4_uproots :::"degree"::: ) (Set "(" ($#k8_uproots :::"BRoots"::: ) (Set "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k2_polynom5 :::"`^"::: ) (Set (Var "n")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "n")))))) ; theorem :: UPROOTS:59 (Bool "for" (Set (Var "L")) "being" ($#v2_polynom5 :::"algebraic-closed"::: ) ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "p")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k4_uproots :::"degree"::: ) (Set "(" ($#k8_uproots :::"BRoots"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1))))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "c" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"fpoly_mult_root"::: "(" "c" "," "n" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) "L" ")" ) means :: UPROOTS:def 10 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) "n") & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) "c" ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) "L" ")" ) ($#k4_polynom5 :::"%>"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"fpoly_mult_root"::: UPROOTS:def 10 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k9_uproots :::"fpoly_mult_root"::: ) "(" (Set (Var "c")) "," (Set (Var "n")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "c")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) )) ")" ) ")" ) ")" ))))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "b" be ($#m1_hidden :::"bag":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "L"))); func :::"poly_with_roots"::: "b" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" means :: UPROOTS:def 11 (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) "L" ")" )) ($#k3_finseq_2 :::"*"::: ) )(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" "L" "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) "b" ")" ))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) "b" ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_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"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k9_uproots :::"fpoly_mult_root"::: ) "(" (Set "(" (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" "b" ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ")" )) ")" ) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "f")) ")" ))) ")" ))); end; :: deftheorem defines :::"poly_with_roots"::: UPROOTS:def 11 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set (Var "b")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" )) ($#k3_finseq_2 :::"*"::: ) )(Bool "ex" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_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"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k9_uproots :::"fpoly_mult_root"::: ) "(" (Set "(" (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ")" )) ")" ) & (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "f")) ")" ))) ")" ))) ")" )))); theorem :: UPROOTS:60 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_group_1 :::"commutative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) "holds" (Bool (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" ($#k16_pre_poly :::"EmptyBag"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_algseq_1 :::"<%"::: ) (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k3_algseq_1 :::"%>"::: ) ))) ; theorem :: UPROOTS:61 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" "(" (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "c")) ($#k6_domain_1 :::"}"::: ) ) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "c")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) )))) ; theorem :: UPROOTS:62 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" )) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_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"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k9_uproots :::"fpoly_mult_root"::: ) "(" (Set "(" (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ")" )) ")" )) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_uproots :::"degree"::: ) (Set (Var "b")))))))) ; theorem :: UPROOTS:63 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "b")) "being" ($#m1_hidden :::"bag":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" )) ($#k3_finseq_2 :::"*"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k1_uproots :::"canFS"::: ) (Set "(" ($#k13_pre_poly :::"support"::: ) (Set (Var "b")) ")" ))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_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"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k9_uproots :::"fpoly_mult_root"::: ) "(" (Set "(" (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "b")) ($#k1_recdef_1 :::"."::: ) (Set "(" (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ")" )) ")" )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b"))))) "implies" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "f")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "c")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k1_recdef_1 :::"."::: ) (Set (Var "c")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k13_pre_poly :::"support"::: ) (Set (Var "b")))))) "implies" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" (Set "(" ($#k5_pre_poly :::"FlattenSeq"::: ) (Set (Var "f")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "c")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" )))))) ; theorem :: UPROOTS:64 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"bag":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "L"))) "holds" (Bool (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" (Set (Var "b1")) ($#k11_pre_poly :::"+"::: ) (Set (Var "b2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k10_uproots :::"poly_with_roots"::: ) (Set (Var "b1")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set "(" ($#k10_uproots :::"poly_with_roots"::: ) (Set (Var "b2")) ")" ))))) ; theorem :: UPROOTS:65 (Bool "for" (Set (Var "L")) "being" ($#v2_polynom5 :::"algebraic-closed"::: ) ($#l6_algstr_0 :::"domRing":::) (Bool "for" (Set (Var "p")) "being" ($#v1_uproots :::"non-zero"::: ) ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set "(" (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k7_nat_d :::"-'"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_struct_0 :::"1."::: ) (Set (Var "L"))))) "holds" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" ($#k8_uproots :::"BRoots"::: ) (Set (Var "p")) ")" ))))) ; theorem :: UPROOTS:66 (Bool "for" (Set (Var "L")) "being" ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "s")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_uproots :::"canFS"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "c")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ))) ")" )) "holds" (Bool (Set ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" "(" (Set (Var "s")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f"))))))) ; theorem :: UPROOTS:67 (Bool "for" (Set (Var "L")) "being" ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#l6_algstr_0 :::"comRing":::) (Bool "for" (Set (Var "s")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "s")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_uproots :::"canFS"::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set ($#k4_polynom5 :::"<%"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "c")) ")" ) "," (Set "(" ($#k5_struct_0 :::"1."::: ) (Set (Var "L")) ")" ) ($#k4_polynom5 :::"%>"::: ) ) "," (Set (Var "x")) ")" ))) ")" )) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k10_uproots :::"poly_with_roots"::: ) (Set "(" "(" (Set (Var "s")) "," (Num 1) ")" ($#k2_uproots :::"-bag"::: ) ")" ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_group_4 :::"Product"::: ) (Set (Var "f")))))))) ;