| products/sources/formale sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: vectors_4D.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(arithmetic
(complex_is_Re_Im 0 (complex_is_Re_Im-1 nil 3294311404 ("" (skosimp) (("" (typepred "Re(z!1)") (("" (typepred "Im(z!1)") (("" (skosimp*) (("" (lemma "unique_characterization") (("" (inst-cp - "x!1" "Re(z!1)" "Im(z!1)" "y!1") (("" (assert) 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) (= const-decl "[T, T -> boolean]" equalities 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) (Re_is_real application-judgement "real" complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (unique_characterization formula-decl nil complex_types nil) (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (complex_is_0_Re_Im 0 (complex_is_0_Re_Im-1 nil 3294676714 ("" (skosimp) (("" (lemma "complex_is_Re_Im" ("z" "z!1")) (("" (prop) (("1" (replace -1) (("1" (lemma "unique_characterization" ("x0" "0" "y0" "0" "x1" "Re(0)" "y1" "Im(0)")) (("1" (assert) (("1" (rewrite "zero_times1") nil nil)) nil)) nil)) nil) ("2" (lemma "unique_characterization" ("x0" "0" "y0" "0" "x1" "Re(0)" "y1" "Im(0)")) (("2" (assert) (("2" (rewrite "zero_times1") (("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (replace -1) (("3" (replace -2) (("3" (rewrite "zero_times1") 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) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (zero_times1 formula-decl nil number_fields_bis nil) (unique_characterization formula-decl nil complex_types nil) (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) (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) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (complex_is_ne_0_Re_Im 0 (complex_is_ne_0_Re_Im-1 nil 3294676902 ("" (skosimp) (("" (lemma "complex_is_0_Re_Im" ("z" "z!1")) (("" (grind) 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_0_Re_Im formula-decl nil arithmetic nil) (/= const-decl "boolean" notequal nil) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (complex_diff_eq_0 0 (complex_diff_eq_0-1 nil 3596363144 ("" (skeep) (("" (ground) (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (case "z2 + (z1-z2) = z1") (("1" (replaces -2) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((complex_minus_complex_is_complex application-judgement "complex" complex_types 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) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" 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 "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (sq_abs_def 0 (sq_abs_def-1 nil 3295002891 ("" (skosimp) (("" (lemma "complex_is_Re_Im" ("z" "z!1")) (("" (name-replace "C" "conjugate(z!1)") (("" (name-replace "RHS" "Re(z!1) * Re(z!1) + Im(z!1) * Im(z!1)") (("" (replace -1) (("" (hide -1) (("" (expand "C") (("" (expand "conjugate") (("" (rewrite "associative_mult" 1 :dir rl) (("" (rewrite "associative_mult" 1 :dir rl) (("" (rewrite "associative_mult" 1 :dir rl) (("" (lemma "i_axiom") (("" (replace -1) (("" (expand "RHS") (("" (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_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (i const-decl "complex" complex_types 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_axiom formula-decl nil complex_types 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) (RHS skolem-const-decl "real" arithmetic nil) (associative_mult formula-decl nil number_fields nil) (C skolem-const-decl "complex" arithmetic nil) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (conjugate const-decl "complex" arithmetic nil) (= const-decl "[T, T -> boolean]" equalities nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (conjugate_nz 0 (conjugate_nz-1 nil 3294677537 ("" (skosimp) (("" (expand "conjugate") (("" (lemma "complex_is_ne_0_Re_Im" ("z" "n0z!1")) (("" (assert) (("" (case-replace "Re(n0z!1) - Im(n0z!1) * i = Re(n0z!1) + -Im(n0z!1) * i") (("1" (hide -1) (("1" (lemma "unique_characterization" ("x0" "Re(n0z!1)" "y0" "-Im(n0z!1)" "x1" "0" "y1" "0")) (("1" (rewrite "zero_times1") (("1" (replace -3 -1) (("1" (simplify -1) (("1" (flatten) (("1" (split) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (assert) (("2" (lemma "both_sides_plus2" ("z" "Im(n0z!1) * i" "x" "-1*( Im(n0z!1) * i)" "y" " -Im(n0z!1) * i")) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (lemma "both_sides_times1" ("n0z" "i" "x" "Im(n0z!1) + (-1 * Im(n0z!1))" "y" "Im(n0z!1) + -Im(n0z!1)")) (("1" (assert) (("1" (rewrite "zero_times1") nil nil)) nil) ("2" (lemma "i_not_real" ("r" "0")) (("2" (assert) 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) (Im_is_real application-judgement "real" complex_types nil) (conjugate const-decl "complex" arithmetic nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (both_sides_plus2 formula-decl nil number_fields_bis nil) (i_not_real formula-decl nil complex_types nil) (nznum nonempty-type-eq-decl nil number_fields nil) (both_sides_times1 formula-decl nil number_fields_bis nil) (zero_times1 formula-decl nil number_fields_bis nil) (unique_characterization formula-decl nil complex_types 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) (- const-decl "[numfield -> numfield]" number_fields nil) (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals 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) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (complex_is_ne_0_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) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil)) shostak)) (sq_abs_realpred 0 (sq_abs_realpred-1 nil 3307799549 ("" (skosimp*) (("" (lemma "complex_is_Re_Im") (("" (name-replace "Cz" "conjugate(z!1)") (("" (inst?) (("" (replace -1) (("" (hide -1) (("" (reveal -3) (("" (replace -1 * rl) (("" (hide -1) (("" (expand "conjugate") (("" (assert) (("" (lemma "i_axiom") (("" (case-replace "Im(z!1) * Im(z!1) * i * i = (Im(z!1) * Im(z!1)) * (i * i)") (("1" (hide -1) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_is_Re_Im formula-decl nil arithmetic nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (i_axiom formula-decl nil complex_types nil) (real_plus_real_is_real application-judgement "real" reals 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) (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) (+ 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_minus_complex_is_complex application-judgement "complex" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (conjugate const-decl "complex" arithmetic 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (nz_sq_abs_pos_TCC1 0 (nz_sq_abs_pos_TCC1-1 nil 3294686654 ("" (skosimp*) (("" (assert) nil nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (sq_abs_realpred formula-decl nil arithmetic nil)) shostak)) (nz_sq_abs_pos 0 (nz_sq_abs_pos-1 nil 3294688448 ("" (expand "conjugate") (("" (skosimp) (("" (lemma "complex_is_Re_Im" ("z" "n0z!1")) (("" (lemma "complex_is_ne_0_Re_Im" ("z" "n0z!1")) (("" (name-replace "X" "Re(n0z!1)") (("" (name-replace "Y" "Im(n0z!1)") (("" (assert) (("" (replace -2) (("" (hide -2) (("" (lemma "commutative_mult") (("" (inst-cp - "Y * i + X" "X") (("" (replace -2 1) (("" (rewrite "distributive" 1) (("" (rewrite "distributive" 1) (("" (name "X2" "X*X") (("" (name "Y2" "Y*Y") (("" (replace -1) (("" (replace -2) (("" (rewrite "associative_mult" 1 :dir rl) (("" (lemma "i_axiom") (("" (replace -1) (("" (rewrite "associative_mult" 1 :dir rl) (("" (assert) (("" (expand "X2") (("" (expand "Y2") (("" (hide-all-but (-6 1)) (("" (case "FORALL (x:nzreal): x*x>0") (("1" (case-replace "X=0") (("1" (rewrite "zero_times1") (("1" (assert) (("1" (inst - "Y") nil nil)) nil)) nil) ("2" (inst-cp - "X") (("1" (case-replace "Y=0") (("1" (rewrite "zero_times1") (("1" (assert) nil nil)) nil) ("2" (inst - "Y") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (lemma "trichotomy" ("x" "x!1")) (("2" (split) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "x!1" "py" "x!1")) (("1" (propax) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (lemma "negreal_times_negreal_is_posreal" ("nx" "x!1" "ny" "x!1")) (("1" (propax) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complex_is_ne_0_Re_Im formula-decl nil arithmetic nil) (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (commutative_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) (real_times_real_is_real application-judgement "real" reals nil) (i_axiom formula-decl nil complex_types nil) (X2 skolem-const-decl "real" arithmetic nil) (trichotomy formula-decl nil real_axioms nil) (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil 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) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (zero_times1 formula-decl nil number_fields_bis nil) (Y skolem-const-decl "{y | EXISTS x: n0z!1 = x + y * i}" arithmetic nil) (X skolem-const-decl "{x | EXISTS y: n0z!1 = x + y * i}" arithmetic nil) (n0z!1 skolem-const-decl "nzcomplex" arithmetic nil) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (nzreal nonempty-type-eq-decl nil reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" 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) (Y2 skolem-const-decl "real" arithmetic nil) (associative_mult formula-decl nil number_fields nil) (distributive formula-decl nil number_fields nil) (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) (complex_minus_complex_is_complex application-judgement "complex" complex_types 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (Re_is_real application-judgement "real" 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) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (conjugate const-decl "complex" arithmetic nil) (Im_is_real application-judgement "real" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (sq_abs_nonneg_TCC1 0 (sq_abs_nonneg_TCC1-1 nil 3294686634 ("" (skosimp*) (("" (assert) nil nil)) nil) ((complex_times_complex_is_complex application-judgement "complex" complex_types nil) (sq_abs_realpred formula-decl nil arithmetic nil)) shostak)) (sq_abs_nonneg 0 (sq_abs_nonneg-1 nil 3294688875 ("" (skosimp) (("" (case-replace "z!1=0") (("1" (rewrite "zero_times1") (("1" (assert) nil nil)) nil) ("2" (lemma "nz_sq_abs_pos" ("n0z" "z!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (conjugate const-decl "complex" arithmetic nil) (zero_times1 formula-decl nil number_fields_bis nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nz_sq_abs_pos formula-decl nil arithmetic nil) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil)) shostak)) (Re_real 0 (Re_real-1 nil 3294273804 ("" (skosimp) (("" (typepred "Re(x!1)") (("" (skosimp) (("" (lemma "unique_characterization" ("x0" "x!1" "y0" "0" "x1" "Re(x!1)" "y1" "y!1")) (("" (assert) 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) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types 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) (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) (Re_is_real application-judgement "real" complex_types nil) (unique_characterization formula-decl nil complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Im_real 0 (Im_real-1 nil 3294274338 ("" (skosimp) (("" (typepred "Im(x!1)") (("" (skosimp) (("" (lemma "unique_characterization" ("x0" "x!1" "y0" "0" "x1" "x!2" "y1" "Im(x!1)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Im const-decl "{y | EXISTS x: z = x + y * i}" 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) (* 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) (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) (Im_is_real application-judgement "real" complex_types nil) (unique_characterization formula-decl nil complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Re_imag 0 (Re_imag-1 nil 3294274425 ("" (skosimp) (("" (typepred "Re(x!1*i)") (("" (skosimp) (("" (lemma "unique_characterization" ("x0" "0" "y0" "x!1" "x1" "Re(x!1*i)" "y1" "y!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities 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) (Re_is_real application-judgement "real" complex_types nil) (unique_characterization formula-decl nil complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Im_imag 0 (Im_imag-1 nil 3294274685 ("" (skosimp) (("" (typepred "Im(x!1*i)") (("" (skosimp) (("" (lemma "unique_characterization" ("x0" "0" "y0" "x!1" "x1" "x!2" "y1" "Im(x!1*i)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities 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) (Im_is_real application-judgement "real" complex_types nil) (unique_characterization formula-decl nil complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Re_neg 0 (Re_neg-1 nil 3294275626 ("" (skosimp) (("" (lemma "complex_is_Re_Im" ("z" "z!1")) (("" (lemma "complex_is_Re_Im" ("z" "-z!1")) (("" (lemma "inverse_add" ("x" "z!1")) (("" (lemma "unique_characterization" ("x0" "Re(z!1)+Re(-z!1)" "y0" "Im(z!1)+Im(-z!1)" "x1" "0" "y1" "0")) (("" (name-replace "K100" "Re(z!1) + Im(z!1) * i") (("" (name-replace "K101" "Re(-z!1) + Im(-z!1) * i") (("" (replace -3 -2) (("" (replace -4 -2) (("" (hide -3 -4) (("" (expand "K100") (("" (expand "K101") (("" (rewrite "zero_times1" -1) (("" (flatten) (("" (hide -2) (("" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) 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) (inverse_add formula-decl nil number_fields nil) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (K101 skolem-const-decl "complex" arithmetic nil) (minus_real_is_real application-judgement "real" reals nil) (zero_times1 formula-decl nil number_fields_bis nil) (K100 skolem-const-decl "complex" arithmetic nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (unique_characterization formula-decl nil complex_types nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities 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) (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Im_neg 0 (Im_neg-1 nil 3294276884 ("" (skosimp) (("" (lemma "unique_characterization" ("x0" "Re(z!1)+Re(-z!1)" "y0" "Im(z!1)+Im(-z!1)" "x1" "0" "y1" "0")) (("" (lemma "complex_is_Re_Im" ("z" "z!1")) (("" (lemma "complex_is_Re_Im" ("z" "-z!1")) (("" (name-replace "K100" "Re(z!1) + Im(z!1) * i") (("" (name-replace "K101" "Re(-z!1) + Im(-z!1) * i") (("" (lemma "inverse_add" ("x" "z!1")) (("" (replace -2 -1) (("" (replace -3 -1) (("" (hide -3 -2) (("" (expand "K101") (("" (expand "K100") (("" (rewrite "zero_times1" -2) (("" (flatten) (("" (hide -3) (("" (split -2) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (- const-decl "[numfield -> numfield]" number_fields 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 "[T, T -> boolean]" equalities nil) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (unique_characterization formula-decl nil complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (minus_complex_is_complex application-judgement "complex" complex_types nil) (K100 skolem-const-decl "complex" arithmetic nil) (minus_real_is_real application-judgement "real" reals nil) (zero_times1 formula-decl nil number_fields_bis nil) (K101 skolem-const-decl "complex" arithmetic nil) (inverse_add formula-decl nil number_fields nil) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (complex_is_Re_Im formula-decl nil arithmetic nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Re_plus 0 (Re_plus-1 nil 3294335512 ("" (skosimp) (("" (typepred "Re(z1!1 + z2!1)") (("" (typepred "Re(z2!1)") (("" (typepred "Re(z1!1)") (("" (skosimp*) (("" (lemma "unique_characterization" ("x0" "Re(z1!1)+Re(z2!1)" "y0" "y!1+y!2" "x1" "Re(z1!1 + z2!1)" "y1" "y!3")) (("" (assert) (("" (assert) (("" (replace -5 1 rl) (("" (hide 2 -5 -2 -4 -6) (("" (lemma "commutative_add") (("" (lemma "associative_add") (("" (inst-cp - "Re(z1!1) + Re(z2!1)" "i * y!1" "i * y!2") (("" (replace -2 1) (("" (inst-cp - "Re(z1!1)" "Re(z2!1)" "i * y!1") (("" (inst-cp - "Re(z1!1)" "Re(z2!1)") (("" (replace -5 -2) (("" (inst-cp - "Re(z2!1)" "Re(z1!1)" "i * y!1") (("" (lemma "commutative_mult" ("y" "i")) (("" (inst-cp - "y!1") (("" (inst - "y!2") (("" (replace -1) (("" (replace -2) (("" (replace -9 -4 rl) (("" (replace -5 -4 rl) (("" (replace -4 1 rl) (("" (inst-cp - "Re(z2!1)" "z1!1") (("" (replace -8 1) (("" (inst - "z1!1" "Re(z2!1)" "i * y!2") (("" (replace -11 -3 rl) (("" (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) ((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) (complex nonempty-type-from-decl nil complex_types nil) (complex_pred const-decl "[number_field -> boolean]" complex_types 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) (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) (Re_is_real application-judgement "real" complex_types nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (unique_characterization formula-decl nil complex_types nil) (associative_add formula-decl nil number_fields nil) (commutative_mult formula-decl nil number_fields nil) (commutative_add formula-decl nil number_fields nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Im_plus 0 (Im_plus-1 nil 3294336438 ("" (skosimp) (("" (lemma "complex_is_Re_Im" ("z" "z1!1+z2!1")) (("" (lemma "Re_plus" ("z1" "z1!1" "z2" "z2!1")) (("" (lemma "complex_is_Re_Im" ("z" "z1!1")) (("" (lemma "complex_is_Re_Im" ("z" "z2!1")) (("" (replace -3 -4) (("" (lemma "both_sides_times1" ("n0z" "i" "x" "Im(z1!1 + z2!1)" "y" "Im(z1!1) + Im(z2!1)")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (name-replace "I1" "Im(z1!1)") (("1" (name-replace "I2" "Im(z2!1)") (("1" (name-replace "I12" "Im(z1!1+z2!1)") (("1" (name-replace "R1" "Re(z1!1)") (("1" (name-replace "R2" "Re(z2!1)") (("1" (replace -1 -4) (("1" (replace -2 -4) (("1" (rewrite "associative_add" -4 :dir rl) (("1" (assert) (("1" (assert) (("1" (replace -4 1 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "i_not_real" ("r" "0")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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_plus_complex_is_complex application-judgement "complex" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types nil) (i_not_real formula-decl nil complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (associative_add formula-decl nil number_fields nil) (Re const-decl "{x | EXISTS y: z = x + y * i}" complex_types 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) (i const-decl "complex" complex_types nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (Im const-decl "{y | EXISTS x: z = x + y * i}" complex_types nil) (Re_plus formula-decl nil arithmetic nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Re_minus 0 (Re_minus-1 nil 3596363408 ("" (skeep) (("" (grind) (("" (lemma "Re_plus") (("" (inst-cp - "z1" "-z2") (("" (assert) (("" (rewrite "Re_neg") (("" (assert) (("" (case "z1-z2 = z1+ - z2") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "number_fields_negative_times") (("2" (inst - "1" "z2") (("2" (replaces -1) (("2" (lemma "identity_mult") (("2" (inst - "z2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Re_is_real application-judgement "real" complex_types nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_complex_is_complex application-judgement "complex" complex_types 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]" number_fields nil) (Re_neg formula-decl nil arithmetic nil) (minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (number_fields_negative_times formula-decl nil number_fields_bis nil) (identity_mult formula-decl nil number_fields 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) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Im_minus 0 (Im_minus-1 nil 3596364512 ("" (skeep) (("" (grind) (("" (lemma "Im_plus") (("" (inst-cp - "z1" "-z2") (("" (assert) (("" (rewrite "Im_neg") (("" (assert) (("" (case "z1-z2 = z1+ - z2") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "number_fields_negative_times") (("2" (inst - "1" "z2") (("2" (replaces -1) (("2" (lemma "identity_mult") (("2" (inst - "z2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Im_is_real application-judgement "real" complex_types nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_complex_is_complex application-judgement "complex" complex_types 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]" number_fields nil) (Im_neg formula-decl nil arithmetic nil) (minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (number_fields_negative_times formula-decl nil number_fields_bis nil) (identity_mult formula-decl nil number_fields nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (Im_plus formula-decl nil arithmetic nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) nil)) (Re_times 0 (Re_times-1 nil 3294675080 ("" (skosimp) (("" (lemma "complex_is_Re_Im") (("" (inst-cp - "z1!1") (("" (inst-cp - "z2!1") (("" (inst - "z1!1*z2!1") (("" (name-replace "RHS" "Re(z1!1 * z2!1) + Im(z1!1 * z2!1) * i") (("" (replace -2 -1) (("" (replace -3 -1) (("" (expand "RHS") (("" (hide -2 -3) (("" (rewrite "associative_mult" -1 :dir rl) (("" (rewrite "associative_mult" -1 :dir rl) (("" (rewrite "associative_mult" -1 :dir rl) (("" (lemma "i_axiom") (("" (expand "sq") (("" (replace -1) (("" (lemma "unique_characterization" ("x0" "Re(z1!1 * z2!1)" "y0" "Im(z1!1 * z2!1)" "x1" "Re(z1!1) * Re(z2!1)+Im(z1!1) * (Im(z2!1) * -1)" "y1" "Im(z1!1) * Re(z2!1)+ Im(z2!1) * Re(z1!1)")) (("" (assert) nil nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.250 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 |
