:: POLYEQ_2 semantic presentation begin definitionlet "a", "b", "c", "d", "e", "x" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Polynom"::: "(" "a" "," "b" "," "c" "," "d" "," "e" "," "x" ")" -> ($#m1_hidden :::"set"::: ) equals :: POLYEQ_2:def 1 (Set (Set "(" (Set "(" (Set "(" (Set "(" "a" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "b" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "c" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "d" ($#k3_xcmplx_0 :::"*"::: ) "x" ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) "e"); end; :: deftheorem defines :::"Polynom"::: POLYEQ_2:def 1 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "x")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "e")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "c")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "d")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "e"))))); registrationlet "a", "b", "c", "d", "e", "x" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" "a" "," "b" "," "c" "," "d" "," "e" "," "x" ")" ) -> ($#v1_xcmplx_0 :::"complex"::: ) ; end; registrationlet "a", "b", "c", "d", "e", "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" "a" "," "b" "," "c" "," "d" "," "e" "," "x" ")" ) -> ($#v1_xreal_0 :::"real"::: ) ; end; theorem :: POLYEQ_2:1 (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "e")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "e")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "e")) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "c")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "e")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "e")) ")" ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "e")) ")" ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "e")) ")" ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "e")) ")" ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ))) ")" ) ")" )) ; theorem :: POLYEQ_2:2 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: POLYEQ_2:3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 8) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "x")) ")" ))) & (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 8) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) & (Bool (Set (Var "y2")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "b")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Num 8) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y1")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "y1")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y2")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "y2")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y1")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "y1")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2))) "or" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "y2")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Num 1) "," (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "y2")) ")" ) "," (Num 1) ")" ")" ) ")" ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2))) ")" ) ")" ))) ; theorem :: POLYEQ_2:4 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4))) & (Bool (Set (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4))) ")" )) ; theorem :: POLYEQ_2:5 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_newton :::"|^"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 3) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" )))) ; theorem :: POLYEQ_2:6 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "y")) ")" ) ($#k1_newton :::"|^"::: ) (Num 4)) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k1_newton :::"|^"::: ) (Num 4) ")" )))) ; theorem :: POLYEQ_2:7 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "," (Set (Var "x")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Var "b5"))) & (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b3")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b4")))) & (Bool (Set (Set "(" (Set "(" (Set (Var "a1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "b1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b4")))) ")" )) ; theorem :: POLYEQ_2:8 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "," (Set (Var "x")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "a1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b3")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a3")))) & (Bool (Set (Set (Var "a2")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b4")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a4")))) ")" )) ; theorem :: POLYEQ_2:9 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "," (Set (Var "x")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Var "b1"))) & (Bool (Set (Var "a2")) ($#r1_hidden :::"="::: ) (Set (Var "b2"))) & (Bool (Set (Var "a3")) ($#r1_hidden :::"="::: ) (Set (Var "b3"))) & (Bool (Set (Var "a4")) ($#r1_hidden :::"="::: ) (Set (Var "b4"))) & (Bool (Set (Var "a5")) ($#r1_hidden :::"="::: ) (Set (Var "b5"))) ")" )) ; definitionlet "a1", "x1", "x2", "x3", "x4", "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Four0"::: "(" "a1" "," "x1" "," "x2" "," "x3" "," "x4" "," "x" ")" -> ($#m1_hidden :::"set"::: ) equals :: POLYEQ_2:def 2 (Set "a1" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" "x" ($#k6_xcmplx_0 :::"-"::: ) "x1" ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k6_xcmplx_0 :::"-"::: ) "x2" ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k6_xcmplx_0 :::"-"::: ) "x3" ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "x" ($#k6_xcmplx_0 :::"-"::: ) "x4" ")" ) ")" )); end; :: deftheorem defines :::"Four0"::: POLYEQ_2:def 2 : (Bool "for" (Set (Var "a1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_polyeq_2 :::"Four0"::: ) "(" (Set (Var "a1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a1")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x4")) ")" ) ")" )))); registrationlet "a1", "x1", "x2", "x3", "x4", "x" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k2_polyeq_2 :::"Four0"::: ) "(" "a1" "," "x1" "," "x2" "," "x3" "," "x4" "," "x" ")" ) -> ($#v1_xreal_0 :::"real"::: ) ; end; theorem :: POLYEQ_2:10 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_polyeq_2 :::"Four0"::: ) "(" (Set (Var "a1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a4")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a5")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x3")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x1")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x2")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" )))) ; theorem :: POLYEQ_2:11 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_polyeq_2 :::"Four0"::: ) "(" (Set (Var "a1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x")) ")" )) ")" )) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "a1")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a2")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a3")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a4")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a5")) ")" ) ($#k13_complex1 :::"/"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x4")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x3")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" )))) ; theorem :: POLYEQ_2:12 (Bool "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_polyeq_2 :::"Polynom"::: ) "(" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_polyeq_2 :::"Four0"::: ) "(" (Set (Var "a1")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x4")) "," (Set (Var "x")) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Set (Var "a2")) ($#k13_complex1 :::"/"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "x4")) ")" ))) & (Bool (Set (Set (Var "a3")) ($#k13_complex1 :::"/"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "x3")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ))) & (Bool (Set (Set (Var "a4")) ($#k13_complex1 :::"/"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set (Var "x2")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")) ")" ) ")" ))) & (Bool (Set (Set (Var "a5")) ($#k13_complex1 :::"/"::: ) (Set (Var "a1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "x1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x2")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x3")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x4")))) ")" )) ; theorem :: POLYEQ_2:13 (Bool "for" (Set (Var "a")) "," (Set (Var "k")) "," (Set (Var "y")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k1_newton :::"|^"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "a")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ))) ")" )) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set (Var "y")) ($#k1_newton :::"|^"::: ) (Num 4) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "y")) ($#k1_newton :::"|^"::: ) (Num 3) ")" ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "k")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "y")) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ;