| products/Sources/formale Sprachen/PVS/complex/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: core_dune.dbg Sprache: LispOriginal von: PVS© |
|
||||||
|
(exp (exp_TCC1 0
(exp_TCC1-1 nil 3294275262 ("" (skosimp) (("" (typepred "exp(Re(z!1))") (("" (lemma "both_sides_times1" ("n0z" "exp(Re(z!1))" "x" "cos(Im(z!1)) + i * sin(Im(z!1))" "y" "0")) (("" (assert) (("" (hide-all-but -1) (("" (lemma "unique_characterization" ("x0" "cos(Im(z!1))" "x1" "0" "y0" "sin(Im(z!1))" "y1" "0")) (("" (rewrite "zero_times1" -1) (("" (assert) (("" (lemma "sin_cos_eq_0" ("a" "Im(z!1)")) (("" (flatten -1) (("" (hide -2) (("" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (rewrite "commutative_mult") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil) (i const-decl "complex" complex_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" 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) (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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nnreal_times_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/") (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Re_is_real application-judgement "real" complex_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (unique_characterization formula-decl nil complex_types nil) (commutative_mult formula-decl nil number_fields nil) (sin_cos_eq_0 formula-decl nil trig_aux nil) (zero_times1 formula-decl nil number_fields_bis nil) (both_sides_times1 formula-decl nil number_fields_bis nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (cos const-decl "real" trig_basic "trig/") (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (sin const-decl "real" trig_basic "trig/") (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (exp_real 0 (exp_real-1 nil 3294334350 ("" (skosimp) (("" (expand "exp" 1 1) (("" (rewrite "Re_real" 1) (("" (rewrite "Im_real" 1) (("" (rewrite "sin_0") (("" (rewrite "cos_0") (("" (rewrite "zero_times2") (("" (rewrite "zero_times1") (("" (rewrite "identity_mult" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (sin_range application-judgement "trig_range" trig_basic "trig/") (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (exp const-decl "nzcomplex" exp nil) (Im_real formula-decl nil arithmetic nil) (cos_0 formula-decl nil trig_basic "trig/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (i const-decl "complex" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (zero_times1 formula-decl nil number_fields_bis nil) (identity_mult formula-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (zero_times2 formula-decl nil number_fields_bis 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/") (sin_0 formula-decl nil trig_basic "trig/") (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) (Re_real formula-decl nil arithmetic nil)) shostak)) (exp_imag 0 (exp_imag-1 nil 3294844116 ("" (skosimp) (("" (expand "exp") (("" (lemma "Re_imag" ("x" "r!1")) (("" (lemma "Im_imag" ("x" "r!1")) (("" (replace -1) (("" (replace -2) (("" (rewrite "exp_0") (("" (rewrite "identity_mult") (("" (lemma "commutative_mult" ("x" "sin(r!1)" "y" "i")) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (sin_range application-judgement "trig_range" trig_basic "trig/") (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (exp const-decl "nzcomplex" exp nil) (Im_imag formula-decl nil arithmetic nil) (sin const-decl "real" trig_basic "trig/") (numfield nonempty-type-eq-decl nil number_fields nil) (identity_mult formula-decl nil number_fields nil) (Re_is_real application-judgement "real" complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (i const-decl "complex" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (commutative_mult formula-decl nil number_fields nil) (exp_0 formula-decl nil ln_exp "lnexp/") (Re_imag formula-decl nil arithmetic 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)) shostak)) (abs_exp_imag 0 (abs_exp_imag-1 nil 3294844749 ("" (skosimp) (("" (rewrite "exp_imag") (("" (expand "abs") (("" (expand "conjugate") (("" (rewrite "Im_plus") (("1" (rewrite "Re_plus") (("1" (assert) (("1" (lemma "Re_imag" ("x" "sin(r!1)")) (("1" (rewrite "commutative_mult" -1) (("1" (replace -1) (("1" (rewrite "Im_real" 1) (("1" (rewrite "zero_times1") (("1" (rewrite "zero_times1") (("1" (rewrite "zero_times1") (("1" (rewrite "zero_times2") (("1" (assert) (("1" (lemma "Im_imag" ("x" "sin(r!1)")) (("1" (rewrite "commutative_mult" -1) (("1" (replace -1) (("1" (rewrite "sq.sq_rew") (("1" (rewrite "Re_real" 1) (("1" (rewrite "sq.sq_rew") (("1" (assert) (("1" (rewrite "associative_mult" 1 :dir rl) (("1" (rewrite "i_axiom") (("1" (assert) (("1" (rewrite "minus_add") (("1" (rewrite "number_fields_times_negative" 1) (("1" (rewrite "number_fields_negate_negate") (("1" (lemma "sin2_cos2" ("a" "r!1")) (("1" (assert) (("1" (replace -1 1) (("1" (rewrite "sqrt_1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "closed_times") (("2" (rewrite "real_is_complex") nil nil)) nil) ("3" (rewrite "real_is_complex") nil nil)) nil)) nil)) nil)) nil)) nil) ((exp_imag formula-decl nil exp 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) (sin_range application-judgement "trig_range" trig_basic "trig/") (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (Re_is_real application-judgement "real" complex_types nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (conjugate const-decl "complex" arithmetic nil) (Re_plus formula-decl nil arithmetic nil) (Re_imag formula-decl nil arithmetic nil) (zero_times1 formula-decl nil number_fields_bis nil) (sq_rew formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (associative_mult formula-decl nil number_fields nil) (number_fields_times_negative formula-decl nil number_fields_bis nil) (minus_real_is_real application-judgement "real" reals nil) (sin2_cos2 formula-decl nil trig_basic "trig/") (sqrt_1 formula-decl nil sqrt "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (number_fields_negate_negate formula-decl nil number_fields_bis nil) (minus_add formula-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (i_axiom formula-decl nil complex_types nil) (Re_real formula-decl nil arithmetic nil) (Im_imag formula-decl nil arithmetic nil) (minus_even_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (zero_times2 formula-decl nil number_fields_bis nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (Im_real formula-decl nil arithmetic nil) (commutative_mult formula-decl nil number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (Im_plus formula-decl nil arithmetic nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (cos const-decl "real" trig_basic "trig/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (i const-decl "complex" complex_types nil) (sin const-decl "real" trig_basic "trig/") (abs const-decl "nnreal" polar nil)) shostak)) (arg_exp_real 0 (arg_exp_real-1 nil 3294848302 ("" (skosimp) (("" (rewrite "exp_real") (("" (typepred "ln_exp.exp(r!1)") (("" (rewrite "arg_is_0" 1) (("" (rewrite "Re_real") (("" (rewrite "Im_real") nil nil)) nil)) nil)) nil)) nil)) nil) ((exp_real formula-decl nil exp 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) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (arg_is_0 formula-decl nil polar nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Im_real formula-decl nil arithmetic nil) (Re_real formula-decl nil arithmetic nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" 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/")) shostak)) (arg_exp_imag 0 (arg_exp_imag-1 nil 3294848362 ("" (skosimp) (("" (rewrite "exp_imag") (("" (typepred "theta!1") (("" (expand "arg") (("" (rewrite "Im_plus") (("1" (rewrite "Im_real") (("1" (rewrite "Re_plus") (("1" (lemma "Re_imag" ("x" "sin(theta!1)")) (("1" (assert) (("1" (lemma "Im_imag" ("x" "sin(theta!1)")) (("1" (rewrite "commutative_mult") (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (assert) (("1" (rewrite "Re_real") (("1" (lift-if) (("1" (prop) (("1" (lemma "unique_characterization" ("x0" "cos(theta!1)" "x1" "0" "y0" "sin(theta!1)" "y1" "0")) (("1" (rewrite "zero_times1" -1) (("1" (rewrite "commutative_mult" -1) (("1" (replace -2) (("1" (flatten -1) (("1" (hide -3) (("1" (lemma "sin_cos_eq_0" ("a" "theta!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "0<=theta!1") (("1" (hide -3 1 2) (("1" (lemma "sin_ge_0" ("a" "theta!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "atan2_cos_sin" ("a" "-theta!1")) (("1" (rewrite "cos_neg") (("1" (rewrite "sin_neg") (("1" (expand "atan2") (("1" (case-replace "cos(theta!1) > 0") (("1" (assert) (("1" (lemma "atan_neg") (("1" (inst - "sin(theta!1) / cos(theta!1)") (("1" (replace -1 -3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "cos(theta!1)=0") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "atan_neg" ("x" "sin(theta!1) / cos(theta!1)")) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("3" (case-replace "0<=theta!1") (("1" (rewrite "atan2_cos_sin") nil nil) ("2" (hide 3 4) (("2" (lemma "sin_gt_0" ("a" "-theta!1")) (("2" (rewrite "sin_neg") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "closed_times") (("2" (rewrite "real_is_complex") nil nil)) nil) ("3" (rewrite "real_is_complex") nil nil)) nil)) nil) ("2" (rewrite "closed_times") (("2" (rewrite "real_is_complex") nil nil)) nil) ("3" (rewrite "real_is_complex") nil nil)) nil)) nil)) nil)) nil)) nil) ((exp_imag formula-decl nil exp 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) (AND const-decl "[bool, bool -> bool]" booleans 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/") (<= const-decl "bool" reals nil) (argrng nonempty-type-eq-decl nil polar nil) (sin_range application-judgement "trig_range" trig_basic "trig/") (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (arg const-decl "argrng" polar nil) (Im_real formula-decl nil arithmetic nil) (Re_imag formula-decl nil arithmetic nil) (Im_imag formula-decl nil arithmetic nil) (Re_real formula-decl nil arithmetic nil) (zero_times1 formula-decl nil number_fields_bis nil) (sin_cos_eq_0 formula-decl nil trig_aux nil) (unique_characterization formula-decl nil complex_types nil) (minus_real_is_real application-judgement "real" reals nil) (atan2_cos_sin formula-decl nil atan2 "trig/") (nnreal type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sin_neg formula-decl nil trig_basic "trig/") (atan_neg formula-decl nil atan "trig/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (complex_div_nzcomplex_is_complex application-judgement "complex" complex_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (atan2 const-decl "real" atan2 "trig/") (cos_neg formula-decl nil trig_basic "trig/") (sin_ge_0 formula-decl nil trig_ineq "trig/") (sin_gt_0 formula-decl nil trig_ineq "trig/") (commutative_mult formula-decl nil number_fields nil) (Re_is_real application-judgement "real" complex_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Re_plus formula-decl nil arithmetic nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (nil application-judgement "nnreal_lt_2pi" atan2 "trig/") (sin const-decl "real" trig_basic "trig/") (i const-decl "complex" complex_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (cos const-decl "real" trig_basic "trig/") (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (Im_plus formula-decl nil arithmetic nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (exp_0 0 (exp_0-1 nil 3294273290 ("" (expand "exp") (("" (rewrite "Re_real") (("" (rewrite "Im_real") (("" (rewrite "exp_0") (("" (rewrite "sin_0") (("" (rewrite "cos_0") (("" (rewrite "zero_times1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Re_real formula-decl nil arithmetic 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) (exp_0 formula-decl nil ln_exp "lnexp/") (cos_0 formula-decl nil trig_basic "trig/") (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (zero_times1 formula-decl nil number_fields_bis nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (i const-decl "complex" complex_types nil) (sin_0 formula-decl nil trig_basic "trig/") (Im_real formula-decl nil arithmetic nil) (exp const-decl "nzcomplex" exp nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (real_times_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic "trig/") (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (exp_1 0 (exp_1-1 nil 3294274905 ("" (expand "exp") (("" (expand "e") (("" (rewrite "Re_real") (("" (rewrite "Im_real") (("" (rewrite "sin_0") (("" (rewrite "cos_0") (("" (rewrite "zero_times2") (("" (rewrite "zero_times1") (("" (rewrite "identity_mult") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((e const-decl "posreal" ln_exp "lnexp/") (Im_real formula-decl nil arithmetic nil) (cos_0 formula-decl nil trig_basic "trig/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (i const-decl "complex" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (zero_times1 formula-decl nil number_fields_bis nil) (identity_mult formula-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (exp_1 formula-decl nil ln_exp "lnexp/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (zero_times2 formula-decl nil number_fields_bis 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/") (sin_0 formula-decl nil trig_basic "trig/") (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) (Re_real formula-decl nil arithmetic nil) (exp const-decl "nzcomplex" exp nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (real_times_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic "trig/") (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (exp_i_pi 0 (exp_i_pi-1 nil 3294274991 ("" (lemma "exp_imag" ("r" "pi")) (("" (rewrite "cos_pi") (("" (rewrite "sin_pi") (("" (rewrite "zero_times2") (("" (assert) (("" (rewrite "commutative_mult") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cos_pi formula-decl nil trig_basic "trig/") (cos_range application-judgement "trig_range" trig_basic "trig/") (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (i const-decl "complex" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (zero_times2 formula-decl nil number_fields_bis nil) (numfield nonempty-type-eq-decl nil number_fields nil) (commutative_mult formula-decl nil number_fields nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (sin_pi formula-decl nil trig_basic "trig/") (exp_imag formula-decl nil exp 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic "trig/") (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic "trig/") (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic "trig/")) shostak)) (exp_plus 0 (exp_plus-1 nil 3294335316 ("" (skosimp) (("" (expand "exp") (("" (rewrite "Re_plus") (("" (rewrite "Im_plus") (("" (rewrite "sin_plus") (("" (rewrite "cos_plus") (("" (rewrite "exp_sum" 1) (("" (assert) (("" (name-replace "DRL101" "ln_exp.exp(Re(x!1)) * ln_exp.exp(Re(y!1)) * sin(Im(x!1)) * sin(Im(y!1))") (("" (rewrite "associative_mult" 1 :dir rl) (("" (rewrite "i_axiom") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (sin_range application-judgement "trig_range" trig_basic "trig/") (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (exp const-decl "nzcomplex" exp nil) (Im_plus formula-decl nil arithmetic nil) (cos_plus formula-decl nil trig_basic "trig/") (real_minus_real_is_real application-judgement "real" reals nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (associative_mult formula-decl nil number_fields nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (i_axiom formula-decl nil complex_types 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) (ln const-decl "real" ln_exp "lnexp/") (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp/") (sin const-decl "real" trig_basic "trig/") (exp_sum formula-decl nil ln_exp "lnexp/") (Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil) (sin_plus formula-decl nil trig_basic "trig/") (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (i const-decl "complex" complex_types nil) (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (Re_plus formula-decl nil arithmetic 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) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil)) shostak)) (exp_negate 0 (exp_negate-1 nil 3294275508 ("" (skosimp) (("" (expand "exp") (("" (rewrite "Re_neg") (("" (rewrite "Im_neg") (("" (rewrite "sin_neg") (("" (rewrite "cos_neg") (("" (rewrite "exp_neg") (("" (assert) (("" (typepred "ln_exp.exp(Re(x!1))") (("" (hide -1 -3) (("" (name-replace "R" "ln_exp.exp(Re(x!1))") (("" (rewrite "div_cancel4" 1) (("" (assert) (("" (lemma "number_fields_negative_times" ("x" "1" "y" "sin(Im(x!1))")) (("" (rewrite "identity_mult") (("" (replace -1 * rl) (("" (hide -1) (("" (assert) (("" (assert) (("" (rewrite "commutative_mult" 1 :dir rl) (("" (rewrite "commutative_mult" 1 :dir rl) (("" (assert) (("" (rewrite "sq.sq_rew") (("" (rewrite "sq.sq_rew") (("" (rewrite "associative_mult" 1 :dir rl) (("" (rewrite "i_axiom") (("" (assert) (("" (rewrite "minus_add" 1) (("" (rewrite "number_fields_times_negative" 1 :dir rl) (("" (assert) (("" (rewrite "number_fields_negate_negate" 1) (("" (rewrite "commutative_mult" 1 :dir rl) (("" (rewrite "identity_mult") (("" (lemma "sin2_cos2" ("a" "Im(x!1)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (sin_range application-judgement "trig_range" trig_basic "trig/") (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic "trig/") (exp const-decl "nzcomplex" exp nil) (Im_neg formula-decl nil arithmetic nil) (cos_neg formula-decl nil trig_basic "trig/") (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (cos const-decl "real" trig_basic "trig/") (sin const-decl "real" trig_basic "trig/") (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (div_cancel4 formula-decl nil number_fields_bis nil) (number_fields_negative_times formula-decl nil number_fields_bis nil) (commutative_mult formula-decl nil number_fields nil) (i_axiom formula-decl nil complex_types nil) (minus_add formula-decl nil number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sin2_cos2 formula-decl nil trig_basic "trig/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (number_fields_negate_negate formula-decl nil number_fields_bis nil) (number_fields_times_negative formula-decl nil number_fields_bis nil) (real_minus_real_is_real application-judgement "real" reals nil) (associative_mult formula-decl nil number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (sq_rew formula-decl nil sq "reals/") (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (identity_mult formula-decl nil number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp/") (ln const-decl "real" ln_exp "lnexp/") (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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (complex_div_nzcomplex_is_complex application-judgement "complex" complex_types nil) (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (exp_neg formula-decl nil ln_exp "lnexp/") (Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil) (sin_neg formula-decl nil trig_basic "trig/") (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (i const-decl "complex" complex_types nil) (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_real_is_real application-judgement "real" reals nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types 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) (Re_neg formula-decl nil arithmetic nil)) shostak)) (exp_minus 0 (exp_minus-1 nil 3294334655 ("" (skosimp) (("" (rewrite "minus_add") (("" (rewrite "exp_plus") (("" (rewrite "exp_negate") (("" (rewrite "commutative_mult") (("" (rewrite "div_def" 1 :dir rl) nil nil)) nil)) nil)) nil)) nil)) nil) ((minus_add formula-decl nil number_fields 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) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (exp_negate formula-decl nil exp nil) (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (complex_div_nzcomplex_is_complex application-judgement "complex" complex_types nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (div_def formula-decl nil number_fields nil) (commutative_mult formula-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (exp const-decl "nzcomplex" exp nil) (nznum_times_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (exp_plus formula-decl nil exp nil) (- const-decl "[numfield -> numfield]" number_fields 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)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.67 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
