Quelle polar.prf
Sprache: Lisp
(polarnil 3297457117"" (assert ) (("" (typepred "pi" ) (("" (assert ) nil nil )) nil )) nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"bool" reals nil )"posreal" trig_basic "trig/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nzcomplex" nil )"nzreal" real_typesnil ))nil 3294310508"" (skosimp)"" (lemma "complex_is_Re_Im" ("z" "z!1" ))"" (expand "conjugate" )"" (name-replace "R" "Re(z!1)" )"" (name-replace "II" "Im(z!1)" )"" (replace -1)"" (hide -1)"" (assert )"" (rewrite "sq.sq_rew" )"" (rewrite "sq.sq_rew" )"" (lemma "i_axiom" )"" (rewrite "associative_mult" :dir rl)"" (expand "sq" -1)"" (replace -1) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil arithmetic nil )"complex" nil )"[T, T -> boolean]" equalities nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"real" reals nil )"complex" nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )nil number_fields nil )"real" reals nil )nil complex_types nil )"odd_int" integers nil )"nzcomplex" nil )nil sq "reals/" )"{y | EXISTS x: z = x + y * i}" complex_types nil )"complex" arithmetic nil )"complex" nil )"real" complex_types nil )"real" complex_types nil ))nil 3385303712"" (skosimp)"" (expand "abs" )"" (lemma "complex_is_Re_Im" ("z" "z!1" ))"" (name-replace "DRL100" "conjugate(z!1)" )"" "DRL101" "sqrt(sq.sq(Im(z!1)) + sq.sq(Re(z!1)))" )"" (replace -1)"" (hide -1)"" (expand "DRL100" )"" (expand "conjugate" )"" (rewrite "associative_mult" 1 :dir rl)"" (rewrite "associative_mult" 1 :dir rl)"" (rewrite "associative_mult" 1 :dir rl)"" (rewrite "i_axiom" )"" (expand "DRL101" )"" expand "sq" )"" rewrite "associative_mult" )"" (rewrite "minus_add" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" polar nil )"complex" arithmetic nil )"[T, T -> boolean]" equalities nil )"complex" polar nil )nil number_fields nil )"{nnz: nnreal | nnz * nnz = sq.sq(Im(z!1)) + sq.sq(Re(z!1))}" nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"complex" nil )"real" reals nil )"nzcomplex" nil )"odd_int" integers nil )nil complex_types nil )"real" reals nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"complex" complex_types nil )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )"nnreal" nil )"complex" nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"complex" nil ))nil 3385304274"" (skosimp)"" (rewrite "abs_def" )"" (rewrite "Im_real" )"" (rewrite "Re_real" )"" (expand "sq" 1 1) (("" (rewrite "sqrt_sq_abs" ) nil nil ))nil ))nil ))nil ))nil ))nil )"complex" nil )nil polar nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"[number_field -> boolean]" reals nil )nil reals nil )"complex" nil )nil arithmetic nil )nil sqrt "reals/" )"nonneg_real" sq "reals/" )nil arithmetic nil ))nil 3596359128"" (skeep)"" (rewrite "abs_def" )"" (rewrite "Re_imag" )"" (rewrite "Im_imag" )"" (case "sq.sq(0) = 0" )"1" (replaces -1)"1" (assert )"1" (lemma "sqrt_sq" )"1" (inst - "real_defs.abs(r)" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"complex" nil )nil polar nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"complex" complex_types nil )"complex" nil )nil arithmetic nil )nil sqrt "reals/" )nil sq "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil arithmetic nil ))nil 3294771107"" (skosimp)"" (expand "abs" )"" (lemma "nz_sq_abs_pos" ("n0z" "n0z!1" ))"" (lemma "sqrt_pos" ("px" "n0z!1 * conjugate(n0z!1)" ))"1" (propax) nil nil )"2" (expand "conjugate" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"nnreal" polar nil )"complex" arithmetic nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil sqrt "reals/" )"complex" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"complex" nil )"real" complex_types nil )"real" complex_types nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil ))nil 3294771228"" (skosimp)"" (prop)"1" (replace -2) (("1" (grind) nil nil )) nil )"2" (lemma "abs_nzcomplex" ("n0z" "z!1" ))"1" (propax) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"complex" nil )"complex" nil )"nnreal" polar nil )nil sqrt "reals/" )"complex" arithmetic nil )nil polar nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil ))nil 3295007153"" (skosimp)"" (prop)"1" (typepred "abs(z!1)" )"1" (expand ">=" )"1" (expand "<=" )"1" (split)"1" (lemma "abs_nz_iff_nz" ("z" "z!1" ))"1" (assert ) nil nil )) nil )"2" (hide -1)"2" (expand "abs" )"2" (rewrite "sq_abs_def" )"2" (rewrite "sq.sq_rew" )"2" (rewrite "sq.sq_rew" )"2" (rewrite "complex_is_0_Re_Im" 1)"2" (typepred "sq.sq(Im(z!1))" )"2" (typepred "sq.sq(Re(z!1))" )"2" "sqrt_eq" "nny" "sq.sq(Im(z!1)) + sq.sq(Re(z!1))" "nnz" "0" ))"2" rewrite "sqrt_0" )"2" replace -1 -4)"2" "2" "sq.sq_nz_pos" )"2" "Re(z!1) = 0" )"1" "Im(z!1)" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" "Re(z!1)" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (expand "abs" )"2" (rewrite "zero_times1" )"2" (rewrite "sqrt_0" ) nil nil )) nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )nil polar nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil sq "reals/" )nil arithmetic nil )nil sqrt "reals/" )nil sq "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil reals nil )"complex" polar nil )"boolean" notequal nil )nil sq "reals/" )nil sqrt "reals/" )"nnreal" nil )"nonneg_real" sq "reals/" )nil real_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" nil )"real" reals nil )"complex" nil )nil arithmetic nil )"bool" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )nil real_types nil )"nnreal" polar nil )"complex" arithmetic nil )nil number_fields_bis nil ))nil 3294998991"" (skosimp)"" (expand "abs" )"" (rewrite "conjugate_neg" )"" (rewrite "neg_times_neg" ) nil nil )) nil ))nil ))nil )"complex" nil )"nnreal" polar nil )"complex" nil )"complex" arithmetic nil )nil number_fields_bis nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil arithmetic nil ))nil 3294697248"" (expand "abs" )"" (skolem 1 ("a" "b" ))"" (lemma "sq_abs_nonneg" ("z" "a" ))"" (lemma "sq_abs_nonneg" ("z" "b" ))"" (lemma "sq_abs_nonneg" ("z" "a*b" ))"" (rewrite "sqrt_times" :dir rl)"1" (assert )"1" (rewrite "conjugate_times" ) nil nil )) nil )"2" (assert )"2" (expand "conjugate" ) (("2" (propax) nil nil ))nil ))nil )"3" (expand "conjugate" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil arithmetic nil )"(total_order?[real])" nil )nil sqrt "reals/" )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"complex" arithmetic nil )nil arithmetic nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"nnreal" polar nil )"complex" nil ))nil 3294998917"" (skosimp) (("" (rewrite "abs_is_0" ) nil nil )) nil )nil polar nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil ))nil 3294999199"" (skosimp)"" (expand "abs" )"" (rewrite "conjugate_inv" )"" (lemma "conjugate_nz" ("n0z" "n0z!1" ))"" (rewrite "div_times" )"" (lemma "nz_sq_abs_pos" ("n0z" "n0z!1" ))"" (rewrite "sqrt_div" )"" (expand "conjugate" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzcomplex" complex_types nil )"nnreal" polar nil )nil arithmetic nil )nil arithmetic nil )nil sqrt "reals/" )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"nzreal" nil )"posreal" sqrt "reals/" )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil )nil arithmetic nil )"nzcomplex" complex_types nil )"posint" nil )"odd_int" integers nil )"complex" nil )nil number_fields_bis nil )nil number_fields nil )"complex" arithmetic nil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil arithmetic nil ))nil 3294999065"" (skosimp)"" (lemma "div_def" ("y" "z!1" "n0x" "n0z!1" ))"" (lemma "abs_mult" ("z1" "z!1" "z2" "1/n0z!1" ))"1" (rewrite "abs_inv" -1) (("1" (assert ) nil nil )) nil )"2" (lemma "real_is_complex" ("x" "1" ))"2" (rewrite "closed_divides" ) nil nil )) nil ))nil ))nil ))nil )nil number_fields nil )nil complex_types nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil number_fields nil )nil polar nil )"nzreal" nil )"complex" nil )"real" reals nil )"complex" nil )"real" reals nil )"nzcomplex" complex_types nil )nil polar nil )"[numfield, nznum -> numfield]" number_fields nil ))nil 3307889278"" (skolem 1 ("a" "b" ))"" (expand "abs" )"" (lemma "sq_abs_nonneg" ("z" "a" ))"" (lemma "sq_abs_nonneg" ("z" "b" ))"" (lemma "sq_abs_nonneg" ("z" "a+b" ))"" (case "real_pred(a * conjugate(a))" )"1" (case "real_pred(b * conjugate(b))" )"1" (case "real_pred((a+b) * conjugate(a+b))" )"1" (name "A2" "a * conjugate(a)" )"1" (replace -1)"1" (name "B2" "b * conjugate(b)" )"1" (replace -1)"1" (name "AB2" "(a+b) * conjugate(a+b)" )"1" (replace -1)"1" "conjugate(a + b) * a + conjugate(a + b) * b = AB2" )"1" rewrite "sq_le" 1 :dir rl)"1" rewrite "sqrt.sq_sqrt" )"1" rewrite "sq.sq_plus" )"1" rewrite "sqrt.sq_sqrt" )"1" rewrite "sqrt.sq_sqrt" )"1" rewrite "sqrt.sqrt_times" "1" rewrite "conjugate_plus" )"1" rewrite "distributive" "1" "commutative_mult" )"1" "a" "conjugate(a)" )"1" "b" "conjugate(b)" )"1" replace "1" replace "1" replace "1" replace "1" "1" "DRL" "conjugate(a) * b + conjugate(b) * a" )"1" "A2 + conjugate(a) * b + conjugate(b) * a + B2 = A2+B2+DRL" )"1" case "real_pred(DRL)" )"1" "1" replace "1" assert )"1" case "A2*B2>=0" )"1" "both_sides_plus_le2" "z" "A2+B2" "x" "DRL" "y" "2*sqrt(A2 * B2)" ))"1" case "DRL<=2 * sqrt(A2 * B2)" )"1" assert )nil nil )"2" "2" "CA" "conjugate(a)" )"2" "CB" "conjugate(b)" )"2" "complex_is_Re_Im" "z" "a" ))"2" "complex_is_Re_Im" "z" "b" ))"2" replace "2" replace "2" expand "CA" )"2" expand "CB" )"2" expand "conjugate" )"2" "DRL = 2*(Re(a)*Re(b)+Im(a)*Im(b))" )"1" "both_sides_times_pos_le1" "pz" "2" "x" "Re(a) * Re(b) + Im(a) * Im(b)" "y" "sqrt(A2 * B2)" ))"1" replace "1" "1" "reals.closed_divides" "x" "2 * (Re(a) * Re(b) + Im(a) * Im(b))" "n0z" "2" ))"1" rewrite "times_div1" "1" rewrite "div_cancel1" "1" case "Im(a) * Im(b) + Re(a) * Re(b) < 0" )"1" assert )nil nil )"2" rewrite "sq_le" "2" rewrite "sq_sqrt" )"2" expand "B2" "2" rewrite "sq_abs_def" "2" "DRL_B" "(Im(b) * Im(b) + Re(b) * Re(b))" )"2" expand "A2" )"2" "sq_abs_def" "z" "a" ))"2" "conjugate(a)" "DRL_B" )"2" replace "2" rewrite "associative_mult" "2" "conjugate(a)" "a" )"2" replace "2" replace "2" expand "DRL_B" )"2" expand "sq" )"2" assert )"2" "IA" "Im(a)" )"2" replace "2" "IB" "Im(b)" )"2" replace "2" "RB" "Re(b)" )"2" replace "2" "RA" "Re(a)" )"2" replace "2" "DRL10" "IA * IA * IB * IB " )"2" "DRL11" "RA * RA * RB * RB " )"2" assert )"2" "both_sides_plus_le2" "z" "DRL10 + DRL11" "x" "2 * (IA * IB * RA * RB)" "y" "IA * IA * RB * RB + IB * IB * RA * RA" ))"2" replace "2" "2" case "IA*IB >= -(RA*RB)" )"1" "1" "trichotomy" "x" "IA*RB-RA*IB" ))"1" "1" "sq_lt" "nna" "0" "nnb" "IA * RB - RA * IB" ))"1" assert )"1" expand "sq" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "sq_eq" "nna" "IA * RB - RA * IB" "nnb" "0" ))"1" assert )"1" expand "sq" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"3" "sq_lt" "nna" "0" "nnb" "-(IA * RB - RA * IB)" ))"1" assert )"1" rewrite "sq.sq_neg" )"1" expand "sq" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" rewrite "associative_mult" "2" rewrite "associative_mult" "2" rewrite "associative_mult" "2" "i_axiom" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "reals.closed_plus" "x" "A2" "y" "B2" ))"2" nil nil ))nil ))nil )"3" "reals.closed_times" "x" "A2" "y" "B2" ))"3" assert )nil nil ))nil ))nil )"2" "2" expand ">=" )"2" expand "<=" "2" "1" "both_sides_times_pos_le1" "pz" "B2" "x" "0" "y" "A2" ))"1" assert )"1" rewrite "zero_times1" )nil nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "reals.closed_times" "x" "A2" "y" "B2" ))"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "DRL" )"2" "conjugate(a) * b + conjugate(b) * a = AB2 - A2 - B2" )"1" assert )"1" "1" "reals.closed_minus" )"1" "1" "reals.closed_minus" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "both_sides_minus1" )"2" "A2 + conjugate(a) * b + conjugate(b) * a + B2" "AB2" "A2+B2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "DRL" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "AB2" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name-replace "APB" "a + b" )"2" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" nil )"nnreal" polar nil )"[number_field -> boolean]" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" arithmetic nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"nnreal" nil )nil sq "reals/" )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil real_types nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"(total_order?[real])" nil )nil sq "reals/" )"nnreal" nil )nil arithmetic nil )nil number_fields nil )nil reals nil )nil reals nil )"bool" reals nil )nil arithmetic nil )"complex" polar nil )"real" reals nil )"nzcomplex" nil )"odd_int" integers nil )nil complex_types nil )nil real_props nil )"bool" reals nil )nil real_types nil )nil number_fields nil )nil number_fields_bis nil )"complex" nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )nil arithmetic nil )"complex" polar nil )nil number_fields nil )"real" polar nil )"complex" nil )nil arithmetic nil )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_axioms nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"complex" nil )"nonneg_real" sq "reals/" )"complex" polar nil )"real" reals nil )"real" reals nil )nil number_fields_bis nil )nil reals nil )"boolean" notequal nil )nil reals nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"complex" polar nil )"real" complex_types nil )"real" complex_types nil )nil real_props nil )nil number_fields_bis nil )"complex" polar nil )nil reals nil )nil number_fields_bis nil )"complex" polar nil )nil number_fields nil )nil sqrt "reals/" )nil sqrt "reals/" )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"complex" nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil ))nil )nil 3294999713"" (skolem 1 ("a" "b" ))"" (expand "abs" )"" (lemma "sq_abs_nonneg" ("z" "a" ))"" (lemma "sq_abs_nonneg" ("z" "b" ))"" (lemma "sq_abs_nonneg" ("z" "a+b" ))"" (case "real_pred(a * conjugate(a))" )"1" (case "real_pred(b * conjugate(b))" )"1" (case "real_pred((a+b) * conjugate(a+b))" )"1" (name "A2" "a * conjugate(a)" )"1" (replace -1)"1" (name "B2" "b * conjugate(b)" )"1" (replace -1)"1" (name "AB2" "(a+b) * conjugate(a+b)" )"1" (replace -1)"1" "conjugate(a + b) * a + conjugate(a + b) * b = AB2" )"1" rewrite "sq_le" 1 :dir rl)"1" rewrite "sq_sqrt" )"1" rewrite "sq.sq_plus" )"1" rewrite "sq_sqrt" )"1" rewrite "sq_sqrt" )"1" rewrite "sqrt_times" "1" rewrite "conjugate_plus" )"1" rewrite "distributive" "1" "commutative_mult" )"1" "a" "conjugate(a)" )"1" "b" "conjugate(b)" )"1" replace "1" replace "1" replace "1" replace "1" "1" "DRL" "conjugate(a) * b + conjugate(b) * a" )"1" "A2 + conjugate(a) * b + conjugate(b) * a + B2 = A2+B2+DRL" )"1" case "real_pred(DRL)" )"1" "1" replace "1" assert )"1" case "A2*B2>=0" )"1" "both_sides_plus_le2" "z" "A2+B2" "x" "DRL" "y" "2*sqrt(A2 * B2)" ))"1" case "DRL<=2 * sqrt(A2 * B2)" )"1" assert )nil nil )"2" "2" "CA" "conjugate(a)" )"2" "CB" "conjugate(b)" )"2" "complex_is_Re_Im" "z" "a" ))"2" "complex_is_Re_Im" "z" "b" ))"2" replace "2" replace "2" expand "CA" )"2" expand "CB" )"2" expand "conjugate" )"2" "DRL = 2*(Re(a)*Re(b)+Im(a)*Im(b))" )"1" "both_sides_times_pos_le1" "pz" "2" "x" "Re(a) * Re(b) + Im(a) * Im(b)" "y" "sqrt(A2 * B2)" ))"1" replace "1" "1" "reals.closed_divides" "x" "2 * (Re(a) * Re(b) + Im(a) * Im(b))" "n0z" "2" ))"1" rewrite "times_div1" "1" rewrite "div_cancel1" "1" case "Im(a) * Im(b) + Re(a) * Re(b) < 0" )"1" assert )nil nil )"2" rewrite "sq_le" "2" rewrite "sq_sqrt" )"2" expand "B2" "2" rewrite "sq_abs_def" "2" "DRL_B" "(Im(b) * Im(b) + Re(b) * Re(b))" )"2" expand "A2" )"2" "sq_abs_def" "z" "a" ))"2" "conjugate(a)" "DRL_B" )"2" replace "2" rewrite "associative_mult" "2" "conjugate(a)" "a" )"2" replace "2" replace "2" expand "DRL_B" )"2" expand "sq" )"2" assert )"2" "IA" "Im(a)" )"2" replace "2" "IB" "Im(b)" )"2" replace "2" "RB" "Re(b)" )"2" replace "2" "RA" "Re(a)" )"2" replace "2" "DRL10" "IA * IA * IB * IB " )"2" "DRL11" "RA * RA * RB * RB " )"2" assert )"2" "both_sides_plus_le2" "z" "DRL10 + DRL11" "x" "2 * (IA * IB * RA * RB)" "y" "IA * IA * RB * RB + IB * IB * RA * RA" ))"2" replace "2" "2" case "IA*IB >= -(RA*RB)" )"1" "1" "trichotomy" "x" "IA*RB-RA*IB" ))"1" "1" "sq_lt" "nna" "0" "nnb" "IA * RB - RA * IB" ))"1" assert )"1" expand "sq" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "sq_eq" "nna" "IA * RB - RA * IB" "nnb" "0" ))"1" assert )"1" expand "sq" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"3" "sq_lt" "nna" "0" "nnb" "-(IA * RB - RA * IB)" ))"1" assert )"1" rewrite "sq.sq_neg" )"1" expand "sq" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" rewrite "associative_mult" "2" rewrite "associative_mult" "2" rewrite "associative_mult" "2" "i_axiom" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "reals.closed_plus" "x" "A2" "y" "B2" ))"2" nil nil ))nil ))nil )"3" "reals.closed_times" "x" "A2" "y" "B2" ))"3" assert )nil nil ))nil ))nil )"2" "2" expand ">=" )"2" expand "<=" "2" "1" "both_sides_times_pos_le1" "pz" "B2" "x" "0" "y" "A2" ))"1" assert )"1" rewrite "zero_times1" )nil nil ))nil )"2" assert )nil nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "reals.closed_times" "x" "A2" "y" "B2" ))"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "DRL" )"2" "conjugate(a) * b + conjugate(b) * a = AB2 - A2 - B2" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "DRL" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "AB2" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name-replace "APB" "a + b" )"2" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" arithmetic nil )nil sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil sq "reals/" )nil arithmetic nil )nil arithmetic nil )nil complex_types nil )nil number_fields_bis nil )nil arithmetic nil )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )"nonneg_real" sq "reals/" )nil number_fields_bis nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil number_fields_bis nil )nil sqrt "reals/" )nil sqrt "reals/" )nil arithmetic nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil ))nil 3596297605"" (skeep)"" (lemma "abs_triangle" )"" (inst - "z2" "z1-z2" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil polar nil )"real" reals nil )"(total_order?[real])" nil )"nnreal" nil )"complex" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"complex" nil ))nil 3307886891"" (skosimp)"" (typepred "abs(z!1)" )"" (expand "abs" )"" (expand "conjugate" )"" (lemma "complex_is_Re_Im" ("z" "z!1" ))"" (name-replace "X" "Re(z!1)" )"" (name-replace "Y" "Im(z!1)" )"" (replace -1)"" (hide -1)"" "DRL1" "X * (X + Y * i) - Y * i * (X + Y * i)" )"" (replace -1)"" (rewrite "Re_real" 1)"1" (rewrite "Im_real" 1)"1" (rewrite "zero_times1" 1)"1" rewrite "zero_times1" 1)"1" rewrite "sq.sq_rew" 1)"1" rewrite "sqrt.sq_sqrt" )nil nil ))nil ))nil ))nil ))nil )"2" (hide -2 2)"2" (rewrite "sq.sq_rew" )"2" rewrite "sq.sq_rew" )"2" rewrite "associative_mult" "2" rewrite "i_axiom" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" polar nil )nil real_types nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"complex" nil )"real" complex_types nil )"real" complex_types nil )"real" reals nil )"complex" arithmetic nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"complex" nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil real_types nil )nil arithmetic nil )"nnreal" nil )nil number_fields_bis nil )nil sqrt "reals/" )nil sq "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )nil arithmetic nil )"nzcomplex" nil )"odd_int" integers nil )"nonneg_real" sq "reals/" )nil number_fields nil )"real" reals nil )nil complex_types nil )"complex" nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil arithmetic nil ))nil )nil 3297714813"" (skosimp)"" (typepred "abs(z!1)" )"" (expand "abs" )"" (expand "conjugate" )"" (lemma "complex_is_Re_Im" ("z" "z!1" ))"" (name-replace "X" "Re(z!1)" )"" (name-replace "Y" "Im(z!1)" )"" (replace -1)"" (hide -1)"" "DRL1" "X * (X + Y * i) - Y * i * (X + Y * i)" )"" (replace -1)"" (rewrite "Re_real" 1)"1" (rewrite "Im_real" 1)"1" (rewrite "zero_times1" 1)"1" rewrite "zero_times1" 1)"1" rewrite "sq_rew" 1)"1" (rewrite "sq_sqrt" 1) nil nil ))nil ))nil ))nil ))nil )"2" (hide -2 2)"2" (rewrite "sq_rew" )"2" rewrite "sq_rew" )"2" rewrite "associative_mult" "2" rewrite "i_axiom" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )"complex" arithmetic nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil arithmetic nil )nil number_fields_bis nil )nil sqrt "reals/" )nil sq "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )nil arithmetic nil )"nonneg_real" sq "reals/" )nil complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil arithmetic nil ))nil 3385194591"" (expand "abs" )"" (expand "conjugate" )"" (lemma "Re_imag" ("x" "1" ))"" (lemma "Im_imag" ("x" "1" ))"" (rewrite "identity_mult" )"" (replace -1)"" (replace -2)"" (rewrite "zero_times1" )"" (rewrite "identity_mult" )"" (rewrite "i_axiom" )"" (rewrite "sqrt_1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" nil )"real" complex_types nil )"real" complex_types nil )"complex" arithmetic nil )nil arithmetic nil )nil number_fields_bis nil )"nzcomplex" nil )"odd_int" integers nil )nil complex_types nil )nil sqrt "reals/" )nil number_fields nil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"complex" complex_types nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"nnreal" polar nil ))nil 3294311190 ("" (skosimp) (("" (assert ) nil nil )) nil )"real" complex_types nil )"real" complex_types nil )"(strict_total_order?[real])" real_props nil )"complex" nil ))nil 3294311658"" (skosimp*)"" (lemma "atan2_ge_0_lt_2pi" ("x" "Re(z!1)" "y" "Im(z!1)" ))"" (split -1)"1" (flatten)"1" (assert )"1" (lemma "trichotomy" ("x" "Re(z!1)" ))"1" (split -1)"1" "atan2_quad4" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (assert ) nil nil )) nil )"2" "atan2_is_3pi2" ("x" "Re(z!1)" "y" "Im(z!1)" ))"2" (assert ) nil nil )) nil )"3" "atan2_quad3" ("x" "Re(z!1)" "y" "Im(z!1)" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil atan2 "trig/" )nil real_axioms nil )nil atan2_props "trig/" )nil atan2_props "trig/" )nil atan2_props "trig/" )nil booleans nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )"nzcomplex" complex_types nil )"posreal" nil )"(total_order?[real])" nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"(strict_total_order?[real])" real_props nil )"nzcomplex" complex_types nil )"posreal" nil )"nzcomplex" nil )"nzreal" real_typesnil )"complex" nil )"real" reals nil )"complex" nil ))nil 3294839112"" (skosimp)"" (lemma "atan2_ge_0_lt_2pi" ("x" "Re(z!1)" "y" "Im(z!1)" ))"" (lemma "complex_is_ne_0_Re_Im" ("z" "z!1" ))"" (assert ) (("" (replace -1) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil atan2 "trig/" )"real" complex_types nil )"real" complex_types nil )"(strict_total_order?[real])" real_props nil )nil arithmetic nil )"complex" nil ))nil 3297458289"" (skosimp)"" (lemma "atan2_is_0" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (lemma "atan2_is_pi2" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (lemma "atan2_is_pi" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (lemma "atan2_quad1" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (lemma "atan2_quad2" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (assert )"1" (case-replace "Im(z!1)=0" )"1" (assert )"1" (lemma "trichotomy" ("x" "Re(z!1)" ))"1" (split -1)"1" (assert ) nil nil )"2" (assert )"2" (replace -1)"2" (assert )"2" "complex_is_ne_0_Re_Im" "z" "z!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "trichotomy" ("x" "Re(z!1)" ))"2" (split -1)"1" (assert )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert )"3" (flatten) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "complex_is_ne_0_Re_Im" ("z" "z!1" ))"2" (assert )"2" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil atan2_props "trig/" )"real" complex_types nil )"real" complex_types nil )nil atan2_props "trig/" )nil atan2_props "trig/" )nil real_axioms nil )nil arithmetic nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzcomplex" complex_types nil )"posreal" nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"(strict_total_order?[real])" real_props nil )"nzcomplex" nil )"nzreal" real_typesnil )nil atan2_props "trig/" )nil atan2_props "trig/" )"complex" nil ))nil 3295019855"" (skosimp*)"" (typepred "arg(n0z!1)" )"" (lemma "complex_is_ne_0_Re_Im" ("z" "n0z!1" ))"" (assert )"" (lemma "atan2_is_0" ("x" "Re(n0z!1)" "y" "Im(n0z!1)" ))"1" (case-replace "Re(n0z!1) > 0 AND Im(n0z!1) = 0" )"1" (flatten)"1" (replace -2)"1" (expand "arg" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (replace 1)"2" (flatten)"2" (split 3)"1" (expand "arg" )"1" (case-replace "Im(n0z!1) < 0" )"1" "atan2_ge_0_lt_2pi" "x" "Re(n0z!1)" "y" "Im(n0z!1)" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil complex_types nil )"boolean" notequal nil )"argrng" polar nil )nil polar nil )"bool" reals nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"real" complex_types nil )"real" complex_types nil )"(total_order?[real])" nil )"nzreal" real_typesnil )"nzcomplex" nil )"(strict_total_order?[real])" real_props nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )nil atan2 "trig/" )"complex" nil )"nzcomplex" complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"[bool, bool -> bool]" booleans nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil atan2_props "trig/" )nil arithmetic nil )"complex" nil ))nil 3295013793"" (skosimp)"" (case-replace "z!1=0" )"1" (expand "arg" )"1" (rewrite "Re_real" )"1" (rewrite "Im_real" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "arg_is_0_nz" ("n0z" "z!1" ))"1" (case-replace "arg(z!1) = 0" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (replace 1)"2" (flatten)"2" (assert )"2" (flatten)"2" (expand ">=" )"2" (expand "<=" )"2" (split -1)"1" (assert ) nil nil )"2" (replace -1 * rl)"2" (lemma "complex_is_Re_Im" ("z" "z!1" ))"2" (replace -2 * rl)"2" replace -3)"2" assert )"2" rewrite "zero_times1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil arithmetic nil )"(total_order?[real])" nil )nil arithmetic nil )"argrng" polar nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"bool" reals nil )nil polar nil )"real" complex_types nil )"real" complex_types nil )"(strict_total_order?[real])" real_props nil )"complex" nil )nil number_fields_bis nil )"complex" complex_types nil )nil arithmetic nil )"(strict_total_order?[real])" real_props nil )nil polar nil )"boolean" notequal nil )nil complex_types nil )"complex" nil ))nil 3295019935"" (skosimp)"" (typepred "arg(z!1)" )"" (expand "arg" )"" (case-replace "z!1=0" )"1" (rewrite "Im_real" ) (("1" (assert ) nil nil )) nil )"2" (assert )"2" (case-replace "Im(z!1) < 0" )"1" "atan2_ge_0_lt_2pi" "x" "Re(z!1)" "y" "Im(z!1)" ))"1" (assert ) nil nil )) nil )"2" (assert )"2" "atan2_is_pi2" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (propax) nil nil )"2" (lemma "complex_is_ne_0_Re_Im" ("z" "z!1" ))"2" (assert )"2" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"argrng" polar nil )nil polar nil )"bool" reals nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"real" complex_types nil )"posreal" nil )"nzcomplex" complex_types nil )"(total_order?[real])" nil )"nzreal" real_typesnil )"nzcomplex" nil )"(strict_total_order?[real])" real_props nil )nil arithmetic nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"complex" nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )nil atan2 "trig/" )nil atan2_props "trig/" )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"complex" nil ))nil 3295019473"" (skosimp)"" (case-replace "z!1=0" )"1" (expand "arg" )"1" (rewrite "Re_real" ) (("1" (assert ) nil nil )) nil )) nil )"2" (lemma "complex_is_ne_0_Re_Im" ("z" "z!1" ))"2" (assert )"2" (typepred "arg(z!1)" )"2" (lemma "atan2_is_pi" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" "atan2_ge_0_lt_2pi" "x" "Re(z!1)" "y" "Im(z!1)" ))"1" (replace -5 -1)"1" (flatten -1)"1" (expand "arg" )"1" (case-replace "Im(z!1) < 0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (split -3)"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil arithmetic nil )"(strict_total_order?[real])" real_props nil )"real" complex_types nil )"argrng" polar nil )"real" complex_types nil )nil atan2_props "trig/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"(total_order?[real])" nil )"real" reals nil )"complex" nil )"nzreal" real_typesnil )"nzcomplex" nil )"posreal" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"(total_order?[real])" nil )nil atan2 "trig/" )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"bool" reals nil )nil polar nil )nil arithmetic nil )"complex" nil ))nil 3297511933"" (skosimp)"" (case-replace "z!1=0" )"1" (expand "arg" )"1" (rewrite "Im_real" ) (("1" (assert ) nil nil )) nil )) nil )"2" (typepred "arg(z!1)" )"2" (lemma "complex_is_ne_0_Re_Im" ("z" "z!1" ))"2" (assert )"2" "atan2_ge_0_lt_2pi" ("x" "Re(z!1)" "y" "Im(z!1)" ))"2" (replace -2 -1)"2" (flatten -1)"2" (expand "arg" )"2" "atan2_is_3pi2" "x" "Re(z!1)" "y" "Im(z!1)" ))"1" (case-replace "Im(z!1) < 0" )"1" (case-replace "Re(z!1)=0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (split -3)"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"nzreal" real_typesnil )"nzcomplex" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil arithmetic nil )"nzcomplex" complex_types nil )"nzreal" nil )"real" complex_types nil )"(strict_total_order?[real])" real_props nil )"argrng" polar nil )nil arithmetic nil )nil atan2 "trig/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil atan2_props "trig/" )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"posreal" nil )"nzcomplex" complex_types nil )"(total_order?[real])" nil )"complex" nil )"real" reals nil )"posreal" nil )"(total_order?[real])" nil )"real" complex_types nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"bool" reals nil )nil polar nil )"complex" nil ))nil 3297512359"" (skosimp)"" (typepred "arg(z!1)" )"" (expand "arg" )"" (case-replace "z!1=0" )"1" (rewrite "Im_real" ) (("1" (assert ) nil nil )) nil )"2" (assert )"2" (lemma "atan2_is_3pi2" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (lemma "atan2_quad3" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" "atan2_quad4" ("x" "Re(z!1)" "y" "Im(z!1)" ))"1" (case-replace "Im(z!1) < 0" )"1" (lemma "trichotomy" ("x" "Re(z!1)" ))"1" (split -1)"1" (assert )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil )"2" (replace -1) (("2" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" (assert )"2" (hide 2 3 4)"2" "complex_is_ne_0_Re_Im" ("z" "z!1" ))"2" (assert )"2" "atan2_ge_0_lt_2pi" "x" "Re(z!1)" "y" "Im(z!1)" ))"2" replace -2 -1)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "complex_is_ne_0_Re_Im" ("z" "z!1" ))"2" (assert )"2" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"argrng" polar nil )nil polar nil )"bool" reals nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"nzreal" real_typesnil )"nzcomplex" nil )"(strict_total_order?[real])" real_props nil )nil arithmetic nil )nil atan2_props "trig/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil atan2_props "trig/" )nil real_axioms nil )"real" reals nil )"posreal" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"complex" nil )"(strict_total_order?[real])" real_props nil )"nzcomplex" complex_types nil )"posreal" nil )nil atan2_props "trig/" )nil arithmetic nil )"complex" nil ))nil 3297607614"" (skosimp*)"" (case-replace "z!1=0" )"1" (expand "arg" )"1" (rewrite "Im_real" ) (("1" (assert ) nil nil )) nil )) nil )"2" (typepred "arg(z!1)" )"2" (expand "<=" )"2" (split -2)"1" (replace -1)"1" (lemma "trichotomy" ("x" "arg(z!1)" ))"1" (split -1)"1" (hide -3)"1" (lemma "complex_is_ne_0_Re_Im" ("z" "z!1" ))"1" (assert )"1" (expand "arg" )"1" "atan2_ge_0_lt_2pi" "x" "Re(z!1)" "y" "Im(z!1)" ))"1" (replace -2)"1" "1" "trichotomy" ("x" "Im(z!1)" ))"1" "1" (propax) nil nil )"2" assert )"2" replace -1)"2" expand "atan2" )"2" rewrite "atan_0" )"2" case "Re(z!1)>0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "arg_is_0_nz" ("n0z" "z!1" ))"1" (assert )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil )"3" (lemma "arg_lt_0" ("z" "z!1" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (replace -1)"2" (lemma "arg_is_pi" ("z" "z!1" ))"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil arithmetic nil )"(strict_total_order?[real])" real_props nil )"argrng" polar nil )nil polar nil )nil arithmetic nil )"complex" nil )"posreal" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"(total_order?[real])" nil )"real" atan2 "trig/" )"complex" nil )nil atan "trig/" )"{y | EXISTS x: z = x + y * i}" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil atan2 "trig/" )"(strict_total_order?[real])" real_props nil )"real" complex_types nil )"real" complex_types nil )"nzreal" real_typesnil )"nzcomplex" nil )nil complex_types nil )"boolean" notequal nil )nil polar nil )nil polar nil )nil real_axioms nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"bool" reals nil )nil polar nil )"complex" nil ))nil 3297512850"" (skosimp*)"" (typepred "arg(z!1)" )"" (expand "<=" )"" (lemma "arg_p_lt_pi" ("z" "z!1" ))"" (lemma "arg_is_pi" ("z" "z!1" ))"" (split 1)"1" (flatten 1)"1" (split -5)"1" (assert ) nil nil )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (flatten 1)"2" (split -1)"1" (assert ) nil nil )"2" (flatten -1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"argrng" polar nil )nil polar nil )"bool" reals nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil polar nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" complex_types nil )"nzcomplex" nil )"nzreal" real_typesnil )"real" complex_types nil )nil polar nil )"complex" nil ))nil 3297701781"" (skosimp)"" (lemma "abs_nz_iff_nz" ("z" "n0x!1" ))"" (assert )"" (expand "arg" )"" (lemma "Im_div" ("z" "n0x!1" "n0z" "abs(n0x!1)" ))"1" (typepred "abs(n0x!1)" )"1" (lemma "Re_real" ("x" "abs(n0x!1)" ))"1" (lemma "Im_real" ("x" "abs(n0x!1)" ))"1" (replace -1)"1" (expand "conjugate" )"1" (replace -1)"1" (replace -2)"1" (rewrite "zero_times1" -4)"1" (rewrite "zero_times1" -4)"1" "div_times" "x" "Im(n0x!1)" "y" "abs(n0x!1)" "n0x" "abs(n0x!1)" "n0y" "abs(n0x!1)" ))"1" rewrite "div_simp" -1)"1" replace -1 -5 rl)"1" "1" rewrite "number_fields_right_identity_mult" )"1" replace -4)"1" "Re_div" "z" "n0x!1" "n0z" "abs(n0x!1)" ))"1" expand "conjugate" )"1" replace -2)"1" replace -3)"1" assert )"1" "div_times" "x" "Re(n0x!1)" "y" "abs(n0x!1)" "n0x" "abs(n0x!1)" "n0y" "abs(n0x!1)" ))"1" rewrite "div_simp" )"1" rewrite "number_fields_right_identity_mult" )"1" replace "1" "complex_is_ne_0_Re_Im" "z" "n0x!1" ))"1" "atan2_cancel_pos" "x" "Re(n0x!1)" "y" "Im(n0x!1)" "pz" "1/abs(n0x!1)" ))"1" "1" replace "1" replace "1" rewrite "div_mult_pos_lt1" "1" "Im(n0x!1) < 0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "abs(n0x!1)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "real_is_complex" ("x" "abs(n0x!1)" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil polar nil )"complex" nil )"argrng" polar nil )NOT const-decl "[bool -> bool]" booleans nil )nil arithmetic nil )"complex" arithmetic nil )"nnreal" nil )"complex" complex_types nil )nil number_fields_bis nil )"complex" nil )"real" reals nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )nil arithmetic nil )nil real_types nil )"bool" reals nil )nil real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil atan2 "trig/" )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"complex" nil )nil arithmetic nil )nil nil )"[numfield, nznum -> numfield]" number_fields nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )nil number_fields_bis nil )nil number_fields_bis nil )"posreal" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"real" reals nil )"complex" nil )"real" reals nil )"real" complex_types nil )"real" complex_types nil )nil arithmetic nil )nil arithmetic nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" polar nil )"nzcomplex" complex_types nil )"(strict_total_order?[real])" real_props nil ))nil 3307887108"" (skosimp*)"" (expand "arg" )"" (expand "abs" )"" (expand "conjugate" )"" (lemma "complex_is_Re_Im" ("z" "n0x!1" ))"" (lemma "complex_is_ne_0_Re_Im" ("z" "n0x!1" ))"" (simplify -1)"" (name-replace "X" "Re(n0x!1)" )"" (name-replace "Y" "Im(n0x!1)" )"" (replace -2)"" (simplify -3)"" (rewrite "sq.sq_rew" )"" (rewrite "sq.sq_rew" )"" rewrite "associative_mult" -3 :dir rl)"" rewrite "i_axiom" )"" "" "cos_period" "a" "atan2(X,Y)" "j" "-1" ))"1" replace -1 1 rl)"1" "cos_atan2" "x" "X" "y" "Y" ))"1" replace -3 -1)"1" "X=0" )"1" replace -2)"1" "Y<0" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" replace -1 2)"2" "1 + sq.sq(Y / X) = 1/sq.sq(X)" )"1" "1" "1" case "sq.sq(X)>0" )"1" rewrite "sqrt_div" )"1" "X>0" )"1" rewrite "sqrt.sqrt_sq" )nil nil )"2" assert )nil nil ))nil ))nil )"2" "sq.sq_nz_pos" "nz" "X" ))"2" nil nil ))nil ))nil ))nil ))nil )"2" rewrite "sq.sq_div" "2" "add_div" "x" "1" "n0x" "1" "y" "sq.sq(Y)" "n0y" "sq.sq(X)" ))"2" replace -1 1)"2" assert )nil nil ))nil ))nil ))nil )"3" "sq.sq_eq_0" "a" "X" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"argrng" polar nil )"real" complex_types nil )"real" complex_types nil )"complex" arithmetic nil )nil arithmetic nil )"[T, T -> boolean]" equalities nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"posreal" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"real" reals nil )nil sq "reals/" )"nzcomplex" nil )"odd_int" integers nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )nil number_fields nil )"nzint" integersnil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"complex" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nzreal" nil )"nzcomplex" complex_types nil )"posreal" nil )"even_int" integersnil )"npreal" nil )"posreal" sqrt "reals/" )"real" reals nil )nil sq "reals/" )nil reals nil )nil sqrt "reals/" )"(total_order?[real])" nil )nil sqrt "reals/" )nil sqrt "reals/" )"real" reals nil )"complex" nil )nil sqrt "reals/" )"bool" reals nil )nil number_fields_bis nil )"nnreal" nil )"real" reals nil )"posrat" nil )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )"trig_range" trig_basic "trig/" )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil atan2 "trig/" )"[numfield -> numfield]" number_fields nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" atan2 "trig/" )"[bool, bool -> bool]" booleans nil )nil trig_basic "trig/" )nil complex_types nil )"complex" nil )"complex" nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"nnreal" polar nil )"complex" nil ))nil )nil 3297716468"" (skosimp*)"" (expand "arg" )"" (expand "abs" )"" (expand "conjugate" )"" (lemma "complex_is_Re_Im" ("z" "n0x!1" ))"" (lemma "complex_is_ne_0_Re_Im" ("z" "n0x!1" ))"" (simplify -1)"" (name-replace "X" "Re(n0x!1)" )"" (name-replace "Y" "Im(n0x!1)" )"" (replace -2)"" (simplify -3)"" (rewrite "sq_rew" )"" (rewrite "sq_rew" )"" rewrite "associative_mult" -3 :dir rl)"" rewrite "i_axiom" )"" "" "cos_period" "a" "atan2(X,Y)" "j" "-1" ))"1" replace -1 1 rl)"1" "cos_atan2" "x" "X" "y" "Y" ))"1" replace -3 -1)"1" "X=0" )"1" replace -2)"1" "Y<0" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" replace -1 2)"2" "sq_eq" "nna" "sqrt(sq(X)+sq(Y))" "nnb" "1" ))"2" rewrite "sq_1" )"2" rewrite "sq_sqrt" )"2" replace -5 -1)"2" "2" "1 + sq(Y / X) = 1/sq(X)" )"1" "1" case "sq(X)>0" )"1" rewrite "sqrt_div" )"1" "X>0" )"1" rewrite "sqrt_sq" )nil nil )"2" assert )nil nil ))nil ))nil )"2" "sq_nz_pos" "nz" "X" ))"2" nil nil ))nil ))nil ))nil )"2" rewrite "sq_div" "2" "add_div" "x" "1" "n0x" "1" "y" "sq(Y)" "n0y" "sq(X)" ))"1" replace "1" replace "1" assert )nil nil ))nil ))nil )"2" "sq_eq_0" "a" "X" ))"2" assert )nil nil ))nil ))nil ))nil )"3" expand "sq" )"3" "sq_eq_0" "a" "X" ))"3" expand "sq" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" arithmetic nil )nil arithmetic nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )nil sq "reals/" )"nonneg_real" sq "reals/" )nil sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil sq "reals/" )nil number_fields_bis nil )nil sq "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil sq "reals/" )nil atan2 "trig/" )"real" atan2 "trig/" )nil trig_basic "trig/" )nil complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil arithmetic nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )nil complex_types nil ))nil 3307887538"" (skosimp)"" (expand "arg" )"" (expand "abs" )"" (expand "conjugate" )"" (lemma "complex_is_Re_Im" ("z" "n0x!1" ))"" (lemma "complex_is_ne_0_Re_Im" ("z" "n0x!1" ))"" (simplify -1)"" (name-replace "X" "Re(n0x!1)" )"" (name-replace "Y" "Im(n0x!1)" )"" (replace -2)"" (simplify -3)"" (rewrite "sq.sq_rew" )"" (rewrite "sq.sq_rew" )"" rewrite "associative_mult" -3 :dir rl)"" rewrite "i_axiom" )"" "" "sin_period" "a" "atan2(X,Y)" "j" "-1" ))"1" replace -1 1 rl)"1" "sin_atan2" "x" "X" "y" "Y" ))"1" replace -3 -1)"1" "X=0" )"1" replace -2)"1" "Y<0" )"1" assert )"1" "sq.sq_neg" )"1" "Y" )"1" replace "1" rewrite "sqrt.sqrt_sq" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "sqrt.sqrt_sq" )"2" "Y" )"2" "1" replace "1" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -1 2)"2" "2" "sq.sq_eq" "nna" "sqrt(sq.sq(X)+sq.sq(Y))" "nnb" "1" ))"2" rewrite "sq.sq_1" )"2" rewrite "sqrt.sq_sqrt" )"2" replace "2" "2" "sq.sq_nz_pos" "nz" "X" ))"2" "1 + sq.sq(Y / X) = 1/sq.sq(X)" )"1" "X>0" )"1" rewrite "sqrt.sqrt_div" "1" rewrite "sqrt.sqrt_sq" )"1" rewrite "div_div2" )nil nil ))nil ))nil )"2" assert )"2" "sq.sq_neg" )"2" "X" )"2" replace "2" rewrite "sqrt.sqrt_div" "2" rewrite "div_div1" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "add_div" "x" "1" "n0x" "1" "y" "sq.sq(X)" "n0y" "sq.sq(Y)" ))"1" replace "1" rewrite "sq.sq_div" "1" assert )nil nil ))nil ))nil )"2" expand "/=" "2" "sq.sq_eq_0" "a" "Y" ))"2" assert )nil nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"argrng" polar nil )"real" complex_types nil )"real" complex_types nil )"complex" arithmetic nil )nil arithmetic nil )"[T, T -> boolean]" equalities nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"posreal" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"real" reals nil )nil sq "reals/" )"nzcomplex" nil )"odd_int" integers nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )nil number_fields nil )"nzint" integersnil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nzreal" nil )"posreal" sqrt "reals/" )"real" reals nil )"complex" nil )nil sq "reals/" )nil sq "reals/" )nil reals nil )nil number_fields_bis nil )nil sq "reals/" )"real" reals nil )"nnreal" nil )"posrat" nil )nil sq "reals/" )"bool" reals nil )nil number_fields_bis nil )nil sqrt "reals/" )nil sqrt "reals/" )nil number_fields_bis nil )"real" reals nil )"even_int" integersnil )"nzcomplex" complex_types nil )"nzreal" nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil sqrt "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil real_types nil )nil sq "reals/" )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"trig_range" trig_basic "trig/" )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )nil sqrt "reals/" )"real" reals nil )"complex" nil )"(total_order?[real])" nil )nil sq "reals/" )"bool" reals nil )nil atan2 "trig/" )"[numfield -> numfield]" number_fields nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" atan2 "trig/" )"[bool, bool -> bool]" booleans nil )nil trig_basic "trig/" )nil complex_types nil )"complex" nil )"complex" nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"nnreal" polar nil )"complex" nil ))nil )nil 3297722477"" (skosimp)"" (expand "arg" )"" (expand "abs" )"" (expand "conjugate" )"" (lemma "complex_is_Re_Im" ("z" "n0x!1" ))"" (lemma "complex_is_ne_0_Re_Im" ("z" "n0x!1" ))"" (simplify -1)"" (name-replace "X" "Re(n0x!1)" )"" (name-replace "Y" "Im(n0x!1)" )"" (replace -2)"" (simplify -3)"" (rewrite "sq_rew" )"" (rewrite "sq_rew" )"" rewrite "associative_mult" -3 :dir rl)"" rewrite "i_axiom" )"" "" "sin_period" "a" "atan2(X,Y)" "j" "-1" ))"1" replace -1 1 rl)"1" "sin_atan2" "x" "X" "y" "Y" ))"1" replace -3 -1)"1" "X=0" )"1" replace -2)"1" "Y<0" )"1" assert )"1" "sq_neg" )"1" "Y" )"1" replace "1" rewrite "sqrt_sq" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "sqrt_sq" )"2" "Y" )"2" "1" replace "1" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -1 2)"2" "2" "sq_eq" "nna" "sqrt(sq(X)+sq(Y))" "nnb" "1" ))"2" rewrite "sq_1" )"2" rewrite "sq_sqrt" )"2" replace "2" "2" "sq_nz_pos" "nz" "X" ))"2" "1 + sq(Y / X) = 1/sq(X)" )"1" "X>0" )"1" rewrite "sqrt_div" "1" rewrite "sqrt_sq" )"1" rewrite "div_div2" )nil nil ))nil ))nil )"2" assert )"2" "sq_neg" )"2" "X" )"2" replace "2" rewrite "sqrt_div" "2" rewrite "div_div1" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "add_div" "x" "1" "n0x" "1" "y" "sq(X)" "n0y" "sq(Y)" ))"1" replace "1" rewrite "sq_div" "1" assert )nil nil ))nil ))nil )"2" expand "/=" "2" "sq_eq_0" "a" "Y" ))"2" assert )nil nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" arithmetic nil )nil arithmetic nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )nil sq "reals/" )"nonneg_real" sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil number_fields_bis nil )nil sq "reals/" )nil sq "reals/" )nil number_fields_bis nil )nil sqrt "reals/" )nil sqrt "reals/" )nil number_fields_bis nil )nil sqrt "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil sq "reals/" )nil sq "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil atan2 "trig/" )"real" atan2 "trig/" )nil trig_basic "trig/" )nil complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )nil arithmetic nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )nil complex_types nil ))nil 3385304736"" (skosimp)"" (typepred "nnx!1" )"" (expand "arg" )"" (expand ">=" )"" (expand "<=" )"" (split -1)"1" (assert )"1" (rewrite "Im_real" )"1" (rewrite "Re_real" )"1" (assert )"1" (expand "atan2" )"1" (rewrite "atan_0" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil arithmetic nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"nzcomplex" complex_types nil )nil atan "trig/" )"real" atan2 "trig/" )nil arithmetic nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"argrng" polar nil )"complex" nil ))nil 3385304815"" (skosimp)"" (typepred "nx!1" )"" (hide -1)"" (expand "arg" )"" (rewrite "Im_real" )"" (rewrite "Re_real" )"" (assert )"" (expand "atan2" ) (("" (rewrite "atan_0" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"complex" nil )"argrng" polar nil )nil arithmetic nil )"real" atan2 "trig/" )nil atan "trig/" )"(strict_total_order?[real])" real_props nil )"posreal" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )nil arithmetic nil ))nil 3385194777"" (lemma "arg_is_pi2" ("z" "i" ))"" (lemma "Re_imag" ("x" "1" ))"" (lemma "Im_imag" ("x" "1" ))"" (rewrite "identity_mult" )"" (replace -1)"" (replace -2) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil arithmetic nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )nil number_fields nil )"real" complex_types nil )"real" complex_types nil )"nzcomplex" complex_types nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil arithmetic nil )"complex" nil )nil polar nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"complex" complex_types nil ))nil 3297516982"" (skolem 1 ("a" ))"" (name "AA" "arg(a)" )"" (replace -1)"" (case-replace "a=0" )"1" (assert ) nil nil )"2" (lemma "complex_is_ne_0_Re_Im" ("z" "a" ))"2" (assert )"2" (typepred "arg(a)" )"2" (lemma "arg_gt_0" ("z" "a" ))"2" (lemma "arg_lt_0" ("z" "a" ))"2" (lemma "arg_is_0_nz" ("n0z" "a" ))"2" (replace -7)"2" (case-replace "0<AA" )"1" (assert )"1" (expand "arg" )"1" rewrite "Im_neg" )"1" rewrite "Re_neg" )"1" "atan2_cancel_neg" "x" "-Re(a)" "y" "-Im(a)" "nz" "-1" ))"1" "1" assert )"1" "1" (assert ) nil nil )"2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "1" (assert ) nil nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "arg" )"2" "AA=0" )"1" assert )"1" rewrite "Re_neg" )"1" rewrite "Im_neg" )"1" "atan2_cancel_neg" "x" "-Re(a)" "y" "-Im(a)" "nz" "-1" ))"1" assert )"1" "1" "1" (assert ) nil nil ))nil )"2" "1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "atan2_cancel_neg" "x" "-Re(a)" "y" "-Im(a)" "nz" "-1" ))"2" rewrite "Im_neg" )"2" rewrite "Re_neg" )"2" "1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil complex_types nil )"boolean" notequal nil )"argrng" polar nil )nil polar nil )"bool" reals nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"real" complex_types nil )"real" complex_types nil )nil polar nil )nil polar nil )nil arithmetic nil )"complex" nil )"{y | EXISTS x: z = x + y * i}" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil atan2 "trig/" )"complex" nil )"real" reals nil )"posreal" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )nil arithmetic nil )"nzreal" real_typesnil )"(total_order?[real])" nil )"complex" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )nil polar nil )NOT const-decl "[bool -> bool]" booleans nil )nil arithmetic nil )"complex" nil )"odd_int" integers nil )"nzcomplex" nil ))nil 3294697583"" (skosimp*)"" (rewrite "arg_div_abs" )"" (lemma "arg_div_abs" ("n0x" "n0x!1" ))"" (lemma "arg_div_abs" ("n0x" "n0y!1" ))"" (replace -1)"" (replace -2)"" (hide -1 -2)"" (rewrite "abs_mult" )"" (rewrite "div_times" 1 :dir rl)"" (name "X" "n0x!1 / abs(n0x!1)" )"" (replace -1)"" (name "Y" "n0y!1 / abs(n0y!1)" )"" (replace -1)"" (lemma "Re_cos_abs1" ("n0x" "X" ))"1" "Re_cos_abs1" ("n0x" "Y" ))"1" "Im_sin_abs1" ("n0x" "X" ))"1" "Im_sin_abs1" ("n0x" "Y" ))"1" "abs(X)=1" )"1" "abs(Y)=1" )"1" "abs_mult" "z1" "X" "z2" "Y" ))"1" replace -2)"1" replace -3)"1" "Re_cos_abs1" "n0x" "X*Y" ))"1" "Im_sin_abs1" "n0x" "X*Y" ))"1" replace -3)"1" case "X/=0" )"1" case "Y/=0" )"1" case "X*Y/=0" )"1" "TH1" "arg(X)" )"1" "TH2" "arg(Y)" )"1" "arg(X)" )"1" "arg(Y)" )"1" replace "1" replace "1" "Re_times" "z1" "X" "z2" "Y" ))"1" "Im_times" "z1" "X" "z2" "Y" ))"1" replace "1" replace "1" replace "1" replace "1" "sin_plus" "a" "TH1" "b" "TH2" ))"1" replace "1" "cos_plus" "a" "TH1" "b" "TH2" ))"1" replace "1" "1" expand "arg" "1" replace "1" replace "1" "TH1 + TH2 > pi" )"1" "TH1+TH2=2*pi" )"1" rewrite "sin_2pi" )"1" rewrite "cos_2pi" )"1" expand "atan2" )"1" rewrite "atan_0" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "sin_lt_0" "a" "TH1+TH2" ))"2" assert )"2" rewrite "atan2_cos_sin" )nil nil ))nil ))nil ))nil )"2" "TH1 + TH2 <= -pi" )"1" assert )"1" "TH1 + TH2 = -pi" )"1" rewrite "sin_neg" "1" rewrite "cos_neg" "1" rewrite "sin_pi" )"1" rewrite "cos_pi" )"1" expand "atan2" )"1" rewrite "atan_0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sin_gt_0" "a" "TH1+TH2+2*pi" ))"2" assert )"2" "sin_period" "a" "TH1+TH2" "j" "1" ))"2" "cos_period" "a" "TH1+TH2" "j" "1" ))"2" assert )"2" "atan2_cos_sin" "a" "TH1 + TH2 + 2 * pi" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "trichotomy" "x" "TH1+TH2" ))"2" "1" "sin_gt_0" "a" "TH1+TH2" ))"1" assert )"1" "TH1+TH2=pi" )"1" rewrite "sin_pi" )"1" rewrite "cos_pi" )"1" expand "atan2" )"1" rewrite "atan_0" )nil nil ))nil ))nil ))nil )"2" assert )"2" rewrite "atan2_cos_sin" )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" rewrite "sin_0" )"2" rewrite "cos_0" )"2" expand "atan2" )"2" rewrite "atan_0" )nil nil ))nil ))nil ))nil ))nil )"3" "sin_lt_0" "a" "TH1+TH2+2*pi" ))"3" assert )"3" "sin_period" "a" "TH1+TH2" "j" "1" ))"3" "cos_period" "a" "TH1+TH2" "j" "1" ))"3" assert )"3" "atan2_cos_sin" "a" "TH1 + TH2 + 2 * pi" ))"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "abs_nz_iff_nz" "z" "X*Y" ))"2" assert )nil nil ))nil ))nil )"2" "abs_nz_iff_nz" "z" "Y" ))"2" assert )nil nil ))nil ))nil )"2" "abs_nz_iff_nz" "z" "X" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "abs_nz_iff_nz" "z" "X*Y" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1 1 rl)"2" rewrite "abs_div" )"1" rewrite "abs_abs" )"1" rewrite "div_simp" )nil nil ))nil )"2" rewrite "real_is_complex" nil nil ))nil ))nil ))nil ))nil )"2" replace -6 1 rl)"2" "2" rewrite "abs_div" )"1" rewrite "abs_abs" )"1" rewrite "div_simp" )nil nil ))nil )"2" rewrite "real_is_complex" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "abs_nzcomplex" "n0z" "n0y!1" ))"2" "real_is_complex" "x" "abs(n0y!1)" ))"2" "nznum_div_nznum_is_nznum" "nzx" "n0y!1" "nzy" "abs(n0y!1)" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "abs_nzcomplex" ("n0z" "n0x!1" ))"2" "nznum_div_nznum_is_nznum" "nzx" "n0x!1" "nzy" "abs(n0x!1)" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzcomplex" complex_types nil )nil polar nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"nzcomplex" complex_types nil )nil polar nil )"nnreal" nil )"complex" nil )"[T, T -> boolean]" equalities nil )"[numfield, nznum -> numfield]" number_fields nil )nil polar nil )nil polar nil )nil polar nil )"real" reals nil )"complex" nil )nil number_fields_bis nil )nil polar nil )nil arithmetic nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )nil trig_basic "trig/" )nil trig_basic "trig/" )"odd_int" integers nil )"posreal" nil )nil trig_basic "trig/" )"complex" nil )"real" reals nil )nil trig_basic "trig/" )nil trig_basic "trig/" )"posint" nil )"even_int" integersnil )"(divides(n))" divides nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil trig_basic "trig/" )nil trig_ineq "trig/" )nil real_axioms nil )nil trig_basic "trig/" )nil trig_basic "trig/" )"even_int" integers nil )"nzint" integers nil )"nzcomplex" nil )nil trig_basic "trig/" )nil atan "trig/" )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nzreal" real_typesnil )"(total_order?[real])" nil )"real" atan2 "trig/" )nil trig_basic "trig/" )"real" reals nil )"complex" nil )nil atan2 "trig/" )"(total_order?[real])" nil )nil trig_ineq "trig/" )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"complex" nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )nil trig_basic "trig/" )nil trig_basic "trig/" )"real" reals nil )"real" complex_types nil )"real" complex_types nil )nil arithmetic nil )NOT const-decl "[bool -> bool]" booleans nil )"argrng" polar nil )nil polar nil )"bool" reals nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil polar nil )nil number_fields_bis nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" polar nil ))nil 3295020761"" (skolem 1 ("a" ))"" (typepred "a" )"" (hide -1 -2)"" (lemma "arg_mult" ("n0x" "a" "n0y" "1/a" ))"1" (rewrite "times_div1" -1)"1" (rewrite "div_simp" -1)"1" (lemma "arg_is_0_nz" ("n0z" "1" ))"1" (rewrite "Re_real" )"1" (rewrite "Im_real" )"1" (assert )"1" (replace -1)"1" (typepred "arg(a)" )"1" (typepred "arg(1/a)" )"1" "arg(1 / a) + arg(a) > pi" )"1" (assert ) nil nil )"2" "arg(1 / a) + arg(a) <= -pi" )"1" (assert ) nil nil )"2" assert )"2" "arg(a)=0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "inv_ne_0" ("n0x" "a" )) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil polar nil )"nzcomplex" complex_types nil )nil number_fields_bis nil )nil reals nil )"[number_field -> boolean]" reals nil )nil arithmetic nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"complex" nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"bool" reals nil )nil polar nil )"argrng" polar nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"nzcomplex" nil )"nzreal" real_typesnil )"(total_order?[real])" nil )"complex" nil )"complex" nil )"[T, T -> boolean]" equalities nil )nil arithmetic nil )nil polar nil )"complex" nil )"nzcomplex" complex_types nil )"posreal" nil )nil number_fields_bis nil ))nil 3295021146"" (skolem 1 ("a" "b" ))"" (rewrite "div_def" )"" (lemma "arg_mult" ("n0x" "a" "n0y" "1/b" ))"1" (lemma "arg_inv" ("n0z" "b" ))"1" (typepred "arg(a)" )"1" (case-replace "arg(b)=0" )"1" (assert ) nil nil )"2" (replace 1)"2" (case-replace "arg(b)=pi" )"1" (assert )"1" (replace -4)"1" (case-replace "arg(a) > 0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (replace -3)"2" (case-replace "arg(a) - arg(b) > pi" )"1" (assert ) nil nil )"2" (case-replace "arg(a) - arg(b) <= -pi" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "real_is_complex" ("x" "1" ))"2" (lemma "closed_divides" ("z" "1" "n0z" "b" ))"1" (propax) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )nil complex_types nil )nil number_fields nil )"posreal" nil )"nzcomplex" complex_types nil )"nzcomplex" complex_types nil )nil polar nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"nzcomplex" nil )"nzreal" real_typesnil )"(total_order?[real])" nil )"complex" nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"complex" nil )"nzint" integers nil )"even_int" integers nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"bool" reals nil )nil polar nil )"argrng" polar nil )"[numfield, nznum -> numfield]" number_fields nil )nil polar nil ))nil 3596190942"" (skeep)"" (expand "from_polar" )"" case "NOT (Re(sin(theta) * i * r + r * cos(theta)) = r*cos(theta) AND Im(sin(theta) * i * r + r * cos(theta)) = r*sin(theta))" )"1" (hide 2)"1" (split)"1" (rewrite "Re_plus" )"1" (lemma "Re_imag" )"1" (inst - "sin(theta)*r" )"1" (assert )"1" (replace -1)"1" (assert )"1" (hide -1)"1" (rewrite "Re_real" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "Im_plus" )"2" (assert )"2" (lemma "Im_real" )"2" (inst - "r*cos(theta)" )"2" (replaces -1)"2" (assert )"2" (lemma "Im_imag" )"2" (inst - "sin(theta)*r" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "arg" )"2" (replace -1)"2" (replace -2)"2" (lift-if)"2" (ground)"1" (rewrite "complex_is_0_Re_Im" -1)"1" (flatten)"1" (replace -3)"1" (replace -4)"1" (assert )"1" "sin_eq_0" )"1" "theta" )"1" "1" "1" case "i!1 >=2" )"1" "pi" )"1" (assert ) nil nil ))nil )"2" case "i!1 <= -1" )"1" "pi" )"1" (assert ) nil nil ))nil )"2" case "i!1 = 1" )"1" "1" assert )"1" replace -2)"1" "cos_pi" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "i!1 = 0" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "r" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "atan2" )"2" (lift-if)"2" (ground)"1" (lemma "atan_tan" )"1" (inst - "theta" )"1" expand "tan" )"1" assert )"1" case "r*sin(theta)/(r*cos(theta)) = atan(theta)" )"1" assert )"1" replace -1)"1" (propax) nil nil ))nil ))nil )"2" assert )"2" replace -1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "NOT (cos(theta)>0 AND sin(theta)<0)" )"1" "1" "r" )"1" (assert ) nil nil ))nil )"2" "r" )"2" (assert ) nil nil ))nil ))nil )"2" "2" "2" "cos_le_0" )"2" "theta" )"2" "sin_ge_0" )"2" "theta" )"2" assert )"2" "cos_neg" )"2" "theta" )"2" "2" "cos_le_0" )"2" "-theta" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "cos_eq_0" )"2" (inst - "theta" )"2" assert )"2" "1" "1" "sin_ge_0" )"1" "theta" )"1" assert )"1" "1" "r" )"1" (assert ) nil nil ))nil )"2" case "NOT sin(theta)<0" )"1" "r" )"1" assert )nil nil ))nil )"2" case "i!1>=0" )"1" "pi" )"1" assert )nil nil ))nil )"2" case "i!1 <= -2" )"1" "pi" )"1" assert )nil nil ))nil )"2" case "i!1 = -1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "r" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" case "NOT (cos(theta) < 0 AND sin(theta) < 0)" )"1" (split)"1" "r" )"1" (assert ) nil nil ))nil )"2" "r" )"2" (assert ) nil nil ))nil ))nil )"2" (flatten)"2" "2" "atan_tan" )"2" "theta+pi" )"1" case "tan(theta+pi) = tan(theta)" )"1" "1" expand "tan" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" expand "tan" 1)"2" rewrite "sin_plus" 1)"2" rewrite "cos_plus" 1)"2" rewrite "cos_pi" )"2" rewrite "sin_pi" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "Tan?" )"3" (assert ) nil nil ))nil ))nil )"2" "cos_ge_0" )"2" "theta" )"2" assert )"2" "sin_ge_0" )"2" "theta" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (case "NOT sin(theta)>=0" )"1" (mult-by 1 "r" ) (("1" (assert ) nil nil ))nil )"2" (hide 1)"2" (case "theta < 0" )"1" (lemma "sin_lt_0" )"1" (inst - "theta + 2*pi" )"1" assert )"1" rewrite "sin_plus" )"1" rewrite "cos_2pi" )"1" rewrite "sin_2pi" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "NOT theta>=0" )"1" (assert ) nil nil )"2" "2" expand "atan2" )"2" "2" assert )"2" "1" case "NOT cos(theta)>0" )"1" "r" )"1" (assert ) nil nil ))nil )"2" "2" "atan_tan" )"2" "theta" )"1" expand "tan" )"1" assert )"1" nil nil ))nil ))nil )"2" assert )"2" "cos_le_0" )"2" "theta" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "cos_eq_0" )"2" "theta" )"2" "1" "1" case "i!1 = 0" )"1" assert )nil nil )"2" case "i!1>=1" )"1" "pi" )"1" assert )nil nil ))nil )"2" assert )"2" case "i!1<=-1" )"1" "pi" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "r" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "cos_eq_0" )"3" "3" assert )"3" "1" "1" case "i!1 = 0" )"1" assert )"1" "1" assert )"1" "1" rewrite "sin_pi2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "i!1>=1" )"1" "pi" )"1" assert )nil nil ))nil )"2" case "i!1<=-1" )"1" "pi" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "r" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" case "NOT cos(theta)<0" )"1" "r" )"1" (assert ) nil nil ))nil )"2" "2" case "NOT theta > pi/2" )"1" "cos_ge_0" )"1" "theta" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "atan_tan" )"2" "theta-pi" )"2" expand "tan" -1)"2" rewrite "sin_minus" )"2" rewrite "cos_minus" )"2" rewrite "sin_pi" )"2" rewrite "cos_pi" )"2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"complex" nil )"trig_range" trig_basic "trig/" )"complex" polar nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"nzcomplex" complex_types nil )"posreal" nil )nil real_props nil )nil trig_basic "trig/" )nil trig_basic "trig/" )nil trig_ineq "trig/" )nil trig_basic "trig/" )nil trig_basic "trig/" )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )nil trig_basic "trig/" )"real" atan2 "trig/" )"complex" nil )"nzcomplex" complex_types nil )"real" reals nil )"posreal" nil )"nzreal" nil )"[numfield, nznum -> numfield]" number_fields nil )"argrng" polar nil )nil atan "trig/" )"real_abs_lt_pi2" atan "trig/" )"real" trig_basic "trig/" )nil trig_ineq "trig/" )nil trig_ineq "trig/" )"complex" nil )nil trig_basic "trig/" )nil trig_inverses "trig/" )"nzint" integers nil )"even_int" integers nil )nil trig_basic "trig/" )nil trig_ineq "trig/" )"bool" trig_basic "trig/" )nil trig_basic "trig/" )nil trig_basic "trig/" )nil trig_basic "trig/" )nil arithmetic nil )nil number_fields_bis nil )"boolean" notequal nil )nil number_fields nil )"odd_int" integers nil )"nzreal" nil )nil extra_real_propsnil )nil trig_basic "trig/" )nil extra_real_propsnil )"(total_order?[real])" nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil trig_basic "trig/" )"real" reals nil )"complex" nil )"argrng" polar nil )nil arithmetic nil )nil arithmetic nil )nil arithmetic nil )nil arithmetic nil )"real" reals nil )nil arithmetic nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nzcomplex" nil )"nzreal" real_typesnil )"(total_order?[real])" nil )nil arithmetic nil )"real" complex_types nil )"real" complex_types nil )"real" reals nil )"complex" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" complex_typesnil )nil complex_types nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"real" trig_basic "trig/" )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"bool" reals nil )nil polar nil )"real" trig_basic "trig/" )"{y | EXISTS x: z = x + y * i}" complex_types nil ))nil 3294313266"" (skosimp)"" (expand "rectangular" )"" (expand "from_rectangular" )"" (lemma "complex_is_Re_Im" ("z" "z!1" ))"" (propax) nil nil )) nil ))nil ))nil ))nil )"complex" nil )"[real, real]" polar nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil arithmetic nil )"complex" polar nil )"real" complex_types nil ))nil 3307887703"" (expand "polar" )"" (expand "from_polar" )"" (skosimp)"" (lemma "complex_is_ne_0_Re_Im" ("z" "n0z!1" ))"" (assert )"" "unique_characterization" "x0" "Re(n0z!1)" "y0" "Im(n0z!1)" "y1" "abs(n0z!1) * sin(arg(n0z!1))" "x1" "abs(n0z!1) * cos(arg(n0z!1))" ))"" (lemma "complex_is_Re_Im" ("z" "n0z!1" ))"" (replace -1 -2 rl)"" (replace -2 1)"" (hide -2)"" (expand "arg" )"" "IF Im(n0z!1) < 0 THEN cos(atan2(Re(n0z!1), Im(n0z!1)) - 2 * pi) ") "1" "IF Im(n0z!1) < 0 THEN sin(atan2(Re(n0z!1), Im(n0z!1)) - 2 * pi) ") "1" (hide -1 -2)"1" "sin_atan2" "x" "Re(n0z!1)" "y" "Im(n0z!1)" ))"1" "cos_atan2" "x" "Re(n0z!1)" "y" "Im(n0z!1)" ))"1" replace -4)"1" "Re(n0z!1)=0" )"1" replace -2)"1" assert )"1" expand "atan2" )"1" rewrite "sin_pi2" )"1" rewrite "sin_3pi2" )"1" expand "abs" )"1" expand "conjugate" )"1" rewrite -1)"1" assert )"1" "DRL1" "Im(n0z!1)" )"1" replace "1" assert )"1" rewrite "sq.sq_rew" )"1" rewrite "associative_mult" "1" rewrite "associative_mult" "1" rewrite "associative_mult" "1" rewrite "associative_mult" "1" rewrite "i_axiom" )"1" rewrite "commutative_mult" "1" rewrite "associative_mult" "1" "DRL1>0" )"1" rewrite "sqrt.sqrt_sq" )nil nil )"2" "sq.sq_neg" )"2" "DRL1" )"2" replace "2" rewrite "sqrt.sqrt_sq" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "DRL1" "Im(n0z!1) / Re(n0z!1)" )"2" replace -1)"2" assert )"2" "X" "Re(n0z!1)" )"2" replace -1)"2" "Y" "Im(n0z!1)" )"2" replace -1)"2" "abs(n0z!1) = sqrt(sq.sq(X)+sq.sq(Y))" )"1" "sqrt(1 + sq.sq(DRL1)) = sqrt(sq.sq(X) + sq.sq(Y))/IF X>0 THEN X ELSE -X ENDIF" )"1" "X>0" )"1" rewrite "div_div1" )"1" rewrite "div_div1" )"1" replace "1" replace "1" "DRL3" "sqrt(sq.sq(X) + sq.sq(Y))" )"1" "div_cancel1" "n0z" "DRL3" "x" "1*X" ))"1" "div_cancel1" "n0z" "DRL3" "x" "DRL1*X" ))"1" replace "1" replace "1" replace "1" rewrite "div_cancel2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )"2" "2" replace "2" rewrite "sq.sq_div" )"2" "X>0" )"1" "sqrt.sqrt_sq" )"1" "X" )"1" "1" "sqrt.sqrt_div" )"1" "sq.sq(X) + sq.sq(Y)" "sq.sq(X)" )"1" "1" assert )nil nil )"2" expand "sq" )"2" "posreal_times_posreal_is_posreal" "px" "X" "py" "X" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "sq.sq_neg" )"2" "X" )"2" "sqrt.sqrt_sq" "x" "-X" ))"2" "1" "sqrt.sqrt_div" )"1" "sq.sq(X)+sq.sq(Y)" "sq.sq(-X)" )"1" "1" assert )"1" assert )nil nil ))nil )"2" expand "sq" )"2" assert )"2" "posreal_times_posreal_is_posreal" "px" "-X" "py" "-X" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil )"2" "2" expand "abs" )"2" expand "conjugate" )"2" replace "2" replace "2" replace "2" assert )"2" rewrite "sq.sq_rew" )"2" rewrite "sq.sq_rew" )"2" rewrite "associative_mult" "2" "i_axiom" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 -3))"2" "Im(n0z!1) < 0" )"1" "sin_minus" "a" "atan2(Re(n0z!1), Im(n0z!1))" "b" "2 * pi" ))"1" rewrite "sin_2pi" )"1" rewrite "cos_2pi" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (case-replace "Im(n0z!1) < 0" )"1" "cos_minus" "a" "atan2(Re(n0z!1), Im(n0z!1))" "b" "2 * pi" ))"1" rewrite "sin_2pi" )"1" rewrite "cos_2pi" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" (split -2)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"4" (split -2)"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"5" (flatten) (("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"complex" nil )"real" reals nil )"trig_range" trig_basic "trig/" )"complex" polar nil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"[number_field -> boolean]" complex_typesnil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil arithmetic nil )"real" trig_basic "trig/" )"{y | EXISTS x: z = x + y * i}" complex_types nil )"argrng" polar nil )nil polar nil )"bool" reals nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" trig_basic "trig/" )"nnreal" polar nil )nil real_types nil )"bool" reals nil )nil booleans nil )"{x | EXISTS y: z = x + y * i}" complex_types nil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" atan2 "trig/" )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil trig_basic "trig/" )"complex" nil )"nzcomplex" complex_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )nil trig_basic "trig/" )nil trig_basic "trig/" )nil trig_basic "trig/" )nil atan2 "trig/" )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"nzcomplex" nil )nil trig_basic "trig/" )"posreal" nil )"nonneg_real" sq "reals/" )nil number_fields nil )nil complex_types nil )"(divides(n))" divides nil )"nzint" integersnil )nil sq "reals/" )"nzcomplex" complex_types nil )"complex" nil )"real" reals nil )"(total_order?[real])" nil )nil sqrt "reals/" )nil number_fields nil )nil sq "reals/" )"complex" arithmetic nil )nil trig_basic "trig/" )"complex" nil )"real" reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" reals nil )"nzreal" nil )nil number_fields_bis nil )nil number_fields_bis nil )nil number_fields_bis nil )nil sq "reals/" )nil sqrt "reals/" )nil real_types nil )nil sqrt "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"posreal" sqrt "reals/" )nil atan2 "trig/" )"real" reals nil )nil trig_basic "trig/" )nil arithmetic nil )"complex" nil )"real" complex_types nil )"real" complex_types nil )"[nnreal, argrng]" polar nil ))nil )nil 3294313327"" (expand "polar" )"" (expand "from_polar" )"" (skosimp)"" (lemma "complex_is_ne_0_Re_Im" ("z" "n0z!1" ))"" (assert )"" "unique_characterization" "x0" "Re(n0z!1)" "y0" "Im(n0z!1)" "y1" "abs(n0z!1) * sin(arg(n0z!1))" "x1" "abs(n0z!1) * cos(arg(n0z!1))" ))"" (lemma "complex_is_Re_Im" ("z" "n0z!1" ))"" (replace -1 -2 rl)"" (replace -2 1)"" (hide -2)"" (expand "arg" )"" "IF Im(n0z!1) < 0 THEN cos(atan2(Re(n0z!1), Im(n0z!1)) - 2 * pi) ") "1" "IF Im(n0z!1) < 0 THEN sin(atan2(Re(n0z!1), Im(n0z!1)) - 2 * pi) ") "1" (hide -1 -2)"1" "sin_atan2" "x" "Re(n0z!1)" "y" "Im(n0z!1)" ))"1" "cos_atan2" "x" "Re(n0z!1)" "y" "Im(n0z!1)" ))"1" replace -4)"1" "Re(n0z!1)=0" )"1" replace -2)"1" assert )"1" expand "atan2" )"1" rewrite "sin_pi2" )"1" rewrite "sin_3pi2" )"1" expand "abs" )"1" expand "conjugate" )"1" rewrite -1)"1" assert )"1" "DRL1" "Im(n0z!1)" )"1" replace "1" assert )"1" rewrite "sq_rew" )"1" rewrite "associative_mult" "1" rewrite "associative_mult" "1" rewrite "associative_mult" "1" rewrite "associative_mult" "1" rewrite "i_axiom" )"1" rewrite "commutative_mult" "1" rewrite "associative_mult" "1" "DRL1>0" )"1" rewrite "sqrt_sq" )nil nil )"2" "sq_neg" )"2" "DRL1" )"2" replace "2" rewrite "sqrt_sq" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "DRL1" "Im(n0z!1) / Re(n0z!1)" )"1" replace -1)"1" assert )"1" "X" "Re(n0z!1)" )"1" replace -1)"1" "Y" "Im(n0z!1)" )"1" replace -1)"1" "abs(n0z!1) = sqrt(sq(X)+sq(Y))" )"1" "sqrt(1 + sq(DRL1)) = sqrt(sq(X) + sq(Y))/IF X>0 THEN X ELSE -X ENDIF" )"1" "X>0" )"1" rewrite "div_div1" )"1" rewrite "div_div1" )"1" replace "1" replace "1" "DRL3" "sqrt(sq(X) + sq(Y))" )"1" "div_cancel1" "n0z" "DRL3" "x" "1*X" ))"1" "div_cancel1" "n0z" "DRL3" "x" "DRL1*X" ))"1" replace "1" replace "1" replace "1" rewrite "div_cancel2" )nil nil ))nil ))nil ))nil ))nil )"2" "abs_nz_iff_nz" "z" "n0z!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" replace "2" rewrite "sq_div" )"2" "X>0" )"1" "sqrt_sq" )"1" "X" )"1" "1" "sqrt_div" )"1" "sq(X) + sq(Y)" "sq(X)" )"1" "1" assert )nil nil )"2" expand "sq" )"2" "posreal_times_posreal_is_posreal" "px" "X" "py" "X" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "sq_neg" )"2" "X" )"2" "sqrt_sq" "x" "-X" ))"2" "1" "sqrt_div" )"1" "sq(X)+sq(Y)" "sq(-X)" )"1" "1" assert )nil nil )"2" expand "sq" )"2" "posreal_times_posreal_is_posreal" "px" "-X" "py" "-X" ))"2" assert )nil nil ))nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.876Bemerkung:
(vorverarbeitet am 2026-05-01)
¤ *Bot Zugriff
2026-05-26
