:: HURWITZ semantic presentation begin theorem :: HURWITZ:1 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k11_algstr_0 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k11_algstr_0 :::"""::: ) )))) ; theorem :: HURWITZ:2 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#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 "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ) ")" ) "," (Set (Var "k")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))))) ; theorem :: HURWITZ:3 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l4_algstr_0 :::"multLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "k1")) "," (Set (Var "k2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "k1")) ")" ")" ) ($#k6_algstr_0 :::"*"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "k2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "k1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k2")) ")" ) ")" ))))) ; theorem :: HURWITZ:4 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#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 "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ) ")" ) "," (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "L")))) & (Bool (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ) ")" ) "," (Set "(" (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "k")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ))) ")" ))) ; theorem :: HURWITZ:5 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "k")) ")" ")" ) ($#k2_complfld :::"*'"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "z")) ($#k2_complfld :::"*'"::: ) ")" ) "," (Set (Var "k")) ")" )))) ; theorem :: HURWITZ:6 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "G"))))) "holds" (Bool (Set (Set (Var "G")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k2_complfld :::"*'"::: ) )) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "G"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" ) ($#k2_complfld :::"*'"::: ) ))) ; theorem :: HURWITZ:7 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F2")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Set (Var "F1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "F2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ))) ")" )) "holds" (Bool (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F2")) ")" ))))) ; theorem :: HURWITZ:8 (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 "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k6_algstr_0 :::"*"::: ) (Set "(" ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" (Set (Var "x")) ($#k9_fvsum_1 :::"*"::: ) (Set (Var "F")) ")" )))))) ; begin theorem :: HURWITZ:9 (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"::: ) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) ; theorem :: HURWITZ:10 (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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "p"))))) ; theorem :: HURWITZ:11 (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 "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "p1")) ($#k8_polynom3 :::"+"::: ) (Set (Var "p2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k8_polynom3 :::"+"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p2")) ")" ))))) ; theorem :: HURWITZ:12 (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 "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "p1")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p1")) ")" ) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p2")))) & (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "p1")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p1")) ($#k11_polynom3 :::"*'"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p2")) ")" ))) ")" ))) ; 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 "F" be ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Const "L")) ")" ); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Coeff"::: "(" "F" "," "i" ")" -> ($#m2_finseq_1 :::"FinSequence":::) "of" "L" means :: HURWITZ:def 1 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "F")) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "L" "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) "i")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Coeff"::: HURWITZ:def 1 : (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 "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k1_hurwitz :::"Coeff"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")))) & (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i")))) ")" )) ")" ) ")" ) ")" ))))); theorem :: HURWITZ:13 (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 "F")) "being" ($#m2_finseq_1 :::"FinSequence":::) "of" (Set "(" ($#k14_polynom3 :::"Polynom-Ring"::: ) (Set (Var "L")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "p")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_rlvect_1 :::"Sum"::: ) (Set "(" ($#k1_hurwitz :::"Coeff"::: ) "(" (Set (Var "F")) "," (Set (Var "i")) ")" ")" ))))))) ; theorem :: HURWITZ:14 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v3_group_1 :::"associative"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x1")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "x2")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k6_algstr_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "p"))))))) ; theorem :: HURWITZ:15 (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 "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "p"))))))) ; theorem :: HURWITZ:16 (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")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "p")) ")" )))))) ; theorem :: HURWITZ:17 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_vectsp_1 :::"left-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set "(" (Set (Var "x1")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "p"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p")) ")" )))))) ; theorem :: HURWITZ:18 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_vectsp_1 :::"right-distributive"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "p2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p1")) ")" ) ($#k2_normsp_1 :::"+"::: ) (Set "(" (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p2")) ")" )))))) ; theorem :: HURWITZ:19 (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"::: ) ($#v5_vectsp_1 :::"distributive"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p1")) ($#k11_polynom3 :::"*'"::: ) (Set "(" (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set (Var "p2")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "p1")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p2")) ")" )))))) ; 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")); func :::"degree"::: "p" -> ($#m1_hidden :::"Integer":::) equals :: HURWITZ:def 2 (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) "p" ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)); end; :: deftheorem defines :::"degree"::: HURWITZ:def 2 : (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 ($#k2_hurwitz :::"degree"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_algseq_1 :::"len"::: ) (Set (Var "p")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))))); notationlet "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")); synonym :::"deg"::: "p" for :::"degree"::: "p"; end; theorem :: HURWITZ:20 (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 ($#k2_hurwitz :::"deg"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 1))) "iff" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) ")" ))) ; theorem :: HURWITZ:21 (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 "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "p1"))) ($#r1_hidden :::"<>"::: ) (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "p2"))))) "holds" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set "(" (Set (Var "p1")) ($#k2_normsp_1 :::"+"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k2_hurwitz :::"deg"::: ) (Set (Var "p1")) ")" ) "," (Set "(" ($#k2_hurwitz :::"deg"::: ) (Set (Var "p2")) ")" ) ")" )))) ; theorem :: HURWITZ:22 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set "(" (Set (Var "p1")) ($#k8_polynom3 :::"+"::: ) (Set (Var "p2")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k2_hurwitz :::"deg"::: ) (Set (Var "p1")) ")" ) "," (Set "(" ($#k2_hurwitz :::"deg"::: ) (Set (Var "p2")) ")" ) ")" )))) ; theorem :: HURWITZ:23 (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 "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p1")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) & (Bool (Set (Var "p2")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) "holds" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set "(" (Set (Var "p1")) ($#k11_polynom3 :::"*'"::: ) (Set (Var "p2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_hurwitz :::"deg"::: ) (Set (Var "p1")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k2_hurwitz :::"deg"::: ) (Set (Var "p2")) ")" ))))) ; theorem :: HURWITZ:24 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v1_group_1 :::"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")) "st" (Bool (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "not" (Bool (Set (Var "p")) "is" ($#v1_polynom5 :::"with_roots"::: ) )))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "k" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"rpoly"::: "(" "k" "," "z" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" equals :: HURWITZ:def 3 (Set (Set "(" ($#k9_polynom3 :::"0_."::: ) "L" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," "k" ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) "L" ")" ) ($#k2_binop_1 :::"."::: ) "(" "z" "," "k" ")" ")" ) ")" ) "," (Set "(" ($#k1_group_1 :::"1_"::: ) "L" ")" ) ")" ")" )); end; :: deftheorem defines :::"rpoly"::: HURWITZ:def 3 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "k")) ")" ($#k5_funct_4 :::"-->"::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "k")) ")" ")" ) ")" ) "," (Set "(" ($#k1_group_1 :::"1_"::: ) (Set (Var "L")) ")" ) ")" ")" )))))); theorem :: HURWITZ:25 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" ")" ) ($#k1_normsp_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "k")) ")" ")" ))) & (Bool (Set (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set ($#k1_group_1 :::"1_"::: ) (Set (Var "L")))) ")" )))) ; theorem :: HURWITZ:26 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_group_1 :::"unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" ")" ) ($#k1_normsp_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L"))))))) ; theorem :: HURWITZ:27 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "k")))))) ; theorem :: HURWITZ:28 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#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")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Num 1)) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) & (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ")" ))) ")" )) ")" ))) ; theorem :: HURWITZ:29 (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "z")))))) ; theorem :: HURWITZ:30 (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"::: ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "holds" (Bool (Set (Var "z")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" )))) ; definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) ; let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "L")); let "k" be ($#m1_hidden :::"Nat":::); func :::"qpoly"::: "(" "k" "," "z" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" means :: HURWITZ:def 4 (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) "k")) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) "L" ")" ) ($#k1_binop_1 :::"."::: ) "(" "z" "," (Set "(" (Set "(" "k" ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) "k")) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "L")) ")" ) ")" ); end; :: deftheorem defines :::"qpoly"::: HURWITZ:def 4 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "k")) "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 ($#k4_hurwitz :::"qpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_group_1 :::"power"::: ) (Set (Var "L")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set "(" (Set "(" (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::">="::: ) (Set (Var "k")))) "holds" (Bool (Set (Set (Var "b4")) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "L")))) ")" ) ")" ) ")" ))))); theorem :: HURWITZ:31 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v4_vectsp_1 :::"well-unital"::: ) ($#l6_algstr_0 :::"doubleLoopStr"::: ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set "(" ($#k4_hurwitz :::"qpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "k")) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))))) ; theorem :: HURWITZ:32 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v5_group_1 :::"commutative"::: ) ($#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 "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Num 1))) "holds" (Bool (Set (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ")" ) ($#k11_polynom3 :::"*'"::: ) (Set "(" ($#k4_hurwitz :::"qpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Set (Var "k")) "," (Set (Var "z")) ")" ))))) ; theorem :: HURWITZ:33 (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"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#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 "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))) "holds" (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "s")))))))) ; begin definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) ; let "p", "s" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); assume (Bool (Set (Const "s")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Const "L")))) ; func "p" :::"div"::: "s" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" means :: HURWITZ:def 5 (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" "L" "st" (Bool "(" (Bool "p" ($#r2_funct_2 :::"="::: ) (Set (Set "(" it ($#k13_polynom3 :::"*'"::: ) "s" ")" ) ($#k8_polynom3 :::"+"::: ) (Set (Var "t")))) & (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "t"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_hurwitz :::"deg"::: ) "s")) ")" )); end; :: deftheorem defines :::"div"::: HURWITZ:def 5 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k5_hurwitz :::"div"::: ) (Set (Var "s")))) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool "(" (Bool (Set (Var "p")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "b4")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "s")) ")" ) ($#k8_polynom3 :::"+"::: ) (Set (Var "t")))) & (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "t"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "s")))) ")" )) ")" )))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) ; let "p", "s" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); func "p" :::"mod"::: "s" -> ($#m1_subset_1 :::"Polynomial":::) "of" "L" equals :: HURWITZ:def 6 (Set "p" ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set "(" "p" ($#k5_hurwitz :::"div"::: ) "s" ")" ) ($#k13_polynom3 :::"*'"::: ) "s" ")" )); end; :: deftheorem defines :::"mod"::: HURWITZ:def 6 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool (Set (Set (Var "p")) ($#k6_hurwitz :::"mod"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k5_hurwitz :::"div"::: ) (Set (Var "s")) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set (Var "s")) ")" ))))); definitionlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) ; let "p", "s" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Const "L")); pred "s" :::"divides"::: "p" means :: HURWITZ:def 7 (Bool (Set "p" ($#k6_hurwitz :::"mod"::: ) "s") ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) "L")); end; :: deftheorem defines :::"divides"::: HURWITZ:def 7 : (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r1_hurwitz :::"divides"::: ) (Set (Var "p"))) "iff" (Bool (Set (Set (Var "p")) ($#k6_hurwitz :::"mod"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) ")" ))); theorem :: HURWITZ:34 (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L"))))) "holds" (Bool "(" (Bool (Set (Var "s")) ($#r1_hurwitz :::"divides"::: ) (Set (Var "p"))) "iff" (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) "st" (Bool (Set (Set (Var "t")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set (Var "p")))) ")" ))) ; theorem :: HURWITZ:35 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "z")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ) ($#r1_hurwitz :::"divides"::: ) (Set (Var "p")))))) ; theorem :: HURWITZ:36 (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"::: ) ($#v33_algstr_0 :::"almost_left_invertible"::: ) ($#v3_group_1 :::"associative"::: ) ($#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"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set (Var "L")) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "L")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k9_polynom3 :::"0_."::: ) (Set (Var "L")))) & (Bool (Set (Var "z")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "p")))) "holds" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set "(" (Set (Var "p")) ($#k5_hurwitz :::"div"::: ) (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_hurwitz :::"deg"::: ) (Set (Var "p")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))))) ; begin definitionlet "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ); attr "f" is :::"Hurwitz"::: means :: HURWITZ:def 8 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_polynom5 :::"is_a_root_of"::: ) "f")) "holds" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))); end; :: deftheorem defines :::"Hurwitz"::: HURWITZ:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) "iff" (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_polynom5 :::"is_a_root_of"::: ) (Set (Var "f")))) "holds" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ")" )); theorem :: HURWITZ:37 (Bool (Bool "not" (Set ($#k9_polynom3 :::"0_."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )) "is" ($#v1_hurwitz :::"Hurwitz"::: ) )) ; theorem :: HURWITZ:38 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool (Set (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set "(" ($#k10_polynom3 :::"1_."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" )) "is" ($#v1_hurwitz :::"Hurwitz"::: ) )) ; theorem :: HURWITZ:39 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k3_polynom5 :::"*"::: ) (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ")" )) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) "iff" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: HURWITZ:40 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set ($#k1_complfld :::"F_Complex"::: ) )))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) "iff" (Bool (Set (Set (Var "z")) ($#k3_polynom5 :::"*"::: ) (Set (Var "f"))) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) ")" ))) ; theorem :: HURWITZ:41 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "g"))) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) ")" ) ")" )) ; definitionlet "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ); func "f" :::"*'"::: -> ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) means :: HURWITZ:def 9 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set it ($#k1_normsp_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" "f" ($#k1_normsp_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_complfld :::"*'"::: ) ")" )))); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_complfld :::"*'"::: ) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b1")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_complfld :::"*'"::: ) ")" ))))) ; end; :: deftheorem defines :::"*'"::: HURWITZ:def 9 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) )) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_group_1 :::"power"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_group_1 :::"1_"::: ) (Set ($#k1_complfld :::"F_Complex"::: ) ) ")" ) ")" ) "," (Set (Var "i")) ")" ")" ) ($#k8_group_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_normsp_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k2_complfld :::"*'"::: ) ")" )))) ")" )); theorem :: HURWITZ:42 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "f"))))) ; theorem :: HURWITZ:43 canceled; theorem :: HURWITZ:44 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "z")) ($#k3_polynom5 :::"*"::: ) (Set (Var "f")) ")" ) ($#k7_hurwitz :::"*'"::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k2_complfld :::"*'"::: ) ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ))))) ; theorem :: HURWITZ:45 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" ($#k5_vfunct_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k7_hurwitz :::"*'"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k5_vfunct_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" )))) ; theorem :: HURWITZ:46 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k8_polynom3 :::"+"::: ) (Set (Var "g")) ")" ) ($#k7_hurwitz :::"*'"::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) ($#k8_polynom3 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k7_hurwitz :::"*'"::: ) ")" )))) ; theorem :: HURWITZ:47 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k13_polynom3 :::"*'"::: ) (Set (Var "g")) ")" ) ($#k7_hurwitz :::"*'"::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) ($#k13_polynom3 :::"*'"::: ) (Set "(" (Set (Var "g")) ($#k7_hurwitz :::"*'"::: ) ")" )))) ; theorem :: HURWITZ:48 (Bool "for" (Set (Var "x")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "z")) ")" ")" ) ($#k7_hurwitz :::"*'"::: ) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "z")) ($#k2_complfld :::"*'"::: ) ")" )))) ; theorem :: HURWITZ:49 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k17_complex1 :::".|"::: ) )))) ; theorem :: HURWITZ:50 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k17_complex1 :::".|"::: ) )) ")" & "(" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k17_complex1 :::".|"::: ) )) ")" & "(" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) "," (Set (Var "x")) ")" ")" ) ($#k17_complex1 :::".|"::: ) )) ")" ")" ))) ; definitionlet "f" be ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ); let "z" be ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ); func :::"F*"::: "(" "f" "," "z" ")" -> ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) equals :: HURWITZ:def 10 (Set (Set "(" (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" "f" ($#k7_hurwitz :::"*'"::: ) ")" ) "," "z" ")" ")" ) ($#k3_polynom5 :::"*"::: ) "f" ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" "f" "," "z" ")" ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" "f" ($#k7_hurwitz :::"*'"::: ) ")" ) ")" )); end; :: deftheorem defines :::"F*"::: HURWITZ:def 10 : (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "holds" (Bool (Set ($#k8_hurwitz :::"F*"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) "," (Set (Var "z")) ")" ")" ) ($#k3_polynom5 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "f")) "," (Set (Var "z")) ")" ")" ) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) ")" ))))); theorem :: HURWITZ:51 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "a")) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "b")) ($#k17_complex1 :::".|"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) "iff" (Bool (Set (Set "(" (Set (Var "a")) ($#k3_polynom5 :::"*"::: ) (Set (Var "f")) ")" ) ($#k3_normsp_1 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k3_polynom5 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) ")" )) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) ")" ))) ; theorem :: HURWITZ:52 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "rho")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "rho"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) )) "holds" (Bool (Set (Set "(" ($#k8_hurwitz :::"F*"::: ) "(" (Set (Var "f")) "," (Set (Var "rho")) ")" ")" ) ($#k5_hurwitz :::"div"::: ) (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "rho")) ")" ")" )) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ))) ; theorem :: HURWITZ:53 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool "ex" (Set (Var "rho")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "rho"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "f")) "," (Set (Var "rho")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) "," (Set (Var "rho")) ")" ")" ) ($#k17_complex1 :::".|"::: ) )) ")" ))) "holds" (Bool "not" (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ))) ; theorem :: HURWITZ:54 (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Polynomial":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k2_hurwitz :::"deg"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "rho")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k1_complfld :::"F_Complex"::: ) ) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "rho"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set (Var "f")) "," (Set (Var "rho")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" ($#k2_polynom4 :::"eval"::: ) "(" (Set "(" (Set (Var "f")) ($#k7_hurwitz :::"*'"::: ) ")" ) "," (Set (Var "rho")) ")" ")" ) ($#k17_complex1 :::".|"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) "iff" (Bool (Set (Set "(" ($#k8_hurwitz :::"F*"::: ) "(" (Set (Var "f")) "," (Set (Var "rho")) ")" ")" ) ($#k5_hurwitz :::"div"::: ) (Set "(" ($#k3_hurwitz :::"rpoly"::: ) "(" (Num 1) "," (Set (Var "rho")) ")" ")" )) "is" ($#v1_hurwitz :::"Hurwitz"::: ) ) ")" ))) ;