:: POLYEQ_5  semantic presentation begin  




theorem :: POLYEQ_5:1 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 2)))) ; 
 
theorem :: POLYEQ_5:2 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 3)))) ; 
 
theorem :: POLYEQ_5:3 (Bool  "for" (Set (Var "a")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 4)))) ; 
 
theorem :: POLYEQ_5:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k1_newton :::"|^"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )))) ; 
 
theorem :: POLYEQ_5:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k1_newton :::"|^"::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )))) ; 
 
theorem :: POLYEQ_5:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k1_newton :::"|^"::: )  (Num 4))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "b")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 6)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" )))) ; 
 notationlet "n" be   ($#m1_hidden :::"Nat":::); let "r" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; synonym "n" :::"-real-root"::: "r" for "n" :::"-root"::: "r"; end; definitionlet "n" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::); let "z" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func "n" :::"-root"::: "z" ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   equals :: POLYEQ_5:def 1 (Set (Set  "(" "n"  ($#k1_power :::"-real-root"::: )  (Set  ($#k17_complex1 :::"|."::: ) "z" ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "("  ($#k1_comptrig :::"Arg"::: )  "z" ")" )  ($#k13_complex1 :::"/"::: )  "n" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "("  ($#k1_comptrig :::"Arg"::: )  "z" ")" )  ($#k13_complex1 :::"/"::: )  "n" ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" )); end; 






:: deftheorem    defines :::"-root"::: POLYEQ_5:def 1 :  (Bool  "for" (Set (Var "n")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "n"))  ($#k1_polyeq_5 :::"-root"::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n"))  ($#k1_power :::"-real-root"::: )  (Set  ($#k17_complex1 :::"|."::: ) (Set (Var "z")) ($#k17_complex1 :::".|"::: ) ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "("  ($#k20_sin_cos :::"cos"::: )  (Set  "(" (Set  "("  ($#k1_comptrig :::"Arg"::: )  (Set (Var "z")) ")" )  ($#k13_complex1 :::"/"::: )  (Set (Var "n")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k17_sin_cos :::"sin"::: )  (Set  "(" (Set  "("  ($#k1_comptrig :::"Arg"::: )  (Set (Var "z")) ")" )  ($#k13_complex1 :::"/"::: )  (Set (Var "n")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" ) ")" ))))); 
 






theorem :: POLYEQ_5:7 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n0")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Set  "(" (Set (Var "n0"))  ($#k1_polyeq_5 :::"-root"::: )  (Set (Var "z")) ")" )  ($#k1_newton :::"|^"::: )  (Set (Var "n0")))  ($#r1_hidden :::"="::: )  (Set (Var "z"))))) ; 
 
theorem :: POLYEQ_5:8 (Bool  "for" (Set (Var "n0")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "n0"))  ($#k1_polyeq_5 :::"-root"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "n0"))  ($#k1_power :::"-real-root"::: )  (Set (Var "r")))))) ; 
 
theorem :: POLYEQ_5:9 (Bool  "for" (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "n0")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"zero"::: )   )   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set (Var "n0"))  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set (Var "z"))  ($#k13_complex1 :::"/"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "n0"))  ($#k1_polyeq_5 :::"-root"::: )  (Set (Var "z")) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "n0"))  ($#k1_polyeq_5 :::"-root"::: )  (Set (Var "r")) ")" )))))) ; 
 
theorem :: POLYEQ_5:10 (Bool  "for" (Set (Var "a")) "," (Set (Var "z")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set (Var "a")))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set (Var "a")) ")" )))  ")" )  ")" )) ; 
 begin  







theorem :: POLYEQ_5:11 (Bool  "for" (Set (Var "z")) "," (Set (Var "a1")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "a0")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" ))) & (Bool (Set (Var "a0"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s1"))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s2")))  ")" )  ")" )) ; 
 
theorem :: POLYEQ_5:12 (Bool  "for" (Set (Var "z")) "," (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a2"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )))  ")" )  ")" )) ; 
 begin  








theorem :: POLYEQ_5:13 (Bool  "for" (Set (Var "z")) "," (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "," (Set (Var "x")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54)))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: POLYEQ_5:14 (Bool  "for" (Set (Var "z")) "," (Set (Var "a2")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a2"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")) ")" ))) & (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" ))) & (Bool (Set (Var "a0"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s1"))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s2"))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s3")))  ")" )  ")" )) ; 
 
theorem :: POLYEQ_5:15 (Bool  "for" (Set (Var "z")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a0")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s")) ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set (Var "s1")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" )  ")" )) ; 
 
theorem :: POLYEQ_5:16 (Bool  "for" (Set (Var "z")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a0")) "," (Set (Var "s1")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "s1"))  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "s1"))  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" )  ")" )) ; 
 definitionlet "a0", "a1", "a2" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"1_root_of_cubic":::  "(" "a0" "," "a1" "," "a2" ")"  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: POLYEQ_5:def 2 (Bool  "ex" (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a2"  ($#k13_complex1 :::"/"::: )  (Num 3) ")" )))  ")" )) if (Bool (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool  "ex" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s")) ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set (Var "s1")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a2"  ($#k13_complex1 :::"/"::: )  (Num 3) ")" )))  ")" )); func  :::"2_root_of_cubic":::  "(" "a0" "," "a1" "," "a2" ")"  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: POLYEQ_5:def 3 (Bool  "ex" (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "s1"))  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" "a2"  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" )) if (Bool (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool  "ex" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s")) ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set (Var "s1")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" "a2"  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" )); func  :::"3_root_of_cubic":::  "(" "a0" "," "a1" "," "a2" ")"  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: POLYEQ_5:def 4 (Bool  "ex" (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "s1"))  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" "a2"  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" )) if (Bool (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool  "ex" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a2"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s")) ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set (Var "s1")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" "a2"  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" )); end; 





















:: deftheorem    defines :::"1_root_of_cubic"::: POLYEQ_5:def 2 :  (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b4")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")" )) "iff" (Bool  "ex" (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" )))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")" )) "iff" (Bool  "ex" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s")) ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set (Var "s1")) ")" ))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" )))  ")" ))  ")" )  ")"   ")" )); 
 
:: deftheorem    defines :::"2_root_of_cubic"::: POLYEQ_5:def 3 :  (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b4")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")" )) "iff" (Bool  "ex" (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "s1"))  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")" )) "iff" (Bool  "ex" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s")) ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set (Var "s1")) ")" ))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k8_complex1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" ))  ")" )  ")"   ")" )); 
 
:: deftheorem    defines :::"3_root_of_cubic"::: POLYEQ_5:def 4 :  (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "b4")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_polyeq_5 :::"3_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")" )) "iff" (Bool  "ex" (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "s1"))  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_polyeq_5 :::"3_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")" )) "iff" (Bool  "ex" (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "s1")) "," (Set (Var "s2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 9))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 9)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a2"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 27)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 54))) & (Bool (Set (Var "s"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 3)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set (Var "r"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s")) ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set (Var "s1")) ")" ))) & (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k10_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k11_complex1 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Num 3) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  ($#k7_complex1 :::"<i>"::: ) ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 2) ")" )))  ")" ))  ")" )  ")"   ")" )); 
 
theorem :: POLYEQ_5:17 (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k4_polyeq_5 :::"3_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a2"))))) ; 
 
theorem :: POLYEQ_5:18 (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_polyeq_5 :::"3_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_polyeq_5 :::"3_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a1")))) ; 
 
theorem :: POLYEQ_5:19 (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k4_polyeq_5 :::"3_root_of_cubic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a0"))))) ; 
 
theorem :: POLYEQ_5:20 (Bool  "for" (Set (Var "z")) "," (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "," (Set (Var "a3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a3"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a3"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "(" (Set (Var "a0"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) "," (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) "," (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) ")" )) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "(" (Set (Var "a0"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) "," (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) "," (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) ")" )) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_polyeq_5 :::"3_root_of_cubic"::: )   "(" (Set  "(" (Set (Var "a0"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) "," (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) "," (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a3")) ")" ) ")" ))  ")" )  ")" )) ; 
 begin  





theorem :: POLYEQ_5:21 (Bool  "for" (Set (Var "z")) "," (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "," (Set (Var "x")) "," (Set (Var "a3")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "p")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" ))) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024)))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) ; 
 
theorem :: POLYEQ_5:22 (Bool  "for" (Set (Var "z")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "," (Set (Var "a3")) "," (Set (Var "s3")) "," (Set (Var "s4")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s4")) ")" ))) & (Bool (Set (Var "a2"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s4")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s4")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "s3"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s4")) ")" ))) & (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s4")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s4")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "s2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s4")) ")" ) ")" ))) & (Bool (Set (Var "a0"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s4"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s1"))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s2"))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s3"))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Var "s4")))  ")" )  ")" )) ; 
 
theorem :: POLYEQ_5:23 (Bool  "for" (Set (Var "z")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s3")) "," (Set (Var "p")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "q"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s3")))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s3")))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3"))))  ")" )  ")" )) ; 
 
theorem :: POLYEQ_5:24 (Bool  "for" (Set (Var "z")) "," (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "a3")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s3")) "," (Set (Var "p")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )  ")" )) ; 
 
