| products/sources/formale Sprachen/PVS/complex/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: polar.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(polar
(argrng_TCC1 0 (argrng_TCC1-1 nil 3297457117 ("" (assert) (("" (typepred "pi") (("" (assert) nil nil)) nil)) nil) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic "trig/") (pi_ub const-decl "posreal" trig_basic "trig/") (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic "trig/") (AND const-decl "[bool, bool -> bool]" booleans 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (abs_TCC1 0 (abs_TCC1-1 nil 3294310508 ("" (skosimp) (("" (lemma "complex_is_Re_Im" ("z" "z!1")) (("" (expand "conjugate") (("" (name-replace "R" "Re(z!1)") (("" (name-replace "II" "Im(z!1)") (("" (replace -1) (("" (hide -1) (("" (assert) (("" (rewrite "sq.sq_rew") (("" (rewrite "sq.sq_rew") (("" (lemma "i_axiom") (("" (rewrite "associative_mult" :dir rl) (("" (expand "sq" -1) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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) (complex_is_Re_Im formula-decl nil arithmetic nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals 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) (Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (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) (real_minus_real_is_real application-judgement "real" reals nil) (i_axiom formula-decl nil complex_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (sq_rew formula-decl nil sq "reals/") (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (conjugate const-decl "complex" arithmetic nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (Im_is_real application-judgement "real" complex_types nil)) shostak)) (abs_def 0 (abs_def-1 nil 3385303712 ("" (skosimp) (("" (expand "abs") (("" (lemma "complex_is_Re_Im" ("z" "z!1")) (("" (name-replace "DRL100" "conjugate(z!1)") (("" (name-replace "DRL101" "sqrt(sq.sq(Im(z!1)) + sq.sq(Re(z!1)))") (("" (replace -1) (("" (hide -1) (("" (expand "DRL100") (("" (expand "conjugate") (("" (rewrite "associative_mult" 1 :dir rl) (("" (rewrite "associative_mult" 1 :dir rl) (("" (rewrite "associative_mult" 1 :dir rl) (("" (rewrite "i_axiom") (("" (expand "DRL101") (("" (expand "sq") (("" (rewrite "associative_mult") (("" (rewrite "minus_add") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs const-decl "nnreal" polar nil) (conjugate const-decl "complex" arithmetic nil) (= const-decl "[T, T -> boolean]" equalities nil) (DRL100 skolem-const-decl "complex" polar nil) (associative_mult formula-decl nil number_fields nil) (DRL101 skolem-const-decl "{nnz: nnreal | nnz * nnz = sq.sq(Im(z!1)) + sq.sq(Re(z!1))}" polar nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_add formula-decl nil number_fields nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals 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) (real_times_real_is_real application-judgement "real" reals nil) (Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil) (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (i const-decl "complex" complex_types nil) (sq const-decl "nonneg_real" sq "reals/") (+ 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) (numfield nonempty-type-eq-decl nil number_fields nil) (nnreal type-eq-decl nil real_types 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) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (complex_is_Re_Im 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) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (abs_real_rew 0 (abs_real_rew-1 nil 3385304274 ("" (skosimp) (("" (rewrite "abs_def") (("" (rewrite "Im_real") (("" (rewrite "Re_real") (("" (expand "sq" 1 1) (("" (rewrite "sqrt_sq_abs") nil nil)) nil)) nil)) nil)) nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (abs_def formula-decl nil polar 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (Re_real formula-decl nil arithmetic nil) (sqrt_sq_abs formula-decl nil sqrt "reals/") (sq const-decl "nonneg_real" sq "reals/") (Im_real formula-decl nil arithmetic nil)) shostak)) (abs_imag_rew 0 (abs_imag_rew-1 nil 3596359128 ("" (skeep) (("" (rewrite "abs_def") (("" (rewrite "Re_imag") (("" (rewrite "Im_imag") (("" (case "sq.sq(0) = 0") (("1" (replaces -1) (("1" (assert) (("1" (lemma "sqrt_sq") (("1" (inst - "real_defs.abs(r)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (abs_def formula-decl nil polar 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (i const-decl "complex" complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (Im_imag formula-decl nil arithmetic nil) (sqrt_sq formula-decl nil sqrt "reals/") (sq_abs formula-decl nil sq "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_ge_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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (Re_imag formula-decl nil arithmetic nil)) shostak)) (abs_nzcomplex 0 (abs_nzcomplex-1 nil 3294771107 ("" (skosimp) (("" (expand "abs") (("" (lemma "nz_sq_abs_pos" ("n0z" "n0z!1")) (("" (lemma "sqrt_pos" ("px" "n0z!1 * conjugate(n0z!1)")) (("1" (propax) nil nil) ("2" (expand "conjugate") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((abs const-decl "nnreal" polar nil) (conjugate const-decl "complex" arithmetic nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (sqrt_pos judgement-tcc nil sqrt "reals/") (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (nz_sq_abs_pos 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) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil)) shostak)) (abs_nz_iff_nz 0 (abs_nz_iff_nz-1 nil 3294771228 ("" (skosimp) (("" (prop) (("1" (replace -2) (("1" (grind) nil nil)) nil) ("2" (lemma "abs_nzcomplex" ("n0z" "z!1")) (("1" (propax) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (abs const-decl "nnreal" polar nil) (sqrt_0 formula-decl nil sqrt "reals/") (conjugate const-decl "complex" arithmetic nil) (abs_nzcomplex formula-decl nil polar 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) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil)) shostak)) (abs_is_0 0 (abs_is_0-1 nil 3295007153 ("" (skosimp) (("" (prop) (("1" (typepred "abs(z!1)") (("1" (expand ">=") (("1" (expand "<=") (("1" (split) (("1" (lemma "abs_nz_iff_nz" ("z" "z!1")) (("1" (assert) nil nil)) nil) ("2" (hide -1) (("2" (expand "abs") (("2" (rewrite "sq_abs_def") (("2" (rewrite "sq.sq_rew") (("2" (rewrite "sq.sq_rew") (("2" (rewrite "complex_is_0_Re_Im" 1) (("2" (typepred "sq.sq(Im(z!1))") (("2" (typepred "sq.sq(Re(z!1))") (("2" (lemma "sqrt_eq" ("nny" "sq.sq(Im(z!1)) + sq.sq(Re(z!1))" "nnz" "0")) (("2" (rewrite "sqrt_0") (("2" (replace -1 -4) (("2" (hide -1) (("2" (lemma "sq.sq_nz_pos") (("2" (case-replace "Re(z!1) = 0") (("1" (inst - "Im(z!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (inst - "Re(z!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "abs") (("2" (rewrite "zero_times1") (("2" (rewrite "sqrt_0") nil nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs_nz_iff_nz formula-decl nil polar nil) (Im const-decl "{y | EXISTS x: 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) (= const-decl "[T, T -> boolean]" equalities nil) (sq_rew formula-decl nil sq "reals/") (complex_is_0_Re_Im formula-decl nil arithmetic nil) (sqrt_0 formula-decl nil sqrt "reals/") (sq_0 formula-decl nil sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (z!1 skolem-const-decl "complex" polar nil) (/= const-decl "boolean" notequal nil) (sq_nz_pos judgement-tcc nil sq "reals/") (sqrt_eq formula-decl nil sqrt "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (Re const-decl "{x | EXISTS y: 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) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (sq_abs_def formula-decl nil arithmetic nil) (<= const-decl "bool" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[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) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (nnreal type-eq-decl nil real_types nil) (abs const-decl "nnreal" polar nil) (conjugate const-decl "complex" arithmetic nil) (zero_times1 formula-decl nil number_fields_bis nil)) shostak)) (abs_neg 0 (abs_neg-1 nil 3294998991 ("" (skosimp) (("" (expand "abs") (("" (rewrite "conjugate_neg") (("" (rewrite "neg_times_neg") nil nil)) nil)) nil)) nil) ((minus_complex_is_complex application-judgement "complex" complex_types nil) (abs const-decl "nnreal" polar nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (conjugate const-decl "complex" arithmetic nil) (neg_times_neg formula-decl nil number_fields_bis 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) (conjugate_neg formula-decl nil arithmetic nil)) shostak)) (abs_mult 0 (abs_mult-1 nil 3294697248 ("" (expand "abs") (("" (skolem 1 ("a" "b")) (("" (lemma "sq_abs_nonneg" ("z" "a")) (("" (lemma "sq_abs_nonneg" ("z" "b")) (("" (lemma "sq_abs_nonneg" ("z" "a*b")) (("" (rewrite "sqrt_times" :dir rl) (("1" (assert) (("1" (rewrite "conjugate_times") nil nil)) nil) ("2" (assert) (("2" (expand "conjugate") (("2" (propax) nil nil)) nil)) nil) ("3" (expand "conjugate") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_abs_realpred formula-decl nil arithmetic nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_times formula-decl nil sqrt "reals/") (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) (conjugate const-decl "complex" arithmetic nil) (conjugate_times formula-decl nil arithmetic nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq_abs_nonneg 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) (abs const-decl "nnreal" polar nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (abs_inv_TCC1 0 (abs_inv_TCC1-1 nil 3294998917 ("" (skosimp) (("" (rewrite "abs_is_0") nil nil)) nil) ((abs_is_0 formula-decl nil polar 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) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil)) shostak)) (abs_inv 0 (abs_inv-1 nil 3294999199 ("" (skosimp) (("" (expand "abs") (("" (rewrite "conjugate_inv") (("" (lemma "conjugate_nz" ("n0z" "n0z!1")) (("" (rewrite "div_times") (("" (lemma "nz_sq_abs_pos" ("n0z" "n0z!1")) (("" (rewrite "sqrt_div") (("" (expand "conjugate") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nzcomplex_div_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (abs const-decl "nnreal" polar nil) (conjugate_nz formula-decl nil arithmetic nil) (nz_sq_abs_pos formula-decl nil arithmetic nil) (sqrt_div formula-decl nil sqrt "reals/") (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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt_1 formula-decl nil sqrt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_abs_realpred formula-decl nil arithmetic nil) (nzcomplex_times_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (div_times formula-decl nil number_fields_bis nil) (nznum nonempty-type-eq-decl nil number_fields nil) (conjugate const-decl "complex" arithmetic nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (/= const-decl "boolean" notequal 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) (conjugate_inv formula-decl nil arithmetic nil)) shostak)) (abs_div 0 (abs_div-1 nil 3294999065 ("" (skosimp) (("" (lemma "div_def" ("y" "z!1" "n0x" "n0z!1")) (("" (lemma "abs_mult" ("z1" "z!1" "z2" "1/n0z!1")) (("1" (rewrite "abs_inv" -1) (("1" (assert) nil nil)) nil) ("2" (lemma "real_is_complex" ("x" "1")) (("2" (rewrite "closed_divides") nil nil)) nil)) nil)) nil)) nil) ((numfield nonempty-type-eq-decl nil number_fields nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal 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) (div_def formula-decl nil number_fields nil) (abs_inv formula-decl nil polar nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (complex_div_nzcomplex_is_complex application-judgement "complex" complex_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (abs_mult formula-decl nil polar nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) shostak)) (abs_triangle 0 (abs_triangle-2 nil 3307889278 ("" (skolem 1 ("a" "b")) (("" (expand "abs") (("" (lemma "sq_abs_nonneg" ("z" "a")) (("" (lemma "sq_abs_nonneg" ("z" "b")) (("" (lemma "sq_abs_nonneg" ("z" "a+b")) (("" (case "real_pred(a * conjugate(a))") (("1" (case "real_pred(b * conjugate(b))") (("1" (case "real_pred((a+b) * conjugate(a+b))") (("1" (name "A2" "a * conjugate(a)") (("1" (replace -1) (("1" (name "B2" "b * conjugate(b)") (("1" (replace -1) (("1" (name "AB2" "(a+b) * conjugate(a+b)") (("1" (replace -1) (("1" (case-replace "conjugate(a + b) * a + conjugate(a + b) * b = AB2") (("1" (rewrite "sq_le" 1 :dir rl) (("1" (rewrite "sqrt.sq_sqrt") (("1" (rewrite "sq.sq_plus") (("1" (rewrite "sqrt.sq_sqrt") (("1" (rewrite "sqrt.sq_sqrt") (("1" (rewrite "sqrt.sqrt_times" 1 :dir rl) (("1" (rewrite "conjugate_plus") (("1" (rewrite "distributive" -2) (("1" (lemma "commutative_mult") (("1" (inst-cp - "a" "conjugate(a)") (("1" (inst-cp - "b" "conjugate(b)") (("1" (replace -2 * rl) (("1" (replace -3 * rl) (("1" (replace -6) (("1" (replace -7) (("1" (hide -4) (("1" (name "DRL" "conjugate(a) * b + conjugate(b) * a") (("1" (case-replace "A2 + conjugate(a) * b + conjugate(b) * a + B2 = A2+B2+DRL") (("1" (case "real_pred(DRL)") (("1" (hide -2) (("1" (replace -6 1 rl) (("1" (assert) (("1" (case "A2*B2>=0") (("1" (lemma "both_sides_plus_le2" ("z" "A2+B2" "x" "DRL" "y" "2*sqrt(A2 * B2)")) (("1" (case "DRL<=2 * sqrt(A2 * B2)") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (name-replace "CA" "conjugate(a)") (("2" (name-replace "CB" "conjugate(b)") (("2" (lemma "complex_is_Re_Im" ("z" "a")) (("2" (lemma "complex_is_Re_Im" ("z" "b")) (("2" (replace -1 -5) (("2" (replace -2 -5) (("2" (expand "CA") (("2" (expand "CB") (("2" (expand "conjugate") (("2" (case-replace "DRL = 2*(Re(a)*Re(b)+Im(a)*Im(b))") (("1" (lemma "both_sides_times_pos_le1" ("pz" "2" "x" "Re(a) * Re(b) + Im(a) * Im(b)" "y" "sqrt(A2 * B2)")) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "reals.closed_divides" ("x" "2 * (Re(a) * Re(b) + Im(a) * Im(b))" "n0z" "2")) (("1" (rewrite "times_div1" -1 :dir rl) (("1" (rewrite "div_cancel1" 1) (("1" (case "Im(a) * Im(b) + Re(a) * Re(b) < 0") (("1" (assert) nil nil) ("2" (rewrite "sq_le" 2 :dir rl) (("2" (rewrite "sq_sqrt") (("2" (expand "B2" 2) (("2" (rewrite "sq_abs_def" 2) (("2" (name-replace "DRL_B" "(Im(b) * Im(b) + Re(b) * Re(b))") (("2" (expand "A2") (("2" (lemma "sq_abs_def" ("z" "a")) (("2" (inst-cp -9 "conjugate(a)" "DRL_B") (("2" (replace -10 2) (("2" (rewrite "associative_mult" 2 :dir rl) (("2" (inst-cp -9 "conjugate(a)" "a") (("2" (replace -10 2) (("2" (replace -1 2) (("2" (expand "DRL_B") (("2" (expand "sq") (("2" (assert) (("2" (name "IA" "Im(a)") (("2" (replace -1) (("2" (name "IB" "Im(b)") (("2" (replace -1) (("2" (name "RB" "Re(b)") (("2" (replace -1) (("2" (name "RA" "Re(a)") (("2" (replace -1) (("2" (name-replace "DRL10" "IA * IA * IB * IB ") (("2" (name-replace "DRL11" "RA * RA * RB * RB ") (("2" (assert) (("2" (lemma "both_sides_plus_le2" ("z" "DRL10 + DRL11" "x" "2 * (IA * IB * RA * RB)" "y" "IA * IA * RB * RB + IB * IB * RA * RA")) (("2" (replace -1 2) (("2" (hide-all-but (1 2)) (("2" (case "IA*IB >= -(RA*RB)") (("1" (hide 1) (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.48 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 |
