:: POLYEQ_3 semantic presentation begin definitionlet "z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"^2"::: redefine func "z" :::"^2"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: POLYEQ_3:def 1 (Set (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) "z" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) "z" ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) "z" ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k4_complex1 :::"Im"::: ) "z" ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )); end; :: deftheorem defines :::"^2"::: POLYEQ_3:def 1 : (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set (Set (Var "z")) ($#k1_polyeq_3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))); definitionlet "a", "b", "c" be ($#m1_subset_1 :::"Real":::); let "z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); :: original: :::"Polynom"::: redefine func :::"Polynom"::: "(" "a" "," "b" "," "c" "," "z" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; theorem :: POLYEQ_3:1 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_polyeq_3 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))))) ; theorem :: POLYEQ_3:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_polyeq_3 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) ; theorem :: POLYEQ_3:3 (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k2_polyeq_3 :::"Polynom"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "b")) ")" ))))) ; theorem :: POLYEQ_3:4 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "," (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k3_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_polyeq_1 :::"Quard"::: ) "(" (Set (Var "a")) "," (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set (Var "z1")) ($#k3_binop_2 :::"+"::: ) (Set (Var "z2")) ")" ))) & (Bool (Set (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z1")) ($#k5_binop_2 :::"*"::: ) (Set (Var "z2")))) ")" ))) ; definitionlet "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "z" :::"^3"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) equals :: POLYEQ_3:def 2 (Set (Set "(" "z" ($#k3_square_1 :::"^2"::: ) ")" ) ($#k5_binop_2 :::"*"::: ) "z"); end; :: deftheorem defines :::"^3"::: POLYEQ_3:def 2 : (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "z")) ($#k3_polyeq_3 :::"^3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z"))))); definitionlet "a", "b", "c", "d", "z" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; redefine func :::"Polynom"::: "(" "a" "," "b" "," "c" "," "d" "," "z" ")" equals :: POLYEQ_3:def 3 (Set (Set "(" (Set "(" (Set "(" "a" ($#k5_binop_2 :::"*"::: ) (Set "(" "z" ($#k3_polyeq_3 :::"^3"::: ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" "b" ($#k5_binop_2 :::"*"::: ) (Set "(" "z" ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" "c" ($#k5_binop_2 :::"*"::: ) "z" ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) "d"); end; :: deftheorem defines :::"Polynom"::: POLYEQ_3:def 3 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k3_polyeq_3 :::"^3"::: ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_binop_2 :::"*"::: ) (Set "(" (Set (Var "z")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set (Var "d"))))); theorem :: POLYEQ_3:5 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set "(" (Set (Var "z")) ($#k3_polyeq_3 :::"^3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set "(" (Set (Var "z")) ($#k3_polyeq_3 :::"^3"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "z")) ")" ) ")" ))) ")" )) ; theorem :: POLYEQ_3:6 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "," (Set (Var "z")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "a9"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "b9"))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Var "c9"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Var "d9"))) ")" )) ; theorem :: POLYEQ_3:7 (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "c")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "b")) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "c")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "b")) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" ))))) ; theorem :: POLYEQ_3:8 (Bool "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "b")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) ; theorem :: POLYEQ_3:9 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "c")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: POLYEQ_3:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "b")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: POLYEQ_3:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k2_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: POLYEQ_3:12 (Bool "for" (Set (Var "y")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "not" (Bool (Set (Set (Var "y")) ($#k5_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "a"))) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set (Var "a")))) "or" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set (Var "a")) ")" ))) ")" )) ; theorem :: POLYEQ_3:13 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k9_binop_2 :::"+"::: ) (Set (Var "v")))) & (Bool (Set (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "v")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "u")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )))))) ; theorem :: POLYEQ_3:14 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k9_binop_2 :::"+"::: ) (Set (Var "v")))) & (Bool (Set (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "v")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "u")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 4) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "d")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 16) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 12) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k12_binop_2 :::"/"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))))) ; theorem :: POLYEQ_3:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "u")) "," (Set (Var "v")) "," (Set (Var "x1")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "z")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))) & (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "u")) ($#k9_binop_2 :::"+"::: ) (Set (Var "v")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))) & (Bool (Set (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "u")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "v")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 6) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 9) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 6) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 9) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 6) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 9) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 6) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 9) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 6) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 9) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Num 3) ($#k2_power :::"-root"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 6) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "d")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 4) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "c")) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 9) ($#k11_binop_2 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k10_binop_2 :::"-"::: ) (Set "(" (Set (Var "b")) ($#k12_binop_2 :::"/"::: ) (Set "(" (Num 3) ($#k11_binop_2 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))))) ; theorem :: POLYEQ_3:16 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k6_binop_2 :::"/"::: ) (Set (Var "z1")) ")" )))) ; begin theorem :: POLYEQ_3:17 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool (Set ($#k3_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "," (Set (Var "z")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "z1")) ($#r1_hidden :::"="::: ) (Set (Var "s1"))) & (Bool (Set (Var "z2")) ($#r1_hidden :::"="::: ) (Set (Var "s2"))) & (Bool (Set (Var "z3")) ($#r1_hidden :::"="::: ) (Set (Var "s3"))) ")" )) ; theorem :: POLYEQ_3:18 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set (Var "a")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "a")) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: POLYEQ_3:19 (Bool "for" (Set (Var "z")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k1_polyeq_3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: POLYEQ_3:20 (Bool "for" (Set (Var "z")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k1_polyeq_3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" )))) ; theorem :: POLYEQ_3:21 (Bool "for" (Set (Var "z")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k1_polyeq_3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_complex1 :::"Re"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: POLYEQ_3:22 (Bool "for" (Set (Var "z")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Set (Var "z")) ($#k1_polyeq_3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k4_complex1 :::"Im"::: ) (Set (Var "s"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )))) ; theorem :: POLYEQ_3:23 (Bool "for" (Set (Var "z")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Set (Var "z")) ($#k1_polyeq_3 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "s"))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) ")" )) ; theorem :: POLYEQ_3:24 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k6_binop_2 :::"/"::: ) (Set (Var "z1")) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: POLYEQ_3:25 (Bool "for" (Set (Var "z1")) "," (Set (Var "z3")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "z1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z3")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set (Var "z3")) ($#k6_binop_2 :::"/"::: ) (Set (Var "z1")) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) ")" ))) ; theorem :: POLYEQ_3:26 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "h")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z2")) ($#k6_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k1_polyeq_3 :::"^2"::: ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "z3")) ($#k6_binop_2 :::"/"::: ) (Set (Var "z1")) ")" ))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k6_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z1")) ")" ))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set (Var "t"))))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set (Var "t"))))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set (Var "t")))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set (Var "t")))))) ; theorem :: POLYEQ_3:27 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")))) & (Bool (Set (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "z")) ($#k1_polyeq_3 :::"^2"::: ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set (Var "z")))) & (Bool (Set (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k3_polyeq_3 :::"^3"::: ) )) ")" )) ; theorem :: POLYEQ_3:28 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set (Var "z2")) ($#k6_binop_2 :::"/"::: ) (Set (Var "z1")) ")" ))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: POLYEQ_3:29 (Bool "for" (Set (Var "z1")) "," (Set (Var "z3")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "z1")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "holds" (Bool "(" "not" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k1_binop_2 :::"-"::: ) (Set "(" (Set (Var "z3")) ($#k6_binop_2 :::"/"::: ) (Set (Var "z1")) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) "or" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "s")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))) ")" ))) ; theorem :: POLYEQ_3:30 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "z1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k7_polyeq_1 :::"Polynom"::: ) "(" (Set (Var "z1")) "," (Set (Var "z2")) "," (Set (Var "z3")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "," (Set (Var "h")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "z2")) ($#k6_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k1_polyeq_3 :::"^2"::: ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set "(" (Set (Var "z3")) ($#k6_binop_2 :::"/"::: ) (Set (Var "z1")) ")" ))) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "z2")) ($#k6_binop_2 :::"/"::: ) (Set "(" (Num 2) ($#k5_binop_2 :::"*"::: ) (Set (Var "z1")) ")" ))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set (Var "t"))))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set (Var "t"))))) & (Bool (Bool "not" (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set (Var "t")))))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k7_binop_2 :::"-"::: ) (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k3_complex1 :::"Re"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k4_complex1 :::"Im"::: ) (Set (Var "h")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Num 2) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k4_binop_2 :::"-"::: ) (Set (Var "t")))))) ; theorem :: POLYEQ_3:31 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" ($#k20_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k17_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "n")) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "n")) ($#k11_binop_2 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) ; theorem :: POLYEQ_3:32 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set (Var "n")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ($#k3_power :::"to_power"::: ) (Set (Var "n")) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set (Var "n")) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) ; theorem :: POLYEQ_3:33 (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set (Var "x")) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set (Var "x")) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ))))) ; theorem :: POLYEQ_3:34 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "n")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" ) ($#k1_newton :::"|^"::: ) (Set (Var "n")))))) ; theorem :: POLYEQ_3:35 (Bool "for" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "n")) ($#k2_power :::"-root"::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "z")) ")" ) ($#k9_binop_2 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) "is" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set (Var "z")))))) ; theorem :: POLYEQ_3:36 (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_comptrig :::"CRoot"::: ) "of" (Num 1) "," (Set (Var "z")) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; theorem :: POLYEQ_3:37 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "v")) "being" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set ($#k6_numbers :::"0"::: ) ) "holds" (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: POLYEQ_3:38 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "z")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "v")) "being" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Set (Var "z")) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))))) ; theorem :: POLYEQ_3:39 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k3_binop_2 :::"+"::: ) (Set "(" (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k11_binop_2 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k11_binop_2 :::"*"::: ) (Set (Var "k")) ")" ) ($#k12_binop_2 :::"/"::: ) (Set (Var "n")) ")" ) ")" ) ($#k5_binop_2 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" )) "is" ($#m1_comptrig :::"CRoot"::: ) "of" (Set (Var "n")) "," (Num 1)))) ; theorem :: POLYEQ_3:40 (Bool "for" (Set (Var "z")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_numbers :::"COMPLEX"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "z")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Set (Var "s")) ($#k1_newton :::"|^"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "z")) ($#k1_newton :::"|^"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "s")) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) )))) ;