:: POLYEQ_1  semantic presentation begin  























definitionlet "a", "b", "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Polynom":::  "(" "a" "," "b" "," "x" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: POLYEQ_1:def 1 (Set (Set  "(" "a"  ($#k3_xcmplx_0 :::"*"::: )  "x" ")" )  ($#k2_xcmplx_0 :::"+"::: )  "b"); end; 







:: deftheorem    defines :::"Polynom"::: POLYEQ_1:def 1 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "b"))))); 
 registrationlet "a", "b", "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_polyeq_1 :::"Polynom"::: )   "(" "a" "," "b" "," "x" ")" ) ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 
end; registrationlet "a", "b", "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k1_polyeq_1 :::"Polynom"::: )   "(" "a" "," "b" "," "x" ")" ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "a", "b", "x" be   ($#m1_subset_1 :::"Real":::); :: original: :::"Polynom"::: redefine func  :::"Polynom":::  "(" "a" "," "b" "," "x" ")"  ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POLYEQ_1:1 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" )))) ; 
 
theorem :: POLYEQ_1:2 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k1_polyeq_1 :::"Polynom"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: POLYEQ_1:3 (Bool  "for" (Set (Var "b")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "holds" (Bool (Bool  "not" (Set   ($#k1_polyeq_1 :::"Polynom"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 definitionlet "a", "b", "c", "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Polynom":::  "(" "a" "," "b" "," "c" "," "x" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: POLYEQ_1:def 2 (Set (Set  "(" (Set  "(" "a"  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "x"  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "b"  ($#k3_xcmplx_0 :::"*"::: )  "x" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  "c"); end; 








:: deftheorem    defines :::"Polynom"::: POLYEQ_1:def 2 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "c"))))); 
 registrationlet "a", "b", "c", "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" "a" "," "b" "," "c" "," "x" ")" ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; registrationlet "a", "b", "c", "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" "a" "," "b" "," "c" "," "x" ")" ) ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 
end; definitionlet "a", "b", "c", "x" be   ($#m1_subset_1 :::"Real":::); :: original: :::"Polynom"::: redefine func  :::"Polynom":::  "(" "a" "," "b" "," "c" "," "x" ")"  ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POLYEQ_1:4 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "x")) ")" ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "c9")))  ")" )) ; 
 
theorem :: POLYEQ_1:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" ) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ))) "or" (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" ) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )))  ")" ))) ; 
 
theorem :: POLYEQ_1:6 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set  "(" (Num 2)  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "a")) ")" ) ")" )))) ; 
 
theorem :: POLYEQ_1:7 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "holds" (Bool (Bool  "not" (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: POLYEQ_1:8 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "b")) ")" ))))) ; 
 
theorem :: POLYEQ_1:9 (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) ; 
 
theorem :: POLYEQ_1:10 (Bool  "for" (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "holds" (Bool (Bool  "not" (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "c")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 definitionlet "a", "x", "x1", "x2" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Quard":::  "(" "a" "," "x1" "," "x2" "," "x" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: POLYEQ_1:def 3 (Set "a"  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" "x"  ($#k6_xcmplx_0 :::"-"::: )  "x1" ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "x"  ($#k6_xcmplx_0 :::"-"::: )  "x2" ")" ) ")" )); end; 








:: deftheorem    defines :::"Quard"::: POLYEQ_1:def 3 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k5_polyeq_1 :::"Quard"::: )   "(" (Set (Var "a")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "x1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "x2")) ")" ) ")" )))); 
 registrationlet "a", "x", "x1", "x2" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k5_polyeq_1 :::"Quard"::: )   "(" "a" "," "x1" "," "x2" "," "x" ")" ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "a", "x", "x1", "x2" be   ($#m1_subset_1 :::"Real":::); :: original: :::"Quard"::: redefine func  :::"Quard":::  "(" "a" "," "x1" "," "x2" "," "x" ")"  ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POLYEQ_1:11 (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k5_polyeq_1 :::"Quard"::: )   "(" (Set (Var "a")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x")) ")" ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "x1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "x2")) ")" ))) & (Bool (Set (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x2"))))  ")" ))) ; 
 begin  definitionlet "a", "b", "c", "d", "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Polynom":::  "(" "a" "," "b" "," "c" "," "d" "," "x" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: POLYEQ_1:def 4 (Set (Set  "(" (Set  "(" (Set  "(" "a"  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "x"  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "b"  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "x"  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" "c"  ($#k3_xcmplx_0 :::"*"::: )  "x" ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  "d"); end; 









:: deftheorem    defines :::"Polynom"::: POLYEQ_1:def 4 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "c"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "d"))))); 
 registrationlet "a", "b", "c", "d", "x" be   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" "a" "," "b" "," "c" "," "d" "," "x" ")" ) ->   ($#v1_xcmplx_0 :::"complex"::: )   ; 
end; registrationlet "a", "b", "c", "d", "x" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" "a" "," "b" "," "c" "," "d" "," "x" ")" ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "a", "b", "c", "d", "x" be   ($#m1_subset_1 :::"Real":::); :: original: :::"Polynom"::: redefine func  :::"Polynom":::  "(" "a" "," "b" "," "c" "," "d" "," "x" ")"  ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POLYEQ_1:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a9")) "," (Set (Var "b9")) "," (Set (Var "c9")) "," (Set (Var "d9")) "," (Set (Var "x")) ")" ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "a"))  ($#r1_hidden :::"="::: )  (Set (Var "a9"))) & (Bool (Set (Var "b"))  ($#r1_hidden :::"="::: )  (Set (Var "b9"))) & (Bool (Set (Var "c"))  ($#r1_hidden :::"="::: )  (Set (Var "c9"))) & (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Var "d9")))  ")" )) ; 
 definitionlet "a", "x", "x1", "x2", "x3" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"Tri":::  "(" "a" "," "x1" "," "x2" "," "x3" "," "x" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: POLYEQ_1:def 5 (Set "a"  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" "x"  ($#k6_xcmplx_0 :::"-"::: )  "x1" ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "x"  ($#k6_xcmplx_0 :::"-"::: )  "x2" ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" "x"  ($#k6_xcmplx_0 :::"-"::: )  "x3" ")" ) ")" )); end; 









:: deftheorem    defines :::"Tri"::: POLYEQ_1:def 5 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k9_polyeq_1 :::"Tri"::: )   "(" (Set (Var "a")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "x1")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "x2")) ")" ) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "x"))  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "x3")) ")" ) ")" )))); 
 registrationlet "a", "x", "x1", "x2", "x3" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set   ($#k9_polyeq_1 :::"Tri"::: )   "(" "a" "," "x1" "," "x2" "," "x3" "," "x" ")" ) ->   ($#v1_xreal_0 :::"real"::: )   ; 
end; definitionlet "a", "x", "x1", "x2", "x3" be   ($#m1_subset_1 :::"Real":::); :: original: :::"Tri"::: redefine func  :::"Tri":::  "(" "a" "," "x1" "," "x2" "," "x3" "," "x" ")"  ->   ($#m1_subset_1 :::"Real":::); end; 
theorem :: POLYEQ_1:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k9_polyeq_1 :::"Tri"::: )   "(" (Set (Var "a")) "," (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "," (Set (Var "x")) ")" ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "x2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "x3")) ")" ))) & (Bool (Set (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x2")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x3")) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "x1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x3")) ")" ))) & (Bool (Set (Set (Var "d"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set  "(" (Set (Var "x1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x2")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "x3")) ")" )))  ")" )) ; 
 