theorem :: POLYEQ_5:25 (Bool  "for" (Set (Var "z")) "," (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "," (Set (Var "s1")) "," (Set (Var "a3")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "p")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" )))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" ))) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )  ")" )) ; 
 definitionlet "a0", "a1", "a2", "a3" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"1_root_of_quartic":::  "(" "a0" "," "a1" "," "a2" "," "a3" ")"  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: POLYEQ_5:def 5 (Bool  "ex" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a3"  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )) if (Bool (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a3"  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )); func  :::"2_root_of_quartic":::  "(" "a0" "," "a1" "," "a2" "," "a3" ")"  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: POLYEQ_5:def 6 (Bool  "ex" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a3"  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )) if (Bool (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a3"  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )); func  :::"3_root_of_quartic":::  "(" "a0" "," "a1" "," "a2" "," "a3" ")"  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: POLYEQ_5:def 7 (Bool  "ex" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a3"  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )) if (Bool (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a3"  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )); func  :::"4_root_of_quartic":::  "(" "a0" "," "a1" "," "a2" "," "a3" ")"  ->   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   means :: POLYEQ_5:def 8 (Bool  "ex" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a3"  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )) if (Bool (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  otherwise (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  "a0" ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  "a3" ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a1" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  "a2" ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "a3"  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" ))) & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" "a3"  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" )); end; 
































:: deftheorem    defines :::"1_root_of_quartic"::: POLYEQ_5:def 5 :  (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b5")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" ))) & (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" ))  ")" )  ")"   ")" )); 
 
:: deftheorem    defines :::"2_root_of_quartic"::: POLYEQ_5:def 6 :  (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b5")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" ))) & (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" ))  ")" )  ")"   ")" )); 
 
:: deftheorem    defines :::"3_root_of_quartic"::: POLYEQ_5:def 7 :  (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b5")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" ))) & (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "s1")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" ))  ")" )  ")"   ")" )); 
 
:: deftheorem    defines :::"4_root_of_quartic"::: POLYEQ_5:def 8 :  (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "b5")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "s1")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ))) & (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "p"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "s1")) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" ))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")" )) "iff" (Bool  "ex" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s1")) "," (Set (Var "s2")) "," (Set (Var "s3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 32))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 8)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 4)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 64))) & (Bool (Set (Var "r"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 256)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a0")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Num 64)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a3")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a1")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Num 16)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a2")) ")" ) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Num 3)  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "a3"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" ) ")" )  ($#k13_complex1 :::"/"::: )  (Num 1024))) & (Bool (Set (Var "s1"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k2_polyeq_5 :::"1_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s2"))  ($#r1_hidden :::"="::: )  (Set (Num 2)  ($#k1_polyeq_5 :::"-root"::: )  (Set  "("  ($#k3_polyeq_5 :::"2_root_of_cubic"::: )   "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) "," (Set  "(" (Set  "(" (Set (Var "p"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "r")) ")" ) "," (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" ) ")"  ")" ))) & (Bool (Set (Var "s3"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_complex1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k13_complex1 :::"/"::: )  (Set  "(" (Set (Var "s1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "s2")) ")" ) ")" ))) & (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "s1"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s2")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "s3")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Num 4) ")" )))  ")" ))  ")" )  ")"   ")" )); 
 
theorem :: POLYEQ_5:26 (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a3"))))) ; 
 
theorem :: POLYEQ_5:27 (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "("  ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a2")))) ; 
 
theorem :: POLYEQ_5:28 (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "("  ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "a1"))))) ; 
 
theorem :: POLYEQ_5:29 (Bool  "for" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "("  ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "("  ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "a0")))) ; 
 
theorem :: POLYEQ_5:30 (Bool  "for" (Set (Var "z")) "," (Set (Var "a2")) "," (Set (Var "a1")) "," (Set (Var "a0")) "," (Set (Var "a3")) "," (Set (Var "a4")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a4"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set (Var "a4"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 4) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a3"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "z"))  ($#k1_newton :::"|^"::: )  (Num 2) ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "z")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a0")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_polyeq_5 :::"1_root_of_quartic"::: )   "(" (Set  "(" (Set (Var "a0"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) ")" )) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_polyeq_5 :::"2_root_of_quartic"::: )   "(" (Set  "(" (Set (Var "a0"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) ")" )) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_polyeq_5 :::"3_root_of_quartic"::: )   "(" (Set  "(" (Set (Var "a0"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) ")" )) "or" (Bool (Set (Var "z"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_polyeq_5 :::"4_root_of_quartic"::: )   "(" (Set  "(" (Set (Var "a0"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a1"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a2"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) "," (Set  "(" (Set (Var "a3"))  ($#k13_complex1 :::"/"::: )  (Set (Var "a4")) ")" ) ")" ))  ")" )  ")" )) ;