Quelle complex_lnexp.prf
Sprache: Lisp
(complex_lnexpnil 3294275262"" (skosimp)"" (assert )"" (rewrite "zero_times3" )"" (rewrite "zero_times3" )"" (lemma "sin_cos_eq_0" ("a" "Im(z!1)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_types nil )"real" trig_basic "trig/" )nil trig_aux nil )"real" complex_types nil )"real" trig_basic "trig/" )"real" complex_types nil )nil complex_types 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 booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil ))nil 3456000255 ("" (grind) nil nil )"real" complex_types nil )"real" complex_types nil )"nzcomplex" complex_lnexp nil )"trig_range" trig_basic "trig/" ))nil 3456000259 ("" (grind) nil nil )"real" complex_types nil )"real" complex_types nil )"nzcomplex" complex_lnexp nil )"trig_range" trig_basic "trig/" ))nil 3294274991"" (assert )"" (rewrite "cos_pi" ) (("" (rewrite "sin_pi" ) nil nil )) nil ))nil )nil trig_basic "trig/" )nil trig_basic "trig/" )nil complex_types nil )nil complex_types nil )nil ln_exp "lnexp/" )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )"nzcomplex" complex_typesnil )"odd_int" integers nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" ))nil 3294335316"" (skosimp)"" (assert )"" (rewrite "exp_sum" )"" (rewrite "cos_plus" )"" (rewrite "sin_plus" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"posreal" nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )"nzcomplex" complex_typesnil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )"real" complex_types nil )nil trig_basic "trig/" )nil trig_basic "trig/" )nil ln_exp "lnexp/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil complex_types nil )"real" complex_types nil ))nil 3294275508"" (skosimp)"" (assert )"" (rewrite "exp_neg" )"" (typepred "exp(x!1)" )"" (lemma "nz_sq_abs_pos" ("n0z" "exp(x!1)" ))"" (rewrite "div_cancel4" 1)"" (rewrite "div_cancel4" 1)"" (rewrite "cos_neg" )"" (rewrite "sin_neg" )"" "div_cancel3" "n0z" "exp(Re(x!1))" "x" "cos(Im(x!1)) * sq_abs(exp(x!1))" "y" "exp(Re(x!1)) * cos(Im(x!1))" ))"" (replace -1)"" (hide -1)"" "div_cancel3" "n0z" "exp(Re(x!1))" "x" "(-1)*sin(Im(x!1)) * sq_abs(exp(x!1))" "y" "(-1)*exp(Re(x!1)) * sin(Im(x!1))" ))"" (replace -1)"" "" expand "sq_abs" )"" assert )"" rewrite "sq_times" )"" rewrite "sq_times" )"" "sin2_cos2" "a" "Im(x!1)" ))"" "sq_nz_pos" "nz" "exp(Re(x!1))" ))"" "both_sides_times1" "n0z" "sq(exp(Re(x!1)))" "x" "sq(sin(Im(x!1))) + sq(cos(Im(x!1)))" "y" "1" ))"" replace -1 -3 rl)"" expand "sq" -3 4)"" 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 )"trig_range" trig_basic "trig/" )"posreal" complex_types nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )"nzcomplex" complex_typesnil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" complex_types nil )nil complex_types nil )"nzcomplex" complex_lnexp nil )"[numfield -> numfield]" number_fields nil )"real" trig_basic "trig/" )"{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 )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nnreal" complex_types nil )nil real_types nil )"bool" reals nil )nil reals nil )nil real_props nil )nil trig_basic "trig/" )nil real_props nil )"odd_int" integers nil )"nzreal" nil )"posreal" nil )nil sq "reals/" )"posreal" sq "reals/" )"nnreal" nil )nil trig_basic "trig/" )nil real_props nil )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil sq "reals/" )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"real" reals nil )nil trig_basic "trig/" )"real" trig_basic "trig/" )nil complex_types nil )"posreal" nil )nil ln_exp "lnexp/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil complex_types nil )"real" complex_types nil ))nil 3294334655"" (skosimp)"" (lemma "exp_negate" ("x" "y!1" ))"" (lemma "exp_plus" ("x" "x!1" "y" "-y!1" ))"" (assert )"" (flatten)"" (rewrite "cos_neg" )"" (rewrite "sin_neg" )"" (rewrite "exp_neg" )"" (replace -1)"" (replace -2)"" (hide -1 -2)"" (split)"1" (cross-mult)"1" "div_distributes_minus" "x" "sq_abs(exp(y!1)) * cos(Im(x!1)) * cos(Im(y!1)) * exp(Re(x!1))" "y" "sq_abs(exp(y!1)) * exp(Re(x!1)) * sin(Im(x!1)) * -sin(Im(y!1))" "n0z" "exp(Re(y!1))" ))"1" replace -1)"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (cross-mult)"2" "div_distributes" "x" "sq_abs(exp(y!1)) * cos(Im(x!1)) * -sin(Im(y!1)) * exp(Re(x!1))" "y" "sq_abs(exp(y!1)) * exp(Re(x!1)) * sin(Im(x!1)) * cos(Im(y!1))" "n0z" "exp(Re(y!1))" ))"2" replace -1)"2" "2" "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 )nil complex_lnexp nil )"nzcomplex" complex_typesnil )"posreal" complex_types nil )"real" reals nil )"nzcomplex" complex_typesnil )"posreal" nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )"real" reals nil )"nzcomplex" complex_typesnil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic "trig/" )"real" complex_types nil )nil ln_exp "lnexp/" )"posreal" nil )nil real_props nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nzcomplex" complex_lnexp nil )nil complex_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"nnreal" complex_types nil )nil real_types nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )"real" trig_basic "trig/" )nil real_props nil )"real" trig_basic "trig/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 booleans nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"odd_int" integers nil )nil real_props nil )nil trig_basic "trig/" )nil complex_lnexp nil )"complex" complex_types 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 )"real" reals nil )"nzcomplex" complex_lnexp nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic "trig/" )nil trig_basic "trig/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" ))nil 3294844650"" (skosimp)"" (assert )"" (expand "abs" )"" (expand "sq_abs" )"" (assert )"" (rewrite "sq_eq" 1 :dir rl)"" (assert )"" (lemma "sin2_cos2" ("a" "Im(z!1)" ))"" (assert )"" (rewrite "sq_times" )"" (rewrite "sq_times" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" polar nil )"nnreal" complex_types nil )nil sq "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" )nil complex_types nil )"real" complex_types nil )"real" trig_basic "trig/" )"real" complex_types nil )"real" trig_basic "trig/" )"posreal" sq "reals/" )"(total_order?[real])" nil )nil trig_basic "trig/" )nil sq "reals/" )"nnreal" nil )nil sqrt "reals/" )nil complex_lnexp nil )nil complex_lnexp nil )"nnreal" nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"nnreal" polar nil ))nil 3456123074"" (skosimp)"" (assert )"" (expand "exp" )"" (expand "arg" )"" (assert )"" (rewrite "zero_times3" )"" (rewrite "zero_times3" )"" "cos(Im(z!1)) = 0 AND sin(Im(z!1)) = 0" )"1" (lemma "sin_cos_eq_0" ("a" "Im(z!1)" ))"1" (flatten) (("1" (assert ) nil nil )) nil )) nil )"2" (replace 1 2)"2" (hide 1)"2" "both_sides_times_pos_lt1" "pz" "exp(Re(z!1))" "x" "sin(Im(z!1))" "y" "0" ))"2" (replace -1)"2" (hide -1)"2" "atan2_cancel_pos" "x" "cos(Im(z!1))" "y" "sin(Im(z!1))" "pz" "exp(Re(z!1))" ))"2" "1" replace -1)"1" "1" case "0<=Im(z!1)" )"1" "sin_ge_0" "a" "Im(z!1)" ))"1" assert )"1" "1" rewrite "atan2_cos_sin" )nil nil ))nil ))nil ))nil )"2" case "Im(z!1)<0" )"1" "1" "sin_period" "a" "Im(z!1)" "j" "1" ))"1" "cos_period" "a" "Im(z!1)" "j" "1" ))"1" replace -1)"1" replace -2)"1" "1" "sin_lt_0" "a" "Im(z!1) + 2 * 1 * pi" ))"1" assert )"1" rewrite "atan2_cos_sin" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "sin_cos_eq_0" "a" "Im(z!1)" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"nzreal" real_typesnil )"(strict_total_order?[real])" real_props nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"argrng" polar nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )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 )"[T, T -> boolean]" equalities nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" )nil complex_types nil )"real" complex_types nil )"real" trig_basic "trig/" )"real" complex_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil trig_aux nil )nil atan2 "trig/" )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"posreal" nil )"bool" reals nil )"(total_order?[real])" nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic"trig/" )"posreal" trig_basic "trig/" )"posreal" trig_basic "trig/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil real_types nil )nil atan2 "trig/" )nil trig_ineq "trig/" )nil trig_basic "trig/" )"real" reals nil )nil trig_ineq "trig/" )"[numfield, numfield -> numfield]" number_fields nil )"nzint" integers nil )"even_int" integers nil )"real" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil trig_basic "trig/" )nil real_props nil )"real" trig_basic "trig/" )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" reals nil )"nzcomplex" complex_lnexp nil ))nil 3456000946"" (skosimp) (("" (expand "ln" 1 1) (("" (assert ) nil nil )) nil ))nil )"complex" complex_lnexp nil )"posreal" polar nil )nil complex_types nil ))nil 3456000994"" (skosimp) (("" (expand "ln" 1 1) (("" (assert ) nil nil )) nil ))nil )"complex" complex_lnexp nil )"posreal" polar nil )nil complex_types nil ))nil 3294847345"" case "FORALL (z: complex): AND Im(z) <= pi =>") "1" (skosimp)"1" (inst - "z!1+(2 * -j!1 * pi) * complex_i" )"1" (split)"1" (lemma "exp_periodicity" ("x" "z!1" "j" "-j!1" ))"1" (assert )"1" (flatten)"1" (expand "arg" )"1" (assert )"1" (replace -1)"1" (replace -2)"1" (assert )"1" "exp(Re(z!1)) * cos(Im(z!1)) = 0 AND ") "1" (assert ) nil nil )"2" (replace 1)"2" "exp(Re(z!1)) * sin(Im(z!1)) < 0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2) (("2" (skosimp) (("2" (assert ) nil nil )) nil )) nil ))nil )nil complex_lnexp nil )"real" reals nil )"odd_int" integers nil )"odd_int" integersnil )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" polar nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )"argrng" polar nil )nil application-judgement "nnreal_lt_2pi" atan2 "trig/" )"posreal" nil )"[T, T -> boolean]" equalities nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" )"real" trig_basic "trig/" )"real" trig_basic "trig/" )nil complex_types nil )nil complex_lnexp nil )"int" integers nil )"nzcomplex" complex_types nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )"complex" complex_types nil )"complex" complex_types nil )"real" reals nil )"nzreal" real_typesnil )nil complex_types nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, 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 )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/" )"real" complex_types nil )"bool" reals nil )"bool" complex_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" complex_types nil )nil complex_types nil )"complex" complex_lnexp nil )"nzcomplex" complex_lnexp nil ))nil 3294854711"" (skosimp)"" (assert )"" (rewrite "exp_ln" )"" (lemma "Re_cos_abs1" ("n0x" "n0z!1/abs(n0z!1)" ))"" (lemma "Im_sin_abs1" ("n0x" "n0z!1/abs(n0z!1)" ))"" (lemma "arg_div_abs" ("n0x" "n0z!1" ))"" (replace -1 * rl)"" (hide -1)"" (rewrite "abs_div2" )"" (rewrite "div_simp" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"posreal" polar nil )"real" reals nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )"nzcomplex" complex_typesnil )nil polar nil )nil reals nil )"complex" complex_types nil )nil polar nil )nil reals nil )nil real_props nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil polar nil )"posreal" nil )"{y: posreal | y >= x}" nil )"(total_order?[real])" nil )nil polar nil )nil polar nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"nnreal" polar nil )nil real_types nil )nil complex_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 )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_exp "lnexp/" ))nil 3294856600"" (skosimp)"" (assert )"" (rewrite "ln_mult" )"" (rewrite "arg_mult" )"" (lift-if) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"even_int" integers nil )"nzint" integers nil )"real" reals nil )"real" reals nil )"posreal" nil )"posreal" polar nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"nzcomplex" complex_typesnil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil polar nil )nil polar nil )nil ln_exp "lnexp/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )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 )nil complex_types nil )nil real_types nil )"nnreal" polar nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" complex_types nil )"real" complex_types nil )nil complex_types nil ))nil 3294948253"" (skosimp)"" (assert )"" (rewrite "arg_inv" )"" (split)"1" (rewrite "ln_div" ) nil nil )"2" (lift-if)"2" (lift-if) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"posreal" nil )"posreal" polar nil )"nzcomplex" complex_typesnil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil polar nil )nil ln_exp "lnexp/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"nnreal" polar nil )nil ln_exp "lnexp/" )"posreal" nil )nil polar nil )nil complex_types nil )nil booleans nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" complex_types nil )"real" complex_types nil )nil complex_types nil ))nil 3295030968"" (skosimp)"" (assert )"" (rewrite "ln_div" )"" (rewrite "arg_div" )"" (lift-if) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"even_int" integers nil )"nzint" integers nil )"real" reals nil )"posreal" nil )"posreal" polar nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"nzcomplex" complex_typesnil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil polar nil )nil polar nil )"posreal" nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"nnreal" polar nil )nil real_types nil )nil complex_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 )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_exp "lnexp/" ))nil 3456899317"" (skosimp) (("" (expand "sin" 1 1) (("" (assert ) nil nil )) nil ))nil )"complex" complex_lnexp nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )nil complex_types nil ))nil 3456899337"" (skosimp) (("" (expand "sin" 1 1) (("" (assert ) nil nil )) nil ))nil )"complex" complex_lnexp nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )nil complex_types nil ))nil 3456899346"" (skosimp) (("" (expand "cos" 1 1) (("" (assert ) nil nil )) nil ))nil )"complex" complex_lnexp nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )nil complex_types nil ))nil 3456899357"" (skosimp) (("" (expand "cos" 1 1) (("" (assert ) nil nil )) nil ))nil )"complex" complex_lnexp nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )nil complex_types nil ))nil 3456644280"" (skosimp)"" (expand "sinh" )"" (assert )"" (rewrite "cos_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"real" hyperbolic "lnexp/" )"complex" complex_lnexp nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic "trig/" )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil ))nil 3456644391"" (skosimp)"" (expand "sinh" )"" (assert )"" (rewrite "sin_neg" )"" (expand "cosh" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"complex" complex_lnexp nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic "trig/" )"posreal" nil )"posreal" nil )"posreal_ge1" hyperbolic "lnexp/" )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil ))nil 3456644501"" (skosimp)"" (expand "cosh" )"" (assert )"" (rewrite "cos_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal_ge1" hyperbolic "lnexp/" )"complex" complex_lnexp nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic "trig/" )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"posreal" nil )"posreal" nil ))nil 3456644519"" (skosimp)"" (assert )"" (expand "cosh" )"" (assert )"" (expand "sinh" )"" (rewrite "sin_neg" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic "trig/" )"real" reals nil )"real" hyperbolic "lnexp/" )"complex" complex_lnexp nil ))nil 3472838191"" (skosimp)"" (split)"1" (flatten)"1" (assert )"1" (flatten)"1" (typepred "cosh(Re(z!1))" )"1" (rewrite "zero_times3" -3)"1" (lemma "sin_cos_eq_0" ("a" "Im(z!1)" ))"1" (replace -3)"1" (rewrite "zero_times3" -2)"1" (replace 1)"1" (lemma "sin_eq_0" ("a" "Im(z!1)" ))"1" (assert )"1" (skosimp)"1" "i!1" )"1" assert )"1" rewrite "zero_times1" )"1" "1" expand "sinh" )"1" "ZZ" "Re(z!1)" )"1" rewrite "div_cancel3" -1)"1" "exp_strict_increasing" )"1" expand "strict_increasing?" )"1" "trichotomy" "x" "ZZ" ))"1" "1" "-ZZ" "ZZ" )"1" assert )nil nil ))nil )"2" nil nil )"3" "ZZ" "-ZZ" )"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 )"2" (skosimp*)"2" (assert )"2" (flatten)"2" (rewrite "zero_times1" )"2" (rewrite "one_times" )"2" (replace -1)"2" (replace -2)"2" (hide -1 -2)"2" (rewrite "sinh_0" )"2" (rewrite "cosh_0" )"2" (rewrite "sin_k_pi" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )"real" complex_types nil )nil complex_types nil )"posreal_ge1" hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )"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 trig_aux nil )"real" trig_basic "trig/" )"real" hyperbolic "lnexp/" )nil trig_basic "trig/" )"[T, T -> boolean]" equalities nil )"real" reals nil )nil ln_exp "lnexp/" )nil real_axioms nil )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" reals nil )nil real_props nil )"boolean" notequal nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" ln_exp "lnexp/" )"{py | x = ln(py)}" ln_exp "lnexp/" )"[numfield -> numfield]" number_fields nil )nil real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields 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_basic"trig/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"(total_order?[real])" nil )nil real_props nil )"real" trig_basic "trig/" )"real" complex_types nil )nil hyperbolic "lnexp/" )nil trig_basic "trig/" )nil integers nil )nil hyperbolic "lnexp/" )nil extra_tegies nil ))nil 3472839104"" (skosimp)"" (split)"1" (flatten)"1" (assert )"1" (flatten)"1" (rewrite "zero_times3" -1)"1" (lemma "sin_cos_eq_0" ("a" "Im(z!1)" ))"1" (replace -1)"1" (rewrite "zero_times3" -2)"1" (replace 1)"1" (hide 1)"1" (rewrite "cos_eq_0" )"1" (skosimp)"1" (inst + "i!1" )"1" assert )"1" "1" "ZZ" "Re(z!1)" )"1" expand "sinh" )"1" "exp_strict_increasing" )"1" expand "strict_increasing?" )"1" "trichotomy" "x" "ZZ" ))"1" "1" "-ZZ" "ZZ" )"1" assert )nil nil ))nil )"2" (propax) nil nil )"3" "ZZ" "-ZZ" )"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 )"2" (skosimp*)"2" (assert )"2" (flatten)"2" (replace -1)"2" (replace -2)"2" (hide -1 -2)"2" (rewrite "sinh_0" )"2" (rewrite "cosh_0" )"2" (assert )"2" "cos_eq_0" "a" "1 / 2 * pi + j!1 * pi" ))"2" (replace -1)"2" (inst + "j!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"posreal" nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil hyperbolic "lnexp/" )"posreal_ge1" hyperbolic "lnexp/" )nil complex_types nil )"real" complex_types nil )"real" trig_basic "trig/" )"real" complex_types nil )nil trig_basic "trig/" )"posreal" nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" real_fun_preds "reals/" )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )nil real_axioms nil )nil ln_exp "lnexp/" )"[T, T -> boolean]" equalities nil )"real" hyperbolic "lnexp/" )"real" trig_basic "trig/" )nil trig_aux nil )"rat" rationals nil )"posrat" nil )nil hyperbolic "lnexp/" )"{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 )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil hyperbolic "lnexp/" ))nil 3456899039 ("" (subtype-tcc) nil nil )"bool" complex_lnexp nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"real" reals nil )"bool" complex_types nil )"real" complex_types nil )"real" complex_types nil )"nzcomplex" complex_lnexp nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_lnexp nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil ))nil ))nil 3456899039 ("" (subtype-tcc) nil nil )"bool" complex_lnexp nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"real" reals nil )"bool" complex_types nil )"real" complex_types nil )"real" complex_types nil )"nzcomplex" complex_lnexp nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_lnexp nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil ))nil ))nil 3456901842"" (assert )"" (rewrite "sin_0" )"" (rewrite "sinh_0" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic "trig/" )nil hyperbolic "lnexp/" )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" ))nil 3456901865"" (assert )"" (rewrite "sin_0" )"" (rewrite "cos_0" )"" (rewrite "cosh_0" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil trig_basic "trig/" )nil hyperbolic "lnexp/" )nil trig_basic "trig/" )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" ))nil 3456901832"" (expand "Cosh?" )"" (assert )"" (flatten)"" (hide -2)"" (rewrite "cos_0" )"" (rewrite "cosh_0" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil hyperbolic "lnexp/" )nil trig_basic "trig/" )"bool" complex_lnexp nil ))nil ))nil 3456901957"" (expand "tanh" )"" (assert )"" (lemma "c_sinh_0" )"" (lemma "c_cosh_0" )"" (assert )"" (flatten)"" (replace -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )"complex" complex_lnexp nil ))nil 3456902083"" (expand "sech" )"" (assert )"" (lemma "c_cosh_0" )"" (assert )"" (flatten)"" (assert )"" (replace -1)"" (expand "sq_abs" )"" (assert )"" (replace -1)"" (replace -2)"" (hide-all-but 1) (("" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )"nzcomplex" complex_typesnil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )"nnreal" complex_types nil )"posreal" nil )"nonneg_real" sq "reals/" )"posreal" nil )"posreal" sq "reals/" )"nzreal" nil )"nnreal" nil )nil complex_lnexp nil )"complex" complex_lnexp nil ))nil 3456902156"" (skosimp)"" (assert )"" (lemma "sin2_cos2" ("a" "Im(z!1)" ))"" (lemma "cosh_sinh_one" ("x" "Re(z!1)" ))"" "both_sides_times1" "x" "sq(cosh(Re(z!1))) - sq(sinh(Re(z!1)))" "y" "1" "n0z" "sq(sin(Im(z!1))) + sq(cos(Im(z!1)))" ))"1" (expand "sq" ) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil hyperbolic "lnexp/" )"real" complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"real" hyperbolic "lnexp/" )"posreal_ge1" hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_basic "trig/" )"real" trig_basic "trig/" )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"nnreal" nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic "trig/" ))nil 3456993091"" (skosimp)"" (typepred "cz!1" )"" (expand "Cosh?" )"" (expand "tanh" )"" (expand "sech" )"" (lemma "c_cosh_sinh_one" ("z" "cz!1" ))"" "complex_sq_div" "z" "sinh(cz!1)" "n0z" "cosh(cz!1)" ))"" "complex_sq_div" "z" "complex_(1,0)" "n0z" "cosh(cz!1)" ))"" (case "sq(cosh(cz!1)) /=0" )"1" (name-replace "SC" "sq(cosh(cz!1))" )"1" (name-replace "SS" "sq(sinh(cz!1))" )"1" "DRL1" "sq(sinh(cz!1) / cosh(cz!1))" )"1" "DRL2" "sq(1 / cosh(cz!1))" )"1" "DRL3" "sq(complex_(1, 0) / cosh(cz!1))" )"1" "1" assert )"1" "1" "Re(DRL2)=Re(DRL3)" )"1" "1" "Im(DRL2)=Im(DRL3)" )"1" "1" replace -2)"1" replace -3)"1" replace -4)"1" replace -5)"1" "1" case "sq_abs(SC)>0" )"1" "div_cancel3" "y" "1" "x" "Im(SS) * Im(SC) + Re(SS) * Re(SC)+Re(SC)" "n0z" "sq_abs(SC)" ))"1" replace "1" "1" "div_cancel3" "y" "0" "x" "Im(SS) * Re(SC) - Re(SS) * Im(SC)-Im(SC)" "n0z" "sq_abs(SC)" ))"1" replace "1" "1" expand "sq_abs" )"1" expand "sq" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" expand "sq_abs" )"2" "1" "sq_nz_pos" "nz" "Re(SC)" ))"1" assert )nil nil )"2" nil nil ))nil )"2" "sq_nz_pos" "nz" "Im(SC)" ))"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "DRL2" )"2" expand "DRL3" )"2" "2" expand "sq" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "DRL2" )"2" expand "DRL3" )"2" expand "sq" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (1 -4))"2" (name-replace "X" "cosh(cz!1)" )"2" (assert )"2" (flatten)"2" "zero_times3" "x" "Im(X)" "y" "Re(X)" ))"2" assert )"2" "1" assert )"1" replace -1)"1" "sq_eq_0" ("a" "Re(X)" ))"1" assert )"1" rewrite "sq_rew" )nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" assert )"2" rewrite "sq_rew" )"2" "sq_eq_0" "a" "Im(X)" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" complex_lnexp nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"complex" complex_lnexp nil )nil complex_lnexp nil )"[complex -> boolean]" complex_typesnil )"[[real, real] -> (complex_?)]" nil )nil real_props nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil sq "reals/" )nil sq "reals/" )"[T, T -> boolean]" equalities nil )"complex" complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"nnreal" nil )nil reals nil )nil sq "reals/" )nil real_props nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" complex_types nil )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )"complex" complex_lnexp nil )"nzcomplex" complex_typesnil )"nzcomplex" complex_typesnil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )"complex" complex_lnexp nil )"complex" complex_types nil )"complex" complex_types nil )"bool" complex_types nil )nil complex_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" complex_types nil )"real" complex_types nil )nil complex_types nil )"complex" complex_lnexp nil )"complex" complex_lnexp nil )"complex" complex_lnexp nil ))nil 3472821686"" (skosimp)"" (typepred "sz!1" )"" (expand "Sinh?" )"" (expand "coth" )"" (expand "csch" )"" "complex_sq_div" "z" "cosh(sz!1)" "n0z" "sinh(sz!1)" ))"" "complex_sq_div" "z" "complex_(1,0)" "n0z" "sinh(sz!1)" ))"" (lemma "c_cosh_sinh_one" ("z" "sz!1" ))"" (name-replace "SINH" "sinh(sz!1)" )"" (name-replace "DRL1" "sq(cosh(sz!1) / SINH)" )"" case "sq(complex_(1, 0) / SINH)=sq(1 / SINH)" )"1" "DRL2" "sq(complex_(1, 0) / SINH)" )"1" (name-replace "DRL3" "sq(1 / SINH)" )"1" (name-replace "SS" "sq(SINH)" )"1" "SC" "sq(cosh(sz!1))" )"1" assert )"1" "1" assert )"1" replace -1)"1" replace -2)"1" replace -5)"1" replace -7)"1" "Im(SC)=Im(SS)" )"1" "Re(SC)=1+Re(SS)" )"1" assert )"1" "div_simp" "n0x" "sq_abs(SS)" ))"1" expand "sq_abs" "1" expand "sq" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -2 -3 -1)"2" (expand "sq" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" complex_lnexp nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"complex" complex_lnexp nil )"complex" complex_lnexp nil )"complex" complex_lnexp nil )nil complex_types nil )"real" complex_types nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil complex_types nil )nil complex_lnexp nil )"complex" complex_types nil )"complex" complex_types nil )nil complex_types nil )nil complex_types nil )"nzcomplex" complex_typesnil )"nzcomplex" complex_typesnil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )nil reals nil )"bool" reals nil )nil real_types nil )"nnreal" complex_types nil )"nonneg_real" sq "reals/" )"complex" complex_types nil )"bool" complex_types nil )"[T, T -> boolean]" equalities nil )"[[real, real] -> (complex_?)]" nil )"[complex -> boolean]" complex_typesnil )"complex" complex_lnexp nil ))nil 3456902338"" (skosimp)"" (assert )"" (assert )"" (lemma "cosh_plus_sinh" ("x" "Re(z!1)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil hyperbolic "lnexp/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil complex_types nil )"real" complex_types nil ))nil 3456902390"" (skosimp)"" (assert )"" (lemma "cosh_minus_sinh" ("x" "Re(z!1)" ))"" (assert )"" (rewrite "cos_neg" )"" (rewrite "sin_neg" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil trig_basic "trig/" )nil trig_basic "trig/" )"real" complex_types nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic "lnexp/" ))nil 3456902501"" (skosimp)"" (assert )"" (rewrite "sin_neg" )"" (rewrite "cos_neg" )"" (rewrite "cosh_neg" )"" (rewrite "sinh_neg" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil trig_basic "trig/" )nil hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )"real" complex_types nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic "trig/" ))nil 3456902540"" (skosimp)"" (assert )"" (rewrite "sinh_neg" )"" (rewrite "cosh_neg" )"" (rewrite "cos_neg" )"" (rewrite "sin_neg" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil hyperbolic "lnexp/" )nil trig_basic "trig/" )nil trig_basic "trig/" )"real" complex_types nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic "lnexp/" ))nil 3456901832 ("" (subtype-tcc) nil nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"real" complex_types nil )"real" complex_types nil )"complex" complex_types nil )"nzcomplex" complex_lnexp nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_lnexp nil )"bool" complex_types nil )"bool" complex_lnexp nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil ))nil ))nil 3472834131"" (skosimp)"" (expand "tanh" )"" (lemma "c_sinh_neg" ("z" "cz!1" ))"" (lemma "c_cosh_neg" ("z" "cz!1" ))"" (typepred "cz!1" )"" (expand "Cosh?" )"" (name-replace "CNZ" "cosh(-cz!1)" )"" (name-replace "SNZ" "sinh(-cz!1)" )"" (name-replace "CZ" "cosh(cz!1)" )"" (name-replace "SZ" "sinh(cz!1)" )"" (assert )"" (flatten)"" (expand "sq_abs" )"" (replace -2)"" replace -3)"" replace -4)"" replace -5)"" "" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_lnexp nil )nil complex_lnexp nil )"complex" complex_lnexp nil )"nnreal" complex_types nil )"nnreal" nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"complex" complex_lnexp nil )"complex" complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil complex_lnexp nil )nil complex_types nil )nil booleans nil )nil booleans nil )"bool" complex_lnexp nil ))nil 3456901832 ("" (subtype-tcc) nil nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"real" complex_types nil )"real" complex_types nil )"complex" complex_types nil )"nzcomplex" complex_lnexp nil )"complex" complex_types nil )"complex" complex_types nil )"complex" complex_lnexp nil )"bool" complex_types nil )"bool" complex_lnexp nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil ))nil ))nil 3472834811"" (skosimp)"" (typepred "sz!1" )"" (expand "Sinh?" )"" (expand "csch" )"" (lemma "c_sinh_neg" ("z" "sz!1" ))"" (name-replace "SNZ" "sinh(-sz!1)" )"" (name-replace "SZ" "sinh(sz!1)" )"" (assert )"" (flatten)"" (expand "sq_abs" )"" (replace -1)"" (replace -2)"" (hide -1 -2)"" (rewrite "sq_neg" )"" rewrite "sq_neg" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" complex_lnexp nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"complex" complex_lnexp nil )"[T, T -> boolean]" equalities nil )"complex" complex_lnexp nil )"complex" complex_types nil )"real" reals nil )"real" reals nil )"nzcomplex" complex_types nil )"nzcomplex" complex_typesnil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"nnreal" nil )"nnreal" complex_types nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil sq "reals/" )"real" complex_types nil )nil complex_lnexp nil ))nil 3472834931"" (skosimp)"" (typepred "cz!1" )"" (expand "Cosh?" )"" (expand "sech" )"" (lemma "c_cosh_neg" ("z" "cz!1" ))"" (name-replace "CNZ" "cosh(-cz!1)" )"" (name-replace "CZ" "cosh(cz!1)" )"" (assert )"" (flatten)"" (expand "sq_abs" )"" (replace -1)"" (replace -2) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" complex_lnexp nil )nil complex_types nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"complex" complex_lnexp nil )"[T, T -> boolean]" equalities nil )"complex" complex_lnexp nil )"complex" complex_types nil )"real" reals nil )"real" reals nil )"nzcomplex" complex_typesnil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"nnreal" nil )"nnreal" complex_types nil )nil complex_lnexp nil ))nil 3472834455"" (skosimp)"" (expand "coth" )"" (typepred "sz!1" )"" (expand "Sinh?" )"" (lemma "c_sinh_neg" ("z" "sz!1" ))"" (lemma "c_cosh_neg" ("z" "sz!1" ))"" (name-replace "SZ" "sinh(sz!1)" )"" (name-replace "SNZ" "sinh(-sz!1)" )"" (name-replace "CZ" "cosh(sz!1)" )"" (name-replace "CNZ" "cosh(-sz!1)" )"" (assert )"" (flatten)"" (expand "sq_abs" )"" (replace -1)"" replace -2)"" replace -3)"" replace -4)"" rewrite "sq_neg" )"" rewrite "sq_neg" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_lnexp nil )nil complex_lnexp nil )"complex" complex_types nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil sq "reals/" )"real" complex_types nil )"nnreal" complex_types nil )"nnreal" nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"complex" complex_lnexp nil )"[T, T -> boolean]" equalities nil )"complex" complex_lnexp nil )nil complex_lnexp nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil complex_types nil )"bool" complex_lnexp nil ))nil 3456902582"" (skosimp)"" (assert )"" (assert )"" (rewrite "sinh_sum" )"" (assert )"" (rewrite "cosh_sum" )"" (rewrite "cos_plus" )"" (rewrite "sin_plus" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )"real" complex_types nil )nil complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )nil trig_basic "trig/" )nil trig_basic "trig/" )"real" complex_types nil ))nil 3456989995"" (skosimp)"" (lemma "c_sinh_sum" ("x" "x!1" "y" "-y!1" ))"" (assert )"" (flatten)"" (rewrite "sin_neg" )"" (rewrite "cos_neg" )"" (rewrite "cosh_neg" )"" (rewrite "sinh_neg" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil trig_basic "trig/" )nil hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )"real" complex_types nil )nil trig_basic "trig/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" ))nil 3456990162"" (skosimp)"" (assert )"" (rewrite "cosh_sum" )"" (rewrite "cos_plus" )"" (rewrite "sinh_sum" )"" (rewrite "sin_plus" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )"real" complex_types nil )nil trig_basic "trig/" )nil trig_basic "trig/" )nil hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil complex_types nil )"real" complex_types nil ))nil 3456990226"" (skosimp)"" (lemma "c_cosh_sum" ("x" "x!1" "y" "-y!1" ))"" (assert )"" (rewrite "cosh_neg" )"" (rewrite "cos_neg" )"" (rewrite "sin_neg" )"" (rewrite "sinh_neg" )"" (assert )"" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complex" complex_types nil )nil complex_types nil )nil complex_lnexp nil )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic "lnexp/" )nil trig_basic "trig/" )nil hyperbolic "lnexp/" )nil trig_basic "trig/" )"real" complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" ))nil 3456991337"" (skosimp)"" (assert )"" (rewrite "cos_2a" )"" (rewrite "sin_2a" )"" (rewrite "sinh2x" )"" (rewrite "cosh2x" )"" (split)"1" (assert ) nil nil )"2" "2*sq(cosh(Re(x!1))) - 1=sq(cosh(Re(x!1)))+sq(sinh(Re(x!1)))" )"1" (expand "sq" ) (("1" (propax) nil nil )) nil )"2" (hide 2)"2" (lemma "cosh_sinh_one" ("x" "Re(x!1)" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil trig_basic "trig/" )nil hyperbolic "lnexp/" )"nnreal" nil )"real" hyperbolic "lnexp/" )"[numfield, numfield -> numfield]" number_fields nil )"posreal_ge1" hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"nnreal" nil )nil hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )"real" complex_types nil )nil trig_basic "trig/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil complex_types nil )"real" complex_types nil ))nil 3456991747"" (skosimp)"" (assert )"" (rewrite "cosh2x" )"" (rewrite "sinh2x" )"" (rewrite "cos_2a" )"" (rewrite "sin_2a" )"" (assert )"" (expand "sq" )"" (rewrite "sq_rew" )"" (rewrite "sq_rew" )"" (rewrite "sq_rew" )"" (lemma "sin2_cos2" ("a" "Im(x!1)" ))"" (expand "sq" )"" (assert )"" "cos(Im(x!1)) * cos(Im(x!1))=1-sin(Im(x!1)) * sin(Im(x!1))" )"1" "1" assert )"1" "cosh_sinh_one" "x" "Re(x!1)" ))"1" expand "sq" )"1" (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 )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil hyperbolic "lnexp/" )nil trig_basic "trig/" )"nonneg_real" sq "reals/" )"posreal_ge1" hyperbolic "lnexp/" )nil hyperbolic "lnexp/" )"bool" reals nil )nil booleans nil )nil trig_basic "trig/" )nil hyperbolic "lnexp/" )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_basic "trig/" )"even_int" integers nil )"nzint" integers nil )"odd_int" integers nil )nil sq "reals/" )"real" trig_basic "trig/" )nil trig_basic "trig/" )"real" complex_types nil )"nnreal" nil )nil hyperbolic "lnexp/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil complex_types nil )"real" complex_types nil ))nil 3456992244"" (skosimp)"" (lemma "c_cosh2x" ("x" "x!1" ))"" (lemma "c_cosh_sinh_one" ("z" "x!1" ))"" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil complex_types nil )nil complex_lnexp nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil ))nil 3456992191"" (skosimp)"" (lemma "c_cosh2x" ("x" "x!1" ))"" (lemma "c_cosh_sinh_one" ("z" "x!1" ))"" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil complex_types nil )nil complex_lnexp nil )"real" reals nil )"trig_range" trig_basic "trig/" )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil ))nil 3456992272"" (skosimp)"" (assert )"" (rewrite "sinh4x" )"" (rewrite "cosh4x" )"" (rewrite "expt_x4" )"" (rewrite "expt_x4" )"" (assert )"" (lemma "cos_2a" ("a" "Im(x!1)" ))"" (lemma "cos_2a" ("a" "2*Im(x!1)" ))"" (replace -1)"" (replace -2)"" (lemma "sin_2a" ("a" "Im(x!1)" ))"" (lemma "sin_2a" ("a" "2*Im(x!1)" ))"" (replace -1)"" replace -2)"" assert )"" replace -4)"" "1" assert )"1" assert )"1" expand "sq" )"1" (propax) nil nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "sq" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil hyperbolic "lnexp/" )"nnreal" nil )"real" hyperbolic "lnexp/" )nil trig_basic "trig/" )"real" complex_types nil )nil trig_basic "trig/" )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil exponentiation nil )nil booleans nil )"bool" reals nil )nil hyperbolic "lnexp/" )"posreal_ge1" hyperbolic "lnexp/" )"nnreal" nil )nil hyperbolic "lnexp/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil complex_types nil )"real" complex_types nil ))nil 3456899653"" (skosimp)"" (assert )"" (lemma "cosh_neg" ("x" "Im(z!1)" ))"" (lemma "sinh_neg" ("x" "Im(z!1)" ))"" (assert )"" (rewrite "zero_times1" )"" (assert )"" (lemma "sin_neg" ("a" "Re(z!1)" ))"" (lemma "cos_neg" ("a" "Re(z!1)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzcomplex" complex_types nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil ))nil 3456899846"" (skosimp)"" (assert )"" (assert )"" (rewrite "Im_cos" )"" (rewrite "Im_cosh" )"" (lemma "cosh_neg" ("x" "Im(z!1)" ))"" (lemma "sinh_neg" ("x" "Im(z!1)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic "trig/" )"real" reals nil )"real" reals nil )"trig_range" trig_basic "trig/" )"real" reals nil )nil complex_types nil )nil complex_lnexp nil )nil complex_lnexp nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_types nil )nil complex_lnexp nil )nil complex_types nil )nil complex_lnexp nil )"real" reals nil )nil hyperbolic "lnexp/" )"real" complex_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil hyperbolic "lnexp/" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.90 Sekunden
(vorverarbeitet am 2026-05-01)
¤ *© Formatika GbR, Deutschland
2026-05-26
