|
(complex_lnexp
(exp_TCC1 0
(exp_TCC1-1 nil 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)
((sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(Re_rew formula-decl nil complex_types nil)
(Im_rew formula-decl nil complex_types nil)
(sin const-decl "real" trig_basic "trig/")
(sin_cos_eq_0 formula-decl nil trig_aux nil)
(Im const-decl "real" complex_types nil)
(cos const-decl "real" trig_basic "trig/")
(Re const-decl "real" complex_types nil)
(complex type-decl nil complex_types nil)
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp/")
(ln const-decl "real" ln_exp "lnexp/")
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(zero_times3 formula-decl nil real_props nil))
shostak))
(Re_exp 0
(Re_exp-1 nil 3456000255 ("" (grind) nil nil)
((Re const-decl "real" complex_types nil)
(Im const-decl "real" complex_types nil)
(exp const-decl "nzcomplex" complex_lnexp nil)
(cos_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(Im_exp 0
(Im_exp-1 nil 3456000259 ("" (grind) nil nil)
((Re const-decl "real" complex_types nil)
(Im const-decl "real" complex_types nil)
(exp const-decl "nzcomplex" complex_lnexp nil)
(sin_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(exp_i_pi 0
(exp_i_pi-1 nil 3294274991
("" (assert)
(("" (rewrite "cos_pi") (("" (rewrite "sin_pi") nil nil)) nil))
nil)
((cos_pi formula-decl nil trig_basic "trig/")
(sin_pi formula-decl nil trig_basic "trig/")
(Re_i formula-decl nil complex_types nil)
(Re_mul3 formula-decl nil complex_types nil)
(exp_0 formula-decl nil ln_exp "lnexp/")
(Im_i formula-decl nil complex_types nil)
(Im_mul3 formula-decl nil complex_types nil)
(Re_exp formula-decl nil complex_lnexp nil)
(Im_exp formula-decl nil complex_lnexp nil)
(c_eq3 formula-decl nil complex_types nil)
(mul_nzcomplex3 application-judgement "nzcomplex" complex_types
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(exp_plus 0
(exp_plus-1 nil 3294335316
("" (skosimp)
(("" (assert)
(("" (rewrite "exp_sum")
(("" (rewrite "cos_plus")
(("" (rewrite "sin_plus") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(mul_nzcomplex1 application-judgement "nzcomplex" complex_types
nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_mul1 formula-decl nil complex_types nil)
(Re_mul1 formula-decl nil complex_types nil)
(Im_exp formula-decl nil complex_lnexp nil)
(Re_exp formula-decl nil complex_lnexp nil)
(Im_add1 formula-decl nil complex_types nil)
(Re_add1 formula-decl nil complex_types nil)
(Im const-decl "real" complex_types nil)
(cos_plus formula-decl nil trig_basic "trig/")
(sin_plus formula-decl nil trig_basic "trig/")
(exp_sum formula-decl nil ln_exp "lnexp/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(complex type-decl nil complex_types nil)
(Re const-decl "real" complex_types nil))
shostak))
(exp_negate 0
(exp_negate-1 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")
((""
(lemma "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)
((""
(lemma "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)
((""
(hide -1)
((""
(expand "sq_abs")
((""
(assert)
((""
(rewrite "sq_times")
((""
(rewrite "sq_times")
((""
(lemma
"sin2_cos2"
("a" "Im(x!1)"))
((""
(lemma
"sq_nz_pos"
("nz" "exp(Re(x!1))"))
((""
(lemma
"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)
((sin_range application-judgement "trig_range" trig_basic "trig/")
(nz_sq_abs_pos application-judgement "posreal" complex_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(div_nzcomplex2 application-judgement "nzcomplex" complex_types
nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_div2 formula-decl nil complex_types nil)
(Im_exp formula-decl nil complex_lnexp nil)
(Re_div2 formula-decl nil complex_types nil)
(Re_exp formula-decl nil complex_lnexp nil)
(Im_neg1 formula-decl nil complex_types nil)
(Re_neg1 formula-decl nil complex_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(Im const-decl "real" complex_types nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(exp const-decl "nzcomplex" complex_lnexp nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(cos const-decl "real" trig_basic "trig/")
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp/")
(ln const-decl "real" ln_exp "lnexp/")
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sq_abs const-decl "nnreal" complex_types nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_cancel4 formula-decl nil real_props nil)
(cos_neg formula-decl nil trig_basic "trig/")
(div_cancel3 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq_times formula-decl nil sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin2_cos2 formula-decl nil trig_basic "trig/")
(both_sides_times1 formula-decl nil real_props nil)
(sq const-decl "nonneg_real" sq "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(sq_nz_pos judgement-tcc nil sq "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_neg formula-decl nil trig_basic "trig/")
(sin const-decl "real" trig_basic "trig/")
(nz_sq_abs_pos judgement-tcc nil complex_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(exp_neg formula-decl nil ln_exp "lnexp/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(complex type-decl nil complex_types nil)
(Re const-decl "real" complex_types nil))
shostak))
(exp_minus 0
(exp_minus-1 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"
(lemma "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"
(hide -1)
(("1"
(cross-mult)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (cross-mult)
(("2"
(lemma "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"
(hide -1)
(("2"
(cross-mult)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((complex type-decl nil complex_types nil)
(exp_negate formula-decl nil complex_lnexp nil)
(div_nzcomplex1 application-judgement "nzcomplex" complex_types
nil)
(nz_sq_abs_pos application-judgement "posreal" complex_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_nzcomplex2 application-judgement "nzcomplex" complex_types
nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(mul_nzcomplex1 application-judgement "nzcomplex" complex_types
nil)
(Re_neg1 formula-decl nil complex_types nil)
(Re_add1 formula-decl nil complex_types nil)
(Im_neg1 formula-decl nil complex_types nil)
(Im_add1 formula-decl nil complex_types nil)
(Re_exp formula-decl nil complex_lnexp nil)
(Im_exp formula-decl nil complex_lnexp nil)
(Re_mul1 formula-decl nil complex_types nil)
(Im_mul1 formula-decl nil complex_types nil)
(c_eq1 formula-decl nil complex_types nil)
(Re_div2 formula-decl nil complex_types nil)
(Im_div2 formula-decl nil complex_types nil)
(Re_sub1 formula-decl nil complex_types nil)
(Im_sub1 formula-decl nil complex_types nil)
(Re_div1 formula-decl nil complex_types nil)
(Im_div1 formula-decl nil complex_types nil)
(Im const-decl "real" complex_types nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(cos_neg formula-decl nil trig_basic "trig/")
(Re const-decl "real" complex_types nil)
(exp_neg formula-decl nil ln_exp "lnexp/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(div_distributes_minus formula-decl nil real_props nil)
(div_cancel3 formula-decl nil real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(exp const-decl "nzcomplex" complex_lnexp nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sq_abs const-decl "nnreal" complex_types nil)
(nnreal type-eq-decl nil real_types nil)
(div_cancel4 formula-decl nil real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(sin const-decl "real" trig_basic "trig/")
(times_div2 formula-decl nil real_props nil)
(cos const-decl "real" trig_basic "trig/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp/")
(ln const-decl "real" ln_exp "lnexp/")
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(times_div1 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(div_distributes formula-decl nil real_props nil)
(sin_neg formula-decl nil trig_basic "trig/")
(exp_plus formula-decl nil complex_lnexp nil)
(- const-decl "complex" complex_types nil))
shostak))
(exp_periodicity 0
(exp_periodicity-1 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)
((""
(lemma "sin_period"
("a" "Im(x!1)" "j" "j!1"))
(("" (replace -1 1 rl)
((""
(lemma "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_times_real_is_real application-judgement "real" reals nil)
(exp const-decl "nzcomplex" complex_lnexp nil)
(int nonempty-type-eq-decl nil integers nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(Im const-decl "real" complex_types nil)
(complex type-decl nil complex_types nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_period formula-decl nil trig_basic "trig/")
(cos_period formula-decl nil trig_basic "trig/")
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(Re_i formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_add1 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_add1 formula-decl nil complex_types nil)
(Re_rew formula-decl nil complex_types nil)
(Im_rew formula-decl nil complex_types nil)
(c_eq1 formula-decl nil complex_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/"))
shostak))
(abs_exp 0
(abs_exp-1 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)
((abs_nzcomplex application-judgement "posreal" polar nil)
(sq_abs const-decl "nnreal" complex_types nil)
(sq_eq formula-decl nil sq "reals/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sq const-decl "nonneg_real" sq "reals/")
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(ln const-decl "real" ln_exp "lnexp/")
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp/")
(complex type-decl nil complex_types nil)
(Re const-decl "real" complex_types nil)
(cos const-decl "real" trig_basic "trig/")
(Im const-decl "real" complex_types nil)
(sin const-decl "real" trig_basic "trig/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sin2_cos2 formula-decl nil trig_basic "trig/")
(sq_times formula-decl nil sq "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sq_sqrt formula-decl nil sqrt "reals/")
(Re_exp formula-decl nil complex_lnexp nil)
(Im_exp formula-decl nil complex_lnexp nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(abs const-decl "nnreal" polar nil))
shostak))
(arg_exp 0
(arg_exp-1 nil 3456123074
("" (skosimp)
(("" (assert)
(("" (expand "exp")
(("" (expand "arg")
(("" (assert)
(("" (rewrite "zero_times3")
(("" (rewrite "zero_times3")
((""
(case-replace
"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"
(lemma "both_sides_times_pos_lt1"
("pz" "exp(Re(z!1))" "x" "sin(Im(z!1))" "y"
"0"))
(("2" (replace -1)
(("2" (hide -1)
(("2"
(lemma "atan2_cancel_pos"
("x"
"cos(Im(z!1))"
"y"
"sin(Im(z!1))"
"pz"
"exp(Re(z!1))"))
(("2"
(split)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(case "0<=Im(z!1)")
(("1"
(lemma
"sin_ge_0"
("a" "Im(z!1)"))
(("1"
(assert)
(("1"
(hide -3)
(("1"
(rewrite "atan2_cos_sin")
nil
nil))
nil))
nil))
nil)
("2"
(case "Im(z!1)<0")
(("1"
(hide 1)
(("1"
(lemma
"sin_period"
("a" "Im(z!1)" "j" "1"))
(("1"
(lemma
"cos_period"
("a" "Im(z!1)" "j" "1"))
(("1"
(replace -1)
(("1"
(replace -2)
(("1"
(hide -1 -2)
(("1"
(lemma
"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"
(flatten)
(("2"
(lemma
"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)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(sin_range application-judgement "trig_range" trig_basic "trig/")
(arg const-decl "argrng" polar nil)
(zero_times3 formula-decl nil real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(ln const-decl "real" ln_exp "lnexp/")
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp/")
(complex type-decl nil complex_types nil)
(Re const-decl "real" complex_types nil)
(cos const-decl "real" trig_basic "trig/")
(Im const-decl "real" complex_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(sin_cos_eq_0 formula-decl nil trig_aux nil)
(atan2_cancel_pos formula-decl nil atan2 "trig/")
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(<= const-decl "bool" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi_lb const-decl "posreal" trig_basic "trig/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(atan2_cos_sin formula-decl nil atan2 "trig/")
(sin_ge_0 formula-decl nil trig_ineq "trig/")
(cos_period formula-decl nil trig_basic "trig/")
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_lt_0 formula-decl nil trig_ineq "trig/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(sin_period formula-decl nil trig_basic "trig/")
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(sin const-decl "real" trig_basic "trig/")
(c_eq3 formula-decl nil complex_types nil)
(Im_rew formula-decl nil complex_types nil)
(Re_rew formula-decl nil complex_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(exp const-decl "nzcomplex" complex_lnexp nil))
shostak))
(Re_ln 0
(Re_ln-1 nil 3456000946
("" (skosimp) (("" (expand "ln" 1 1) (("" (assert) nil nil)) nil))
nil)
((ln const-decl "complex" complex_lnexp nil)
(abs_nzcomplex application-judgement "posreal" polar nil)
(Re_rew formula-decl nil complex_types nil))
shostak))
(Im_ln 0
(Im_ln-1 nil 3456000994
("" (skosimp) (("" (expand "ln" 1 1) (("" (assert) nil nil)) nil))
nil)
((ln const-decl "complex" complex_lnexp nil)
(abs_nzcomplex application-judgement "posreal" polar nil)
(Im_rew formula-decl nil complex_types nil))
shostak))
(ln_exp 0
(ln_exp-1 nil 3294847345
(""
(case "FORALL (z: complex):
-pi < Im(z) AND Im(z) <= pi =>
ln(exp(z))=z")
(("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"
(case-replace
"exp(Re(z!1)) * cos(Im(z!1)) = 0 AND
exp(Re(z!1)) * sin(Im(z!1)) = 0")
(("1" (assert) nil nil)
("2" (replace 1)
(("2"
(case-replace
"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)
((arg_exp formula-decl nil complex_lnexp nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs_nzcomplex application-judgement "posreal" polar nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(real_plus_real_is_real application-judgement "real" reals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(Re_i formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_add1 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_add1 formula-decl nil complex_types nil)
(Re_exp formula-decl nil complex_lnexp nil)
(Im_exp formula-decl nil complex_lnexp nil)
(c_eq1 formula-decl nil complex_types nil)
(abs_exp formula-decl nil complex_lnexp nil)
(Re_ln formula-decl nil complex_lnexp nil)
(Im_ln formula-decl nil complex_lnexp nil)
(Re_sub1 formula-decl nil complex_types nil)
(Im_sub1 formula-decl nil complex_types nil)
(arg const-decl "argrng" polar nil)
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(ln const-decl "real" ln_exp "lnexp/")
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp/")
(cos const-decl "real" trig_basic "trig/")
(sin const-decl "real" trig_basic "trig/")
(c_eq3 formula-decl nil complex_types nil)
(exp_periodicity formula-decl nil complex_lnexp nil)
(minus_int_is_int application-judgement "int" integers nil)
(complex_i const-decl "nzcomplex" complex_types nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "complex" complex_types nil)
(+ const-decl "complex" complex_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(complex type-decl nil complex_types nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(pi_lb const-decl "posreal" trig_basic "trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(Im const-decl "real" complex_types nil)
(<= const-decl "bool" reals nil)
(= const-decl "bool" complex_types nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(Re const-decl "real" complex_types nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(ln const-decl "complex" complex_lnexp nil)
(exp const-decl "nzcomplex" complex_lnexp nil))
shostak))
(exp_ln 0
(exp_ln-1 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)
((sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(abs_nzcomplex application-judgement "posreal" polar nil)
(real_times_real_is_real application-judgement "real" reals nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_exp formula-decl nil complex_lnexp nil)
(Re_exp formula-decl nil complex_lnexp nil)
(Im_ln formula-decl nil complex_lnexp nil)
(Re_ln formula-decl nil complex_lnexp nil)
(div_nzcomplex3 application-judgement "nzcomplex" complex_types
nil)
(Re_cos_abs1 formula-decl nil polar nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/ const-decl "complex" complex_types nil)
(arg_div_abs formula-decl nil polar nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_simp formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(Re_div3 formula-decl nil complex_types nil)
(Im_div3 formula-decl nil complex_types nil)
(abs_abs formula-decl nil polar nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_div2 formula-decl nil polar nil)
(Im_sin_abs1 formula-decl nil polar nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(Im const-decl "real" complex_types nil)
(Re const-decl "real" complex_types nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(abs const-decl "nnreal" polar nil)
(nnreal type-eq-decl nil real_types nil)
(complex type-decl nil complex_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(exp_ln formula-decl nil ln_exp "lnexp/"))
shostak))
(ln_mult 0
(ln_mult-1 nil 3294856600
("" (skosimp)
(("" (assert)
(("" (rewrite "ln_mult")
(("" (rewrite "arg_mult")
(("" (lift-if) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(abs_nzcomplex application-judgement "posreal" polar nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(mul_nzcomplex1 application-judgement "nzcomplex" complex_types
nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_sub1 formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_add1 formula-decl nil complex_types nil)
(Im_ln formula-decl nil complex_lnexp nil)
(Re_sub1 formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_i formula-decl nil complex_types nil)
(Re_add1 formula-decl nil complex_types nil)
(Re_ln formula-decl nil complex_lnexp nil)
(abs_mult formula-decl nil polar nil)
(arg_mult formula-decl nil polar nil)
(ln_mult formula-decl nil ln_exp "lnexp/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(complex type-decl nil complex_types nil)
(nnreal type-eq-decl nil real_types nil)
(abs const-decl "nnreal" polar nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(Re const-decl "real" complex_types nil)
(Im const-decl "real" complex_types nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil))
shostak))
(ln_inv 0
(ln_inv-1 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_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(abs_nzcomplex application-judgement "posreal" polar nil)
(div_nzcomplex2 application-judgement "nzcomplex" complex_types
nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_sub1 formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_ln formula-decl nil complex_lnexp nil)
(Re_sub1 formula-decl nil complex_types nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_i formula-decl nil complex_types nil)
(Re_ln formula-decl nil complex_lnexp nil)
(abs_inv formula-decl nil polar nil)
(ln_div formula-decl nil ln_exp "lnexp/")
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(abs const-decl "nnreal" polar nil)
(ln_1 formula-decl nil ln_exp "lnexp/")
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(arg_inv formula-decl nil polar nil)
(complex type-decl nil complex_types nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(/= const-decl "boolean" notequal nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(Re const-decl "real" complex_types nil)
(Im const-decl "real" complex_types nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil))
shostak))
(ln_div 0
(ln_div-1 nil 3295030968
("" (skosimp)
(("" (assert)
(("" (rewrite "ln_div")
(("" (rewrite "arg_div")
(("" (lift-if) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(abs_nzcomplex application-judgement "posreal" polar nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(div_nzcomplex1 application-judgement "nzcomplex" complex_types
nil)
(c_eq1 formula-decl nil complex_types nil)
(Im_mul2 formula-decl nil complex_types nil)
(Im_i formula-decl nil complex_types nil)
(Im_sub1 formula-decl nil complex_types nil)
(Im_ln formula-decl nil complex_lnexp nil)
(Re_mul2 formula-decl nil complex_types nil)
(Re_i formula-decl nil complex_types nil)
(Re_sub1 formula-decl nil complex_types nil)
(Re_ln formula-decl nil complex_lnexp nil)
(abs_div formula-decl nil polar nil)
(arg_div formula-decl nil polar nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(Im const-decl "real" complex_types nil)
(Re const-decl "real" complex_types nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(abs const-decl "nnreal" polar nil)
(nnreal type-eq-decl nil real_types nil)
(complex type-decl nil complex_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(ln_div formula-decl nil ln_exp "lnexp/"))
shostak))
(Re_sin 0
(Re_sin-1 nil 3456899317
("" (skosimp) (("" (expand "sin" 1 1) (("" (assert) nil nil)) nil))
nil)
((sin const-decl "complex" complex_lnexp nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(Re_rew formula-decl nil complex_types nil))
shostak))
(Im_sin 0
(Im_sin-1 nil 3456899337
("" (skosimp) (("" (expand "sin" 1 1) (("" (assert) nil nil)) nil))
nil)
((sin const-decl "complex" complex_lnexp nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(Im_rew formula-decl nil complex_types nil))
shostak))
(Re_cos 0
(Re_cos-1 nil 3456899346
("" (skosimp) (("" (expand "cos" 1 1) (("" (assert) nil nil)) nil))
nil)
((cos const-decl "complex" complex_lnexp nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(Re_rew formula-decl nil complex_types nil))
shostak))
(Im_cos 0
(Im_cos-1 nil 3456899357
("" (skosimp) (("" (expand "cos" 1 1) (("" (assert) nil nil)) nil))
nil)
((cos const-decl "complex" complex_lnexp nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(Im_rew formula-decl nil complex_types nil))
shostak))
(Re_sinh 0
(Re_sinh-1 nil 3456644280
("" (skosimp)
(("" (expand "sinh")
(("" (assert)
(("" (rewrite "cos_neg") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((sinh const-decl "real" hyperbolic "lnexp/")
(sinh const-decl "complex" complex_lnexp nil)
(Im const-decl "real" complex_types nil)
(complex type-decl nil complex_types nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(cos_neg formula-decl nil trig_basic "trig/")
(Re_div3 formula-decl nil complex_types nil)
(Re_sub1 formula-decl nil complex_types nil)
(Im_neg1 formula-decl nil complex_types nil)
(Re_neg1 formula-decl nil complex_types nil)
(Re_exp formula-decl nil complex_lnexp nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(Im_sinh 0
(Im_sinh-1 nil 3456644391
("" (skosimp)
(("" (expand "sinh")
(("" (assert)
(("" (rewrite "sin_neg")
(("" (expand "cosh") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((sinh const-decl "complex" complex_lnexp nil)
(Im const-decl "real" complex_types nil)
(complex type-decl nil complex_types nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_neg formula-decl nil trig_basic "trig/")
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cosh const-decl "posreal_ge1" hyperbolic "lnexp/")
(Im_div3 formula-decl nil complex_types nil)
(Im_sub1 formula-decl nil complex_types nil)
(Im_neg1 formula-decl nil complex_types nil)
(Re_neg1 formula-decl nil complex_types nil)
(Im_exp formula-decl nil complex_lnexp nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(Re_cosh 0
(Re_cosh-1 nil 3456644501
("" (skosimp)
(("" (expand "cosh")
(("" (assert)
(("" (rewrite "cos_neg") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((cosh const-decl "posreal_ge1" hyperbolic "lnexp/")
(cosh const-decl "complex" complex_lnexp nil)
(Im const-decl "real" complex_types nil)
(complex type-decl nil complex_types nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(cos_neg formula-decl nil trig_basic "trig/")
(Re_div3 formula-decl nil complex_types nil)
(Re_add1 formula-decl nil complex_types nil)
(Im_neg1 formula-decl nil complex_types nil)
(Re_neg1 formula-decl nil complex_types nil)
(Re_exp formula-decl nil complex_lnexp nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" trig_basic "trig/")
(minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil))
shostak))
(Im_cosh 0
(Im_cosh-1 nil 3456644519
("" (skosimp)
(("" (assert)
(("" (expand "cosh")
(("" (assert)
(("" (expand "sinh")
(("" (rewrite "sin_neg") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((sin_range application-judgement "trig_range" trig_basic "trig/")
(real_times_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(Im_exp formula-decl nil complex_lnexp nil)
(Re_neg1 formula-decl nil complex_types nil)
(Im_neg1 formula-decl nil complex_types nil)
(Im_add1 formula-decl nil complex_types nil)
(Im_div3 formula-decl nil complex_types nil)
(Im const-decl "real" complex_types nil)
(complex type-decl nil complex_types nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_neg formula-decl nil trig_basic "trig/")
(real_minus_real_is_real application-judgement "real" reals nil)
(sinh const-decl "real" hyperbolic "lnexp/")
(cosh const-decl "complex" complex_lnexp nil))
shostak))
(sinh_eq_0 0
(sinh_eq_0-1 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"
(inst + "i!1")
(("1"
(assert)
(("1"
(rewrite "zero_times1")
(("1"
(hide-all-but (-3 2))
(("1"
(expand "sinh")
(("1"
(name-replace "ZZ" "Re(z!1)")
(("1"
(rewrite "div_cancel3" -1)
(("1"
(lemma
"exp_strict_increasing")
(("1"
(expand
"strict_increasing?")
(("1"
(lemma
"trichotomy"
("x" "ZZ"))
(("1"
(split)
(("1"
(inst
-
"-ZZ"
"ZZ")
(("1"
(assert)
nil
nil))
nil)
("2"
(propax)
nil
nil)
("3"
(inst
-
"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)
((sin_range application-judgement "trig_range" trig_basic "trig/")
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.114Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