theorem :: POLYEQ_1:14 (Bool  "for" (Set (Var "y")) "," (Set (Var "h")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "y"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "h")) ")" )  ($#k1_newton :::"|^"::: )  (Num 3))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k3_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "h"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "h"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )))) ; 
 
theorem :: POLYEQ_1:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "h")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ))) & (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))) & (Bool (Set (Var "a2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))) & (Bool (Set (Var "a3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "d"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k3_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "h")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a1")) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "h"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "h")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "a2")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "h"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "a1"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "h"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a2"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "h")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "a3")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: POLYEQ_1:16 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "h")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k3_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ))) & (Bool (Set (Var "a1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))) & (Bool (Set (Var "a2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))) & (Bool (Set (Var "a3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "d"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k3_real_1 :::"+"::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "c")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "d")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: POLYEQ_1:17 (Bool  "for" (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "," (Set (Var "d")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "y"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k3_real_1 :::"+"::: )  (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "y"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "c")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "y")) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "d")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "c")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "b"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "d")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "c")) ")" ) ")" )  ($#k10_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )))) "holds"  (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )))) ; 
 
theorem :: POLYEQ_1:18 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "v")))) & (Bool (Set (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "v")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "u")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "u"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "v"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "q")))) & (Bool (Set (Set  "(" (Set (Var "u"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "v"))  ($#k1_newton :::"|^"::: )  (Num 3) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "p"))  ($#k6_real_1 :::"/"::: )  (Num 3) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3)))  ")" ))) ; 
 
theorem :: POLYEQ_1:19 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Num 1) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "v")))) & (Bool (Set (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "v")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "u")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k6_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "q"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Num 4) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_real_1 :::"/"::: )  (Num 3) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k6_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "q"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Num 4) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_real_1 :::"/"::: )  (Num 3) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )))) & (Bool (Bool  "not" (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k6_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "q"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Num 4) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_real_1 :::"/"::: )  (Num 3) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k6_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "q"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Num 4) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_real_1 :::"/"::: )  (Num 3) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ))))) "holds"  (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k6_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "q"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Num 4) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_real_1 :::"/"::: )  (Num 3) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "q"))  ($#k6_real_1 :::"/"::: )  (Num 2) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "q"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Num 4) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_real_1 :::"/"::: )  (Num 3) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ))))) ; 
 
theorem :: POLYEQ_1:20 (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")" )  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")"  ")" ) ")" ) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" ))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) ")"  ")" ) ")" ) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "b")) ")" )))) ; 
 
theorem :: POLYEQ_1:21 (Bool  "for" (Set (Var "a")) "," (Set (Var "p")) "," (Set (Var "c")) "," (Set (Var "q")) "," (Set (Var "d")) "," (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "d"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))) & (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "c")) "," (Set (Var "d")) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool  "for" (Set (Var "u")) "," (Set (Var "v")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "u"))  ($#k2_xcmplx_0 :::"+"::: )  (Set (Var "v")))) & (Bool (Set (Set  "(" (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "v")) ")" )  ($#k8_real_1 :::"*"::: )  (Set (Var "u")) ")" )  ($#k7_real_1 :::"+"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "d"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "d"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "d"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "d"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "d"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "d"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "d"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "d"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "d"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "d"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Num 3)  ($#k2_power :::"-root"::: )  (Set  "(" (Set  "("  ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "d"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" ) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "("  ($#k7_square_1 :::"sqrt"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "d"))  ($#k3_square_1 :::"^2"::: )  ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 4)  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "a"))  ($#k3_square_1 :::"^2"::: )  ")" ) ")" ) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "c"))  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 3)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ) ")" )  ($#k2_newton :::"|^"::: )  (Num 3) ")" ) ")" ) ")" ) ")" ) ")" ))))) ; 
 
theorem :: POLYEQ_1:22 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" ) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" ))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set (Var "b")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k1_quin_1 :::"delta"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")"  ")" ) ")" ) ")" )  ($#k6_real_1 :::"/"::: )  (Set  "(" (Num 2)  ($#k8_real_1 :::"*"::: )  (Set (Var "a")) ")" )))) ; 
 
theorem :: POLYEQ_1:23 (Bool  "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "x")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set   ($#k7_polyeq_1 :::"Polynom"::: )   "(" (Set (Var "a")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "c")) "," (Set  ($#k6_numbers :::"0"::: ) ) "," (Set (Var "x")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ) ")" ))))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "("  ($#k6_square_1 :::"sqrt"::: )  (Set  "("  ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "c"))  ($#k7_xcmplx_0 :::"/"::: )  (Set (Var "a")) ")" ) ")" ) ")" )))) ;