(exp (exp_TCC1 0nil 3294275262"" (skosimp)"" (typepred "exp(Re(z!1))" )"" "both_sides_times1" "n0z" "exp(Re(z!1))" "x" "cos(Im(z!1)) + i * sin(Im(z!1))" "y" "0" ))"" (assert )"" (hide-all-but -1)"" "unique_characterization" "x0" "cos(Im(z!1))" "x1" "0" "y0" "sin(Im(z!1))" "y1" "0" ))"" (rewrite "zero_times1" -1)"" (assert )"" (lemma "sin_cos_eq_0" ("a" "Im(z!1)" ))"" (flatten -1)"" (hide -2)"" (split -1)"1" "1" (assert ) nil nil ))nil )"2" assert )"2" "2" rewrite "commutative_mult" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{x | EXISTS y: z = x + y * i}" complex_typesnil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )nil complex_types nil )"[number_field -> boolean]" nil )"{py | x = ln(py)}" ln_exp "lnexp/" )"real" ln_exp "lnexp/" )"[T, T -> boolean]" equalities 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]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nnreal" nil )"real" realsnil )"trig_range" trig_basic"trig/" )"trig_range" trig_basic"trig/" )"complex" complex_types nil )"(strict_total_order?[real])" real_props nil )"real" complex_types nil )"(total_order?[real])" nil )nil complex_types nil )nil number_fields nil )nil trig_aux nil )nil number_fields_bis nil )nil number_fields_bis nil )"boolean" notequal nil )nil number_fields nil )"real" trig_basic "trig/" )"{y | EXISTS x: z = x + y * i}" complex_typesnil )"real" trig_basic "trig/" )"complex" complex_types nil ))nil 3294334350"" (skosimp)"" (expand "exp" 1 1)"" (rewrite "Re_real" 1)"" (rewrite "Im_real" 1)"" (rewrite "sin_0" )"" (rewrite "cos_0" )"" (rewrite "zero_times2" )"" (rewrite "zero_times1" )"" (rewrite "identity_mult" 1) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_types nil )"trig_range" trig_basic"trig/" )"real" realsnil )"trig_range" trig_basic"trig/" )"nzcomplex" exp nil )nil arithmetic nil )nil trig_basic "trig/" )"nnreal" nil )"complex" complex_types nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields nil )"posreal" real_types nil )"nzcomplex" complex_types nil )"nznum" nil )nil number_fields_bis nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" )nil trig_basic "trig/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil arithmetic nil ))nil 3294844116"" (skosimp)"" (expand "exp" )"" (lemma "Re_imag" ("x" "r!1" ))"" (lemma "Im_imag" ("x" "r!1" ))"" (replace -1)"" (replace -2)"" (rewrite "exp_0" )"" (rewrite "identity_mult" )"" "commutative_mult" "x" "sin(r!1)" "y" "i" ))"" (replace -1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_types nil )"trig_range" trig_basic"trig/" )"real" realsnil )"trig_range" trig_basic"trig/" )"nzcomplex" exp nil )nil arithmetic nil )"real" trig_basic "trig/" )nil number_fields nil )nil number_fields nil )"real" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields nil )nil ln_exp "lnexp/" )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3294844749"" (skosimp)"" (rewrite "exp_imag" )"" (expand "abs" )"" (expand "conjugate" )"" (rewrite "Im_plus" )"1" (rewrite "Re_plus" )"1" (assert )"1" (lemma "Re_imag" ("x" "sin(r!1)" ))"1" (rewrite "commutative_mult" -1)"1" (replace -1)"1" (rewrite "Im_real" 1)"1" (rewrite "zero_times1" )"1" rewrite "zero_times1" )"1" rewrite "zero_times1" )"1" rewrite "zero_times2" )"1" assert )"1" "Im_imag" "x" "sin(r!1)" ))"1" rewrite "commutative_mult" "1" replace -1)"1" rewrite "sq.sq_rew" )"1" rewrite "Re_real" 1)"1" rewrite "sq.sq_rew" )"1" assert )"1" rewrite "associative_mult" "1" rewrite "i_axiom" )"1" assert )"1" rewrite "minus_add" )"1" rewrite "number_fields_times_negative" "1" rewrite "number_fields_negate_negate" )"1" "sin2_cos2" "a" "r!1" ))"1" assert )"1" replace "1" rewrite "sqrt_1" )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" (rewrite "closed_times" )"2" (rewrite "real_is_complex" ) nil nil )) nil )"3" (rewrite "real_is_complex" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil exp nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"trig_range" trig_basic"trig/" )"complex" complex_types nil )"trig_range" trig_basic"trig/" )"complex" complex_types nil )"real" complex_types nil )"real" realsnil )"real" complex_types nil )"complex" complex_types nil )"complex" arithmetic nil )nil arithmetic nil )nil arithmetic nil )nil number_fields_bis nil )nil sq "reals/" )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )nil number_fields nil )nil nil )"real" reals nil )nil trig_basic "trig/" )nil sqrt "reals/" )"nnreal" nil )nil number_fields_bisnil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil complex_types nil )nil arithmetic nil )nil arithmetic nil )"even_int" integersnil )"(divides(m))" dividesnil )"(divides(n))" dividesnil )"even_int" nil )nil number_fields_bis nil )"odd_int" integers nil )"nzcomplex" nil )"complex" nil )"nznum" nil )nil arithmetic nil )nil number_fields nil )"real" reals nil )nil arithmetic nil )"[number_field -> boolean]" nil )nil complex_types nil )"real" trig_basic "trig/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"complex" complex_types nil )"real" trig_basic "trig/" )"nnreal" polar nil ))nil 3294848302"" (skosimp)"" (rewrite "exp_real" )"" (typepred "ln_exp.exp(r!1)" )"" (rewrite "arg_is_0" 1)"" (rewrite "Re_real" )"" (rewrite "Im_real" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil exp nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"complex" complex_types nil )nil polar nil )"[number_field -> boolean]" nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"(total_order?[real])" nil )nil arithmetic nil )nil arithmetic nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" ))nil 3294848362"" (skosimp)"" (rewrite "exp_imag" )"" (typepred "theta!1" )"" (expand "arg" )"" (rewrite "Im_plus" )"1" (rewrite "Im_real" )"1" (rewrite "Re_plus" )"1" (lemma "Re_imag" ("x" "sin(theta!1)" ))"1" (assert )"1" (lemma "Im_imag" ("x" "sin(theta!1)" ))"1" (rewrite "commutative_mult" )"1" (replace -1)"1" replace -2)"1" "1" assert )"1" rewrite "Re_real" )"1" "1" "1" "unique_characterization" "x0" "cos(theta!1)" "x1" "0" "y0" "sin(theta!1)" "y1" "0" ))"1" rewrite "zero_times1" "1" rewrite "commutative_mult" "1" replace -2)"1" "1" "1" "sin_cos_eq_0" "a" "theta!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "0<=theta!1" )"1" "1" "sin_ge_0" "a" "theta!1" ))"1" assert )nil nil ))nil ))nil )"2" "atan2_cos_sin" "a" "-theta!1" ))"1" rewrite "cos_neg" )"1" rewrite "sin_neg" )"1" expand "atan2" )"1" "cos(theta!1) > 0" )"1" assert )"1" "atan_neg" )"1" "sin(theta!1) / cos(theta!1)" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "cos(theta!1)=0" )"1" assert )nil nil )"2" assert )"2" "atan_neg" "x" "sin(theta!1) / cos(theta!1)" ))"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" "0<=theta!1" )"1" rewrite "atan2_cos_sin" )nil nil )"2" "2" "sin_gt_0" "a" "-theta!1" ))"2" rewrite "sin_neg" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "closed_times" )"2" (rewrite "real_is_complex" ) nil nil )) nil )"3" (rewrite "real_is_complex" ) nil nil ))nil ))nil )"2" (rewrite "closed_times" )"2" (rewrite "real_is_complex" ) nil nil )) nil )"3" (rewrite "real_is_complex" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil exp nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals 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/" )"bool" reals nil )nil polar nil )"trig_range" trig_basic"trig/" )"complex" complex_types nil )"trig_range" trig_basic"trig/" )"complex" complex_types nil )"argrng" polar nil )nil arithmetic nil )nil arithmetic nil )nil arithmetic nil )nil arithmetic nil )nil number_fields_bis nil )nil trig_aux nil )nil complex_types nil )"real" reals nil )nil atan2 "trig/" )nil real_types nil )"(total_order?[real])" nil )nil trig_basic "trig/" )nil atan "trig/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"(strict_total_order?[real])" real_props nil )"complex" complex_types nil )"real" realsnil )"complex" complex_types nil )"real" realsnil )"[T, T -> boolean]" equalities nil )"nznum" nil )"real" atan2 "trig/" )nil trig_basic "trig/" )nil trig_ineq "trig/" )nil trig_ineq "trig/" )nil number_fields nil )"real" complex_types nil )"(strict_total_order?[real])" real_props nil )"nznum" nil )"complex" nil )"nzcomplex" nil )"nzreal" nil )"(total_order?[real])" nil )nil arithmetic nil )"real" reals nil )"posreal" real_types nil )"nzcomplex" complex_types nil )"nznum" nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"real" trig_basic "trig/" )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fieldsnil )"real" trig_basic "trig/" )nil complex_types nil )"[number_field -> boolean]" nil )nil arithmetic nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3294273290"" (expand "exp" )"" (rewrite "Re_real" )"" (rewrite "Im_real" )"" (rewrite "exp_0" )"" (rewrite "sin_0" )"" (rewrite "cos_0" )"" (rewrite "zero_times1" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil ln_exp "lnexp/" )nil trig_basic "trig/" )"odd_int" integersnil )"posint" nil )"complex" complex_types nil )nil number_fields_bis nil )"[number_field -> boolean]" nil )nil complex_types nil )"complex" complex_types nil )nil trig_basic "trig/" )nil arithmetic nil )"nzcomplex" exp nil )"trig_range" trig_basic"trig/" )"real" realsnil )"trig_range" trig_basic"trig/" )"complex" complex_types nil ))nil 3294274905"" (expand "exp" )"" (expand "e" )"" (rewrite "Re_real" )"" (rewrite "Im_real" )"" (rewrite "sin_0" )"" (rewrite "cos_0" )"" (rewrite "zero_times2" )"" (rewrite "zero_times1" )"" (rewrite "identity_mult" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" ln_exp "lnexp/" )nil arithmetic nil )nil trig_basic "trig/" )"nnreal" nil )"complex" complex_types nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields nil )nil ln_exp "lnexp/" )"posreal" real_types nil )"nzcomplex" complex_types nil )"nznum" nil )nil number_fields_bis nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" )nil trig_basic "trig/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil arithmetic nil )"nzcomplex" exp nil )"trig_range" trig_basic"trig/" )"real" realsnil )"trig_range" trig_basic"trig/" )"complex" complex_types nil ))nil 3294274991"" (lemma "exp_imag" ("r" "pi" ))"" (rewrite "cos_pi" )"" (rewrite "sin_pi" )"" (rewrite "zero_times2" )"" (assert )"" (rewrite "commutative_mult" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic "trig/" )"trig_range" trig_basic"trig/" )"complex" complex_types nil )"odd_int" integers nil )"nzcomplex" nil )"complex" nil )"nznum" nil )"complex" complex_types nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields_bis nil )nil number_fields nil )nil number_fields nil )"complex" complex_types nil )"odd_int" integersnil )nil trig_basic "trig/" )nil exp nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans 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/" )"bool" reals nil )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" "trig/" ))nil 3294335316"" (skosimp)"" (expand "exp" )"" (rewrite "Re_plus" )"" (rewrite "Im_plus" )"" (rewrite "sin_plus" )"" (rewrite "cos_plus" )"" (rewrite "exp_sum" 1)"" (assert )"" "DRL101" "ln_exp.exp(Re(x!1)) * ln_exp.exp(Re(y!1)) * sin(Im(x!1)) * sin(Im(y!1))" )"" (rewrite "associative_mult" 1 :dir rl)"" (rewrite "i_axiom" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_types nil )"trig_range" trig_basic"trig/" )"real" realsnil )"trig_range" trig_basic"trig/" )"nznum" nil )"nzcomplex" complex_types nil )"posreal" real_types nil )"nzcomplex" exp nil )nil arithmetic nil )nil trig_basic "trig/" )"real" realsnil )"complex" complex_types nil )nil number_fields nil )"nznum" nil )"complex" nil )"nzcomplex" nil )"odd_int" integers nil )nil complex_types nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" )"real" trig_basic "trig/" )nil ln_exp "lnexp/" )"{x | EXISTS y: z = x + y * i}" complex_typesnil )nil trig_basic "trig/" )"[number_field -> boolean]" reals nil )nil reals nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"complex" complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_typesnil )"complex" complex_types nil )"real" reals nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" nil )nil complex_types nil ))nil 3294275508"" (skosimp)"" (expand "exp" )"" (rewrite "Re_neg" )"" (rewrite "Im_neg" )"" (rewrite "sin_neg" )"" (rewrite "cos_neg" )"" (rewrite "exp_neg" )"" (assert )"" (typepred "ln_exp.exp(Re(x!1))" )"" (hide -1 -3)"" (name-replace "R" "ln_exp.exp(Re(x!1))" )"" (rewrite "div_cancel4" 1)"" assert )"" "number_fields_negative_times" "x" "1" "y" "sin(Im(x!1))" ))"" rewrite "identity_mult" )"" replace -1 * rl)"" "" assert )"" assert )"" rewrite "commutative_mult" "" rewrite "commutative_mult" "" assert )"" rewrite "sq.sq_rew" )"" rewrite "sq.sq_rew" )"" rewrite "associative_mult" "" rewrite "i_axiom" )"" assert )"" rewrite "minus_add" "" rewrite "number_fields_times_negative" "" assert )"" rewrite "number_fields_negate_negate" "" rewrite "commutative_mult" "" rewrite "identity_mult" )"" "sin2_cos2" "a" "Im(x!1)" ))"" 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 )"complex" complex_types nil )"trig_range" trig_basic"trig/" )"real" realsnil )"trig_range" trig_basic"trig/" )"nzcomplex" exp nil )nil arithmetic nil )nil trig_basic "trig/" )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"real" trig_basic "trig/" )"real" trig_basic "trig/" )nil number_fields nil )"boolean" notequal nil )nil number_fields_bis nil )nil nil )nil number_fields nil )nil complex_types nil )nil number_fields nil )"real" reals nil )"nnreal" nil )nil trig_basic "trig/" )"nnreal" nil )nil number_fields_bisnil )nil nil )"real" realsnil )nil number_fields nil )"nonneg_real" sq "reals/" )nil sq "reals/" )"complex" complex_types nil )"odd_int" integers nil )"nzcomplex" nil )"nznum" nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )"{py | x = ln(py)}" ln_exp "lnexp/" )"real" ln_exp "lnexp/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )"nznum" nil )"complex" complex_types nil )"nzcomplex" complex_types nil )"posreal" nil )nil ln_exp "lnexp/" )"{x | EXISTS y: z = x + y * i}" complex_typesnil )nil trig_basic "trig/" )"[number_field -> boolean]" reals nil )nil reals nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"complex" complex_types nil )"{y | EXISTS x: z = x + y * i}" complex_typesnil )"complex" nil )"real" reals nil )"complex" complex_types nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil arithmetic nil ))nil 3294334655"" (skosimp)"" (rewrite "minus_add" )"" (rewrite "exp_plus" )"" (rewrite "exp_negate" )"" (rewrite "commutative_mult" )"" (rewrite "div_def" 1 :dir rl) nil nil )) nil ))nil ))nil ))nil ))nil )nil number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )nil number_fields nil )"[number_field -> boolean]" nil )nil complex_types nil )"nznum" nil )"nzcomplex" nil )"odd_int" integers nil )"complex" nil )"complex" complex_types nil )nil exp nil )"nzcomplex" complex_types nil )"complex" complex_types nil )"nznum" nil )nil number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil complex_types nil )"nzcomplex" exp nil )"nznum" nil )"complex" complex_types nil )"nzcomplex" complex_types nil )nil exp nil )"[numfield -> numfield]" number_fields nil ))nil 3295026159"" (skosimp)"" (expand "exp" )"" (lemma "Re_imag" ("x" "2 * j!1 * pi" ))"" (assert )"" (lemma "Im_imag" ("x" "2 * j!1 * pi" ))"" (assert )"" (rewrite "Re_plus" )"" (rewrite "Im_plus" )"" (replace -1)"" (replace -2)"" (assert )"" "sin_period" "a" "Im(x!1)" "j" "j!1" ))"" replace -1 1 rl)"" "cos_period" "a" "Im(x!1)" "j" "j!1" ))"" replace -1 1 rl)"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_types nil )"trig_range" trig_basic"trig/" )"real" realsnil )"trig_range" trig_basic"trig/" )"nzcomplex" exp nil )"complex" complex_types nil )"(divides(n))" dividesnil )"even_int" nil )"real" complex_types nil )"real" complex_types nil )nil arithmetic nil )nil trig_basic "trig/" )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{y | EXISTS x: z = x + y * i}" complex_typesnil )nil integers nil )nil trig_basic "trig/" )"real" reals nil )nil arithmetic nil )"[number_field -> boolean]" nil )nil complex_types nil )"complex" complex_types nil )nil arithmetic nil )nil arithmetic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans 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/" )"bool" reals nil )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" "trig/" ))nil 3294844650"" (skosimp)"" (expand "exp" )"" "abs_mult" "z1" "ln_exp.exp(Re(z!1))" "z2" "sin(Im(z!1)) * i + cos(Im(z!1))" ))"1" (typepred "ln_exp.exp(Re(z!1))" )"1" (expand "abs" -4 2)"1" (expand "conjugate" )"1" (lemma "Im_real" ("x" "ln_exp.exp(Re(z!1))" ))"1" (replace -1)"1" (rewrite "zero_times1" )"1" (rewrite "zero_times1" )"1" "Re_real" "x" "ln_exp.exp(Re(z!1))" ))"1" (replace -1)"1" "sq.sq_rew" "a" "ln_exp.exp(Re(z!1))" ))"1" replace -1)"1" rewrite "sqrt_sq" )"1" replace -7 1)"1" "1" "abs_exp_imag" "r" "Im(z!1)" ))"1" rewrite "exp_imag" -1)"1" rewrite "commutative_mult" "1" replace -1)"1" rewrite "commutative_mult" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "closed_plus" )"1" (rewrite "closed_times" )"1" (rewrite "real_is_complex" ) nil nil )) nil )"2" (rewrite "real_is_complex" ) nil nil ))nil )"3" (rewrite "real_is_complex" ) nil nil ))nil ))nil ))nil )"trig_range" trig_basic"trig/" )"real" realsnil )"trig_range" trig_basic"trig/" )"nzcomplex" exp nil )NOT const-decl "[bool -> bool]" booleans nil )"real" complex_types nil )"real" complex_types nil )"complex" arithmetic nil )"nznum" nil )"nzcomplex" complex_types nil )"posreal" real_types nil )nil exp nil )nil number_fields nil )nil exp nil )"posreal" sqrt "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil arithmetic nil )"nnreal" nil )nil number_fields_bis nil )nil arithmetic nil )"nnreal" polar nil )"complex" complex_types nil )nil polar nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" nil )nil complex_types nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"complex" complex_types nil )"{x | EXISTS y: z = x + y * i}" complex_typesnil )"real" trig_basic "trig/" )"{y | EXISTS x: z = x + y * i}" complex_typesnil )"real" trig_basic "trig/" )"complex" complex_types nil ))nil 3294846787"" (skosimp) (("" (rewrite "abs_nzcomplex" ) nil nil )) nil )nil polar nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" nil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil ))nil 3294846944"" (expand "ln" )"" (expand "abs" )"" (expand "conjugate" )"" (expand "arg" )"" (rewrite "Re_real" )"" (rewrite "Im_real" )"" (rewrite "zero_times1" )"" (assert )"" (expand "atan2" )"" (rewrite "atan_0" )"" (rewrite "zero_times1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" polar nil )"argrng" polar nil )nil arithmetic nil )"(strict_total_order?[real])" real_props nil )"complex" complex_types nil )"complex" complex_types nil )nil sqrt "reals/" )nil ln_exp "lnexp/" )nil atan "trig/" )"real" atan2 "trig/" )nil number_fields_bis nil )"[number_field -> boolean]" nil )nil complex_types nil )"complex" complex_types nil )"posreal" real_types nil )"nzcomplex" complex_types nil )"nznum" nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"odd_int" integers nil )"nzcomplex" nil )"complex" nil )"nznum" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil arithmetic nil )"complex" arithmetic nil )"real" complex_types nil )"real" complex_types nil )"complex" complex_types nil )"complex" exp nil ))nil 3294847041"" (expand "ln" )"" (expand "abs" )"" (expand "conjugate" )"" (expand "arg" )"" (typepred "e" )"" (rewrite "Re_real" )"" (rewrite "Im_real" )"" (assert )"" (expand "atan2" )"" (rewrite "atan_0" )"" (rewrite "zero_times1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" polar nil )"argrng" polar nil )nil arithmetic nil )"nznum" nil )"nzcomplex" complex_types nil )"posreal" real_types nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"(strict_total_order?[real])" real_props nil )"complex" complex_types nil )"complex" complex_types nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sqrt "reals/" )nil ln_exp "lnexp/" )nil atan "trig/" )nil number_fields_bis nil )"[number_field -> boolean]" nil )nil complex_types nil )"complex" complex_types nil )"real" atan2 "trig/" )nil arithmetic nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" ln_exp "lnexp/" )"complex" arithmetic nil )"real" complex_types nil )"real" realsnil )"real" complex_types nil )"complex" complex_types nil )"complex" exp nil ))nil 3294847345"" (skosimp)"" (expand "ln" 1)"" (rewrite "abs_exp" 1)"" (rewrite "ln_exp" 1)"" (lemma "exp_plus" ("x" "Re(z!1)" "y" "Im(z!1)*i" ))"1" (lemma "complex_is_Re_Im" ("z" "z!1" ))"1" (replace -1 -2 rl)"1" (typepred "exp(Re(z!1))" )"1" (typepred "exp(Im(z!1) * i)" )"1" (hide -1 -2 -4 -5)"1" "arg_mult" "n0x" "exp(Re(z!1))" "n0y" "exp((Im(z!1)-2*j!1*pi)*i)" ))"1" "arg_exp_imag" "theta" "Im(z!1)-2*j!1*pi" ))"1" replace -1)"1" "arg_exp_real" "r" "Re(z!1)" ))"1" replace -1)"1" "exp_periodicity" "x" "Im(z!1)*i" "j" "(-1)*j!1" ))"1" assert )"1" replace -1 * LR)"1" assert )"1" replace -8 -4 rl)"1" replace -4 1)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert )"2" rewrite "closed_minus" )"2" rewrite "closed_times" )"1" rewrite "closed_times" )"1" rewrite "real_is_complex" )nil nil )"2" rewrite "closed_times" )"2" rewrite "real_is_complex" )nil nil ))nil ))nil )"2" rewrite "real_is_complex" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "closed_times" )"2" (rewrite "real_is_complex" ) nil nil )) nil )"3" (rewrite "real_is_complex" ) nil nil ))nil ))nil ))nil ))nil ))nil )"complex" exp nil )"{x | EXISTS y: z = x + y * i}" complex_typesnil )"complex" complex_types nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil ln_exp "lnexp/" )nil arithmetic nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"boolean" notequal nil )nil complex_types nil )"nzcomplex" exp nil )nil exp nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil polar nil )"(strict_total_order?[real])" real_props nil )"nznum" nil )"complex" nil )"nzcomplex" nil )"nzreal" nil )"(total_order?[real])" nil )nil exp nil )nil exp nil )"nzint" integersnil )"even_int" integersnil )"real" reals nil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"odd_int" integers nil )"posreal" real_types nil )"nzcomplex" complex_types nil )"nznum" nil )"{r: posreal | r > pi_lb AND r < pi_ub}" "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 integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil polar nil )"real" realsnil )"{y | EXISTS x: z = x + y * i}" complex_typesnil )nil exp nil )"real" complex_types nil )"odd_int" integersnil )"complex" complex_types nil )"odd_int" integersnil )"complex" complex_types nil )"(divides(m))" dividesnil )"(divides(n))" dividesnil )"even_int" nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil exp nil )"complex" complex_types nil ))nil 3294854711"" (skosimp)"" (typepred "n0z!1" )"" (expand "ln" )"" (rewrite "exp_plus" )"1" (rewrite "exp_real" )"1" (lemma "abs_nzcomplex" ("n0z" "n0z!1" ))"1" (rewrite "exp_ln" 1)"1" (rewrite "exp_imag" )"1" (lemma "idempotent_polar" ("n0z" "n0z!1" ))"1" (expand "polar" )"1" (expand "from_polar" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "closed_times" )"2" (rewrite "real_is_complex" ) nil nil )) nil )"3" (rewrite "real_is_complex" ) nil nil ))nil ))nil ))nil ))nil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"complex" complex_types nil )nil exp nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp/" )nil real_types nil )"nnreal" polar nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" "trig/" )"bool" reals nil )nil polar nil )"argrng" polar nil )"complex" complex_types nil )"nzcomplex" complex_types nil )"nznum" nil )nil polar nil )nil exp nil )"trig_range" trig_basic"trig/" )"trig_range" trig_basic"trig/" )"complex" complex_types nil )"[nnreal, argrng]" polar nil )"(strict_total_order?[real])" real_props nil )"complex" polar nil )"real" realsnil )nil polar nil )nil ln_exp "lnexp/" )nil exp nil )"complex" exp nil ))nil 3294856600"" (skosimp*)"" (expand "ln" )"" (rewrite "abs_mult" )"" (rewrite "arg_mult" )"" (lemma "abs_nz_iff_nz" ("z" "n0x!1" ))"" (lemma "abs_nz_iff_nz" ("z" "n0y!1" ))"" (assert )"" (rewrite "ln_mult" )"" "arg(n0x!1) + arg(n0y!1) > pi" )"1" (assert ) nil nil )"2" "arg(n0x!1) + arg(n0y!1) <= -pi" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_types nil )"complex" exp nil )nil polar nil )"(strict_total_order?[real])" real_props nil )nil ln_exp "lnexp/" )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"nnreal" polar nil )"nznum" nil )"nzreal" nil )"nzcomplex" nil )"complex" nil )"nznum" nil )"(total_order?[real])" nil )"complex" complex_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"{r: posreal | r > pi_lb AND r < pi_ub}" "trig/" )"bool" reals nil )nil polar nil )"argrng" polar nil )nil polar nil )"nnreal" nil )"real" reals nil )"complex" complex_types nil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil polar nil ))nil 3294948253"" (skosimp)"" (expand "ln" )"" (rewrite "abs_inv" )"" (rewrite "arg_inv" )"" (lemma "ln_div" )"" (lemma "abs_nz_iff_nz" ("z" "n0x!1" ))"" (assert )"" (inst - "1" "abs(n0x!1)" )"" (rewrite "ln_exp_ax.ln_1" )"" (replace -2)"" (case-replace "arg(n0x!1) = 0" )"1" (assert )"1" (rewrite "zero_times1" ) nil nil ))nil )"2" (assert )"2" "arg(n0x!1) = pi" )"1" "2 * pi * i - pi * i = i*(2*pi-pi)" )"1" assert )"1" rewrite "commutative_mult" 2)nil nil ))nil )"2" "2" "minus_add" "x" "2*pi" "y" "pi" ))"2" "DRL1" "2 * pi * i - pi * i" )"2" replace -1)"2" replace -2 1)"2" rewrite "distributive" "2" rewrite "minus_add" "2" replace -1 1 rl)"2" rewrite "commutative_mult" "2" assert )"2" rewrite "number_fields_times_negative" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" rewrite "associative_mult" 3)"2" "associative_mult" "x" "-1" "y" "arg(n0x!1)" "z" "i" ))"2" replace -1 3)"2" "both_sides_times1" "x" "-arg(n0x!1)" "n0z" "i" "y" "-1 * arg(n0x!1)" ))"1" (assert ) nil nil )"2" assert )"2" "i_not_real" "r" "0" ))"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" exp nil )nil polar nil )nil polar nil )"nnreal" polar nil )nil real_types 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 )"argrng" polar nil )nil polar nil )"bool" reals nil )"{r: posreal | r > pi_lb AND r < pi_ub}" "trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"complex" complex_types nil )nil number_fields_bis nil )nil ln_exp "lnexp/" )"real" realsnil )nil nil )"real" reals nil )nil number_fields nil )"nzreal" nil )"nzcomplex" nil )"complex" nil )"nznum" nil )"posreal" real_types nil )"nzcomplex" complex_types nil )nil number_fields nil )"real" realsnil )nil number_fields nil )"nznum" nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields_bis nil )nil number_fields nil )nil complex_types nil )"odd_int" integers nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )"complex" complex_types nil )"complex" complex_types nil )nil ln_exp "lnexp/" )"nznum" nil )"complex" complex_types nil )"nzcomplex" complex_types nil )"nzreal" nil )"complex" complex_types nil )nil complex_types nil )"boolean" notequal nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil polar nil ))nil 3295030968"" (skosimp)"" (lemma "div_def" ("y" "n0x!1" "n0x" "n0y!1" ))"" (replace -1)"" (lemma "inv_ne_0" ("n0x" "n0y!1" ))"" (lemma "ln_inv" ("n0x" "n0y!1" ))"" (lemma "ln_mult" ("n0x" "n0x!1" "n0y" "1/n0y!1" ))"" (replace -1)"" (replace -2)"" (hide-all-but (1 -3))"" (assert )"" (rewrite "arg_inv" )"" (assert )"" "arg(n0y!1) = pi" )"1" assert )"1" case "arg(n0x!1)>0" )"1" (assert ) nil nil )"2" assert )"2" "number_fields_negative_times" "x" "1" "y" "-2*i*pi" ))"2" rewrite "identity_mult" -1)"2" rewrite "number_fields_negative_times" "2" rewrite "number_fields_negate_negate" )"2" replace -1 2 rl)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "arg(n0y!1) = 0" )"1" (assert ) nil nil )"2" assert )"2" assert )"2" rewrite "minus_add" 3)nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil number_fields nil )nil complex_types nil )nil complex_types nil )"[number_field -> boolean]" nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil number_fields nil )nil number_fields_bis nil )"nznum" nil )"complex" complex_types nil )"nzcomplex" complex_types nil )nil exp nil )"[numfield, nznum -> numfield]" number_fieldsnil )"complex" complex_types nil )"odd_int" integers nil )"real" reals nil )"real" realsnil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"nzreal" nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"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/" )"bool" reals nil )nil polar nil )"argrng" polar nil )nil polar nil )nil exp nil )"nzreal" nil )"even_int" integersnil )"nzint" integersnil )"nzcomplex" nil )"complex" nil )"nznum" nil )"posreal" real_types nil )"nzcomplex" complex_types nil )"complex" complex_types nil )"nznum" nil )"complex" complex_types nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.49 Sekunden
(vorverarbeitet am 2026-04-29)
¤ *© Formatika GbR, Deutschland
