:: QUIN_1 semantic presentation begin definitionlet "a", "b", "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func :::"delta"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_hidden :::"set"::: ) equals :: QUIN_1:def 1 (Set (Set "(" "b" ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) "a" ")" ) ($#k3_xcmplx_0 :::"*"::: ) "c" ")" )); end; :: deftheorem defines :::"delta"::: QUIN_1:def 1 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c")) ")" )))); registrationlet "a", "b", "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_quin_1 :::"delta"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#v1_xcmplx_0 :::"complex"::: ) ; end; registrationlet "a", "b", "c" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_quin_1 :::"delta"::: ) "(" "a" "," "b" "," "c" ")" ) -> ($#v1_xreal_0 :::"real"::: ) ; end; definitionlet "a", "b", "c" be ($#m1_subset_1 :::"Real":::); :: original: :::"delta"::: redefine func :::"delta"::: "(" "a" "," "b" "," "c" ")" -> ($#m1_subset_1 :::"Real":::); end; theorem :: QUIN_1:1 (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"::: ) ))) "holds" (Bool (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"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "b")) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 4) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" )))) ; theorem :: QUIN_1:2 (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_xxreal_0 :::">"::: ) (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 (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"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:3 (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_xxreal_0 :::">"::: ) (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 (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"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:4 (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_xxreal_0 :::"<"::: ) (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 (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"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:5 (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_xxreal_0 :::"<"::: ) (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 (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"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:6 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (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"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:7 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (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"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:8 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (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"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:9 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (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"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:10 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 (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"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 (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"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:12 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 (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"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:13 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "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 (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"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) & (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:14 (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 (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"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:15 (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 (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"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Bool "not" (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))))) "holds" (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )))) ; theorem :: QUIN_1:16 (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"::: ) ))) "holds" (Bool (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"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "x")) ($#k6_xcmplx_0 :::"-"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ")" ) ")" )))) ; theorem :: QUIN_1:17 (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_xxreal_0 :::"<"::: ) (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 (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )))) ; theorem :: QUIN_1:18 (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_xxreal_0 :::"<"::: ) (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 "(" (Bool (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"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) ")" ) ")" )) ; theorem :: QUIN_1:19 (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_xxreal_0 :::"<"::: ) (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 "(" (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) "or" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) ")" ) "iff" (Bool (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"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ; theorem :: QUIN_1:20 (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 (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"))) ($#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 :: QUIN_1:21 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (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"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_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_xxreal_0 :::">"::: ) (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"::: ) ))) "holds" (Bool "(" (Bool (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"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (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 :: QUIN_1:23 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" (Set "(" (Set "(" (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "b")) ")" ) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k1_quin_1 :::"delta"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (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"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: QUIN_1:24 (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_xxreal_0 :::"<"::: ) (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"::: ) ))) "holds" (Bool "(" (Bool (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"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (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 :: QUIN_1:25 (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_xxreal_0 :::">"::: ) (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 (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::">"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )))) ; theorem :: QUIN_1:26 (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_xxreal_0 :::">"::: ) (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 "(" (Bool (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"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) )) "iff" (Bool "(" (Bool (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x"))) & (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) ")" ) ")" )) ; theorem :: QUIN_1:27 (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_xxreal_0 :::">"::: ) (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 "(" (Bool "(" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::"<"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) "or" (Bool (Set (Var "x")) ($#r1_xxreal_0 :::">"::: ) (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")) ")" ")" ) ")" ) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set "(" (Num 2) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "a")) ")" ))) ")" ) "iff" (Bool (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"))) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) ;