| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/complex/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 184 kB |
|
Quelle arithmetic.prfSprache: Lisp |
|||||||||||||||
|
(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)) 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) (= const-decl "[T, T -> boolean]" equalities 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) (real_times_real_is_real application-judgement "real" reals nil) (Re_is_real application-judgement "real" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (i_axiom formula-decl nil complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (unique_characterization formula-decl nil complex_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (associative_mult formula-decl nil number_fields nil) (RHS skolem-const-decl "complex" arithmetic 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_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (Im_times 0 (Im_times-1 nil 3294675432 ("" (skosimp) (("" (lemma "complex_is_Re_Im" ("z" "z1!1")) (("" (lemma "complex_is_Re_Im" ("z" "z2!1")) (("" (lemma "complex_is_Re_Im" ("z" "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) (("" (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)")) (("" (rewrite "associative_mult" -2 :dir rl) (("" (rewrite "associative_mult" -2 :dir rl) (("" (rewrite "associative_mult" -2 :dir rl) (("" (lemma "i_axiom") (("" (expand "sq") (("" (replace -1) (("" (hide -1) (("" (assert) nil 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (RHS skolem-const-decl "complex" arithmetic nil) (real_plus_real_is_real application-judgement "real" reals nil) (unique_characterization formula-decl nil complex_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (i_axiom formula-decl nil complex_types nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (associative_mult formula-decl nil number_fields 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) (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) (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) (= const-decl "[T, T -> boolean]" equalities 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_div_TCC1 0 (Re_div_TCC1-1 nil 3294676620 ("" (skosimp) (("" (lemma "nz_sq_abs_pos" ("n0z" "n0z!1")) (("" (assert) nil nil)) nil)) 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) (nz_sq_abs_pos formula-decl nil arithmetic 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)) shostak)) (Re_div 0 (Re_div-2 nil 3308999185 ("" (skolem 1 ("b" "a")) (("" (typepred "b") (("" (hide -1 -2) (("" (lemma "complex_is_Re_Im" ("z" "a")) (("" (lemma "complex_is_Re_Im" ("z" "a/b")) (("" (name-replace "RHS" "Re(a / b) + Im(a / b) * i") (("" (replace -2 -1) (("" (expand "RHS") (("" (lemma "conjugate_nz" ("n0z" "b")) (("" (lemma "div_cancel1" ("n0z" "conjugate(b)" "x" "(Re(a) + Im(a) * i) / b")) (("1" (rewrite "div_div2" -1) (("1" (replace -1 -3 rl) (("1" (hide -1) (("1" (name "D" "b * conjugate(b)") (("1" (lemma "nz_sq_abs_pos" ("n0z" "b")) (("1" (replace -2) (("1" (hide -3) (("1" (expand "conjugate" -3) (("1" (assert) (("1" (rewrite "div_distributes" -3 :dir rl) (("1" (simplify -3) (("1" (rewrite "times_div1" -3) (("1" (case-replace "Im(b) * (Im(a) * i / D) * i = -(Im(a)*Im(b)/D)") (("1" (lemma "unique_characterization" ("x0" "(Re(b) * Re(a)) / D + Im(a) * Im(b) / D" "y0" "Re(b) * Im(a) / D - Im(b) * (Re(a) / D)" "x1" "Re(a / b)" "y1" "Im(a / b)")) (("1" (replace -5 -1 rl) (("1" (assert) (("1" (case-replace "Re(b) * Im(a) / D * i + Im(a) * Im(b) / D = Re(b) * (Im(a) * i / D) - -(Im(a) * Im(b) / D)") (("1" (flatten -2) (("1" (hide -1) (("1" (replace -1 1 rl) (("1" (hide-all-but (-4 1)) (("1" (rewrite "div_distributes") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 -5) (("2" (rewrite "times_div1" 1) (("2" (rewrite "times_div2" 1) (("2" (rewrite "minus_add" 1) (("2" (rewrite "number_fields_negate_negate") (("2" (assert) (("2" (lemma "commutative_mult" ("x" "Im(a)" "y" "Re(b)")) (("2" (replace -1 1) (("2" (rewrite "associative_mult" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "Re(b)") (("2" (typepred "Re(a)") (("2" (typepred "Im(a)") (("2" (typepred "Im(b)") (("2" (hide -1 -3 -5 -7) (("2" (rewrite "times_div1" 1) (("2" (case-replace "Re(b) * Im(a) / D - (Im(b) * Re(a)) / D = (Re(b) * Im(a) - Im(b) * Re(a)) / D") (("1" (lemma "reals.closed_divides" ("x" "Re(b) * Im(a) - Im(b) * Re(a)" "n0z" "D")) (("1" (propax) nil nil) ("2" (assert) (("2" (expand "D") (("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -8 2 -5) (("2" (rewrite "div_distributes_minus" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide 2) (("3" (case "real_pred(D)") (("1" (assert) (("1" (case "real_pred(Im(a) )") (("1" (case "real_pred(Im(b) )") (("1" (flatten) (("1" (case "real_pred(Re(b) )") (("1" (case "real_pred(Re(a) )") (("1" (hide -6 -8 -9 -10) (("1" (lemma "reals.closed_plus") (("1" (inst - "Im(a) * Im(b) / D" "(Re(b) * Re(a)) / D") (("1" (lemma "reals.closed_divides") (("1" (inst?) nil nil)) nil) ("2" (lemma "reals.closed_divides") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (replace -3 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "number_fields_bis.times_div1") (("2" (rewrite "number_fields_bis.times_div1") (("2" (rewrite "number_fields_bis.times_div2" 1) (("2" (rewrite "associative_mult" 1 :dir rl) (("2" (rewrite "associative_mult" 1 :dir rl) (("2" (rewrite "associative_mult" 1 :dir rl) (("2" (lemma "i_axiom") (("2" (replace -1 1) (("2" (assert) (("2" (lemma "both_sides_div1" ("n0z" "D" "x" "Im(a) * (Im(b) * -1)" "y" "-(Im(a) * Im(b))")) (("2" (flatten) (("2" (hide -1) (("2" (split -1) (("1" (replace -1 1) (("1" (hide-all-but (-3 1)) (("1" (rewrite "div_cancel3" 1) (("1" (name-replace "K100" "Im(a) * Im(b)") (("1" (lemma "both_sides_plus2" ("z" "K100" "x" "-K100" "y" "-(K100 / D) * D")) (("1" (replace -1 1 rl) (("1" (rewrite "inverse_add" 1) (("1" (hide -1) (("1" (rewrite "div_def") (("1" (rewrite "number_fields_negative_times") (("1" (rewrite "div_cancel2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -4) (("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) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (complex_is_Re_Im formula-decl nil arithmetic nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (= const-decl "[T, T -> boolean]" equalities 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) (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) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (Re_is_real application-judgement "real" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (RHS skolem-const-decl "complex" arithmetic nil) (div_cancel1 formula-decl nil number_fields_bis nil) (conjugate const-decl "complex" arithmetic nil) (div_distributes formula-decl nil number_fields_bis nil) (times_div1 formula-decl nil number_fields_bis 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) (both_sides_div1 formula-decl nil number_fields_bis nil) (div_cancel3 formula-decl nil number_fields_bis nil) (minus_real_is_real application-judgement "real" reals nil) (both_sides_plus2 formula-decl nil number_fields_bis nil) (inverse_add formula-decl nil number_fields nil) (div_def formula-decl nil number_fields nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (div_cancel2 formula-decl nil number_fields_bis nil) (number_fields_negative_times formula-decl nil number_fields_bis nil) (i_axiom formula-decl nil complex_types nil) (unique_characterization formula-decl nil complex_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (times_div2 formula-decl nil number_fields_bis nil) (number_fields_negate_negate formula-decl nil number_fields_bis nil) (commutative_mult formula-decl nil number_fields nil) (associative_mult formula-decl nil number_fields nil) (minus_add formula-decl nil number_fields nil) (sq_abs_realpred formula-decl nil arithmetic nil) (D skolem-const-decl "complex" arithmetic nil) (nzreal nonempty-type-eq-decl nil reals nil) (closed_divides formula-decl nil reals nil) (div_distributes_minus formula-decl nil number_fields_bis nil) (a skolem-const-decl "complex" arithmetic nil) (b skolem-const-decl "nzcomplex" arithmetic nil) (closed_plus formula-decl nil reals nil) (- const-decl "[numfield -> numfield]" number_fields 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) (nz_sq_abs_pos formula-decl nil arithmetic nil) (div_div2 formula-decl nil number_fields_bis nil) (conjugate_nz formula-decl nil arithmetic nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (complex_div_nzcomplex_is_complex application-judgement "complex" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) nil) (Re_div-1 nil 3294677093 ("" (skolem 1 ("b" "a")) (("" (typepred "b") (("" (hide -1 -2) (("" (lemma "complex_is_Re_Im" ("z" "a")) (("" (lemma "complex_is_Re_Im" ("z" "a/b")) (("" (name-replace "RHS" "Re(a / b) + Im(a / b) * i") (("" (replace -2 -1) (("" (expand "RHS") (("" (lemma "conjugate_nz" ("n0z" "b")) (("" (lemma "div_cancel1" ("n0z" "conjugate(b)" "x" "(Re(a) + Im(a) * i) / b")) (("1" (rewrite "div_div2" -1) (("1" (replace -1 -3 rl) (("1" (hide -1) (("1" (name "D" "b * conjugate(b)") (("1" (lemma "nz_sq_abs_pos" ("n0z" "b")) (("1" (replace -2) (("1" (hide -3) (("1" (expand "conjugate" -3) (("1" (assert) (("1" (rewrite "div_distributes" -3 :dir rl) (("1" (simplify -3) (("1" (rewrite "times_div1" -3) (("1" (case-replace "Im(b) * (Im(a) * i / D) * i = -(Im(a)*Im(b)/D)") (("1" (lemma "unique_characterization" ("x0" "(Re(b) * Re(a)) / D + Im(a) * Im(b) / D" "y0" "Re(b) * Im(a) / D - Im(b) * (Re(a) / D)" "x1" "Re(a / b)" "y1" "Im(a / b)")) (("1" (replace -5 -1 rl) (("1" (assert) (("1" (case-replace "Re(b) * Im(a) / D * i + Im(a) * Im(b) / D = Re(b) * (Im(a) * i / D) - -(Im(a) * Im(b) / D)") (("1" (flatten -2) (("1" (hide -1) (("1" (replace -1 1 rl) (("1" (hide-all-but (-4 1)) (("1" (rewrite "div_distributes") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 -5) (("2" (rewrite "times_div1" 1) (("2" (rewrite "times_div2" 1) (("2" (rewrite "minus_add" 1) (("2" (rewrite "number_fields_negate_negate") (("2" (assert) (("2" (lemma "commutative_mult" ("x" "Im(a)" "y" "Re(b)")) (("2" (replace -1 1) (("2" (rewrite "associative_mult" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "Re(b)") (("2" (typepred "Re(a)") (("2" (typepred "Im(a)") (("2" (typepred "Im(b)") (("2" (hide -1 -3 -5 -7) (("2" (rewrite "times_div1" 1) (("2" (case-replace "Re(b) * Im(a) / D - (Im(b) * Re(a)) / D = (Re(b) * Im(a) - Im(b) * Re(a)) / D") (("1" (lemma "reals.closed_divides" ("x" "Re(b) * Im(a) - Im(b) * Re(a)" "n0z" "D")) (("1" (propax) nil nil) ("2" (assert) (("2" (expand "D") (("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -8 2 -5) (("2" (rewrite "div_distributes_minus" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide 2) (("3" (case "real_pred(D)") (("1" (assert) (("1" (case "real_pred(Im(a) )") (("1" (case "real_pred(Im(b) )") (("1" (flatten) (("1" (case "real_pred(Re(b) )") (("1" (case "real_pred(Re(a) )") (("1" (hide -6 -8 -9 -10) (("1" (case "(FORALL (x,y: number_field): real_pred(x) AND real_pred(y) IMPLIES real_pred(x+y))") (("1" (inst - "Im(a) * Im(b) / D" "(Re(b) * Re(a)) / D") (("1" (assert) (("1" (lemma "reals.closed_divides") (("1" (split) (("1" (inst?) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (lemma "reals.closed_plus") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (replace -3 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "number_fields_bis.times_div1") (("2" (rewrite "number_fields_bis.times_div1") (("2" (rewrite "number_fields_bis.times_div2" 1) (("2" (rewrite "associative_mult" 1 :dir rl) (("2" (rewrite "associative_mult" 1 :dir rl) (("2" (rewrite "associative_mult" 1 :dir rl) (("2" (lemma "i_axiom") (("2" (replace -1 1) (("2" (assert) (("2" (lemma "both_sides_div1" ("n0z" "D" "x" "Im(a) * (Im(b) * -1)" "y" "-(Im(a) * Im(b))")) (("2" (flatten) (("2" (hide -1) (("2" (split -1) (("1" (replace -1 1) (("1" (hide-all-but (-3 1)) (("1" (rewrite "div_cancel3" 1) (("1" (name-replace "K100" "Im(a) * Im(b)") (("1" (lemma "both_sides_plus2" ("z" "K100" "x" "-K100" "y" "-(K100 / D) * D")) (("1" (replace -1 1 rl) (("1" (rewrite "inverse_add" 1) (("1" (hide -1) (("1" (rewrite "div_def") (("1" (rewrite "number_fields_negative_times") (("1" (rewrite "div_cancel2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -4) (("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) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_div2 formula-decl nil number_fields_bis nil) (div_distributes_minus formula-decl nil number_fields_bis nil) (number_fields_negate_negate formula-decl nil number_fields_bis nil) (times_div2 formula-decl nil number_fields_bis nil) (unique_characterization formula-decl nil complex_types nil) (i_axiom formula-decl nil complex_types nil) (number_fields_negative_times formula-decl nil number_fields_bis nil) (div_cancel2 formula-decl nil number_fields_bis nil) (both_sides_plus2 formula-decl nil number_fields_bis nil) (div_cancel3 formula-decl nil number_fields_bis nil) (both_sides_div1 formula-decl nil number_fields_bis nil) (times_div1 formula-decl nil number_fields_bis nil) (div_distributes formula-decl nil number_fields_bis nil) (div_cancel1 formula-decl nil number_fields_bis 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) (complex_pred const-decl "[number_field -> boolean]" complex_types nil) (complex nonempty-type-from-decl nil complex_types nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil)) shostak)) (Im_div 0 (Im_div-1 nil 3294695540 ("" (skolem 1 ("b" "a")) (("" (typepred "b") (("" (hide -1 -2) (("" (lemma "conjugate_nz" ("n0z" "b")) (("" (lemma "nz_sq_abs_pos" ("n0z" "b")) (("" (lemma "complex_is_Re_Im" ("z" "a")) (("" (lemma "complex_is_Re_Im" ("z" "a/b")) (("" (name-replace "RHS" "Re(a / b) + Im(a / b) * i") (("" (replace -2 -1) (("" (expand "RHS") (("" (lemma "div_cancel1" ("x" "(Re(a) + Im(a) * i) / b" "n0z" "conjugate(b)")) (("1" (rewrite "div_div2" -1) (("1" (name-replace "D" "b * conjugate(b)") (("1" (replace -1 -2 rl) (("1" (hide -1 -5) (("1" (rewrite "times_div1" -1) (("1" (expand "conjugate") (("1" (rewrite "associative_mult" -1 :dir rl) (("1" (rewrite "associative_mult" -1 :dir rl) (("1" (rewrite "associative_mult" -1 :dir rl) (("1" (rewrite "associative_mult" -1 :dir rl) (("1" (lemma "i_axiom") (("1" (replace -1 -2) (("1" (rewrite "associative_mult" -2) (("1" (rewrite "associative_mult" -2) (("1" (rewrite "div_cancel3" -2) (("1" (rewrite "div_cancel4" 1) (("1" (lemma "unique_characterization" ("x0" "Im(a) * Im(b) + Re(a) * Re(b)" "y0" "Im(a) * Re(b)-Im(b) * Re(a)" "x1" "Re(a / b) * D" "y1" "Im(a / b) * D")) (("1" (assert) (("1" (hide 2) (("1" (rewrite "associative_mult" -2) nil nil)) nil)) nil) ("2" (lemma "reals.closed_times" ("x" "Im(a / b)" "y" "D")) (("1" (propax) nil nil) ("2" (expand "D") (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "reals.closed_times" ("x" "Re(a / b)" "y" "D")) (("1" (propax) nil nil) ("2" (expand "D") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (conjugate_nz formula-decl nil arithmetic nil) (complex_is_Re_Im formula-decl nil arithmetic nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (= const-decl "[T, T -> boolean]" equalities 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) (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) (real_minus_real_is_real application-judgement "real" reals nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (Re_is_real application-judgement "real" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (RHS skolem-const-decl "complex" arithmetic nil) (div_div2 formula-decl nil number_fields_bis nil) (times_div1 formula-decl nil number_fields_bis nil) (associative_mult formula-decl nil number_fields nil) (i_axiom formula-decl nil complex_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_cancel3 formula-decl nil number_fields_bis nil) (real_plus_real_is_real application-judgement "real" reals nil) (unique_characterization formula-decl nil complex_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (D skolem-const-decl "complex" arithmetic nil) (sq_abs_realpred formula-decl nil arithmetic nil) (closed_times formula-decl nil reals nil) (div_cancel4 formula-decl nil number_fields_bis nil) (conjugate const-decl "complex" arithmetic nil) (div_cancel1 formula-decl nil number_fields_bis nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (complex_div_nzcomplex_is_complex application-judgement "complex" complex_types nil) (nz_sq_abs_pos formula-decl nil arithmetic nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (plus_conjugate 0 (plus_conjugate-1 nil 3294995244 ("" (skosimp) (("" (lemma "complex_is_Re_Im" ("z" "z!1")) (("" (name-replace "DRL1" "conjugate(z!1)") (("" (name-replace "DRL2" "Re(z!1)") (("" (replace -1) (("" (hide -1) (("" (expand "DRL2") (("" (expand "DRL1") (("" (expand "conjugate") (("" (propax) 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) (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) (DRL1 skolem-const-decl "complex" arithmetic nil) (DRL2 skolem-const-decl "{x | EXISTS y: z!1 = x + y * i}" arithmetic nil) (Im_is_real application-judgement "real" complex_types nil) (Re_is_real application-judgement "real" complex_types 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)) (minus_conjugate 0 (minus_conjugate-1 nil 3294995386 ("" (skosimp) (("" (name-replace "DRL1" "conjugate(z!1)") (("" (name-replace "DRL2" "Im(z!1)") (("" (lemma "complex_is_Re_Im" ("z" "z!1")) (("" (replace -1 1) (("" (expand "DRL1") (("" (expand "conjugate") (("" (expand "DRL2") (("" (propax) nil nil)) nil)) nil)) nil)) 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) (conjugate const-decl "complex" arithmetic nil) (real_times_real_is_real application-judgement "real" reals nil) (Im_is_real application-judgement "real" complex_types nil) (complex_is_Re_Im formula-decl nil arithmetic nil) (DRL1 skolem-const-decl "complex" arithmetic nil) (DRL2 skolem-const-decl "{y | EXISTS x: z!1 = x + y * i}" arithmetic 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 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (conjugate_plus 0 (conjugate_plus-1 nil 3294995439 ("" (expand "conjugate") (("" (skosimp) (("" (rewrite "Re_plus") (("" (rewrite "Im_plus") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Im_plus formula-decl nil arithmetic 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) (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_plus formula-decl nil arithmetic nil) (conjugate const-decl "complex" arithmetic nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (complex_plus_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) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (conjugate_neg 0 (conjugate_neg-1 nil 3294995463 ("" (expand "conjugate") (("" (skosimp) (("" (rewrite "Re_neg") (("" (rewrite "Im_neg") (("" (lemma "complex_is_Re_Im" ("z" "-(Re(z!1) - Im(z!1) * i)")) (("" (rewrite "Re_neg" -1) (("" (rewrite "Im_neg" -1) (("" (lemma "unique_characterization" ("x0" "Re((Re(z!1) - Im(z!1) * i))" "x1" "Re(z!1)" "y0" "Im((Re(z!1) - Im(z!1) * i))" "y1" "-Im(z!1)")) (("" (flatten) (("" (hide -2) (("" (split -1) (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (replace -3 1) (("1" (assert) (("1" (rewrite "number_fields_negate_negate") (("1" (assert) (("1" (lemma "neg_times_neg" ("x" "1" "y" "Im(z!1)*i")) (("1" (rewrite "number_fields_negative_times" -1 :dir rl) (("1" (replace -1 1) (("1" (rewrite "number_fields_left_identity_mult") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "minus_add" ("x" "Re(z!1)" "y" "Im(z!1)*i")) (("2" (rewrite "number_fields_negative_times" -1 :dir rl) (("2" (replace -1 1 rl) (("2" (name-replace "DRL1" "Re(z!1) - Im(z!1) * i") (("2" (lemma "complex_is_Re_Im" ("z" "DRL1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Im_neg formula-decl nil arithmetic nil) (unique_characterization formula-decl nil complex_types nil) (minus_add formula-decl nil number_fields nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types nil) (number_fields_negative_times formula-decl nil number_fields_bis nil) (number_fields_left_identity_mult formula-decl nil number_fields_bis nil) (neg_times_neg formula-decl nil number_fields_bis nil) (number_fields_negate_negate formula-decl nil number_fields_bis nil) (complex_is_Re_Im formula-decl nil arithmetic nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[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) (= const-decl "[T, T -> boolean]" equalities 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) (minus_complex_is_complex application-judgement "complex" complex_types nil) (minus_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_nznum_is_nznum application-judgement "nznum" 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) (Re_neg formula-decl nil arithmetic 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) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (conjugate_minus 0 (conjugate_minus-1 nil 3294996440 ("" (skosimp) (("" (lemma "minus_add") (("" (inst-cp - "z1!1" "z2!1") (("" (inst - "conjugate(z1!1)" "conjugate(z2!1)") (("" (lemma "conjugate_plus" ("z1" "z1!1" "z2" "-z2!1")) (("" (lemma "conjugate_neg" ("z" "z2!1")) (("" (replace -4 1) (("" (replace -3 1) (("" (replace -1 1 rl) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_add formula-decl nil number_fields nil) (conjugate const-decl "complex" arithmetic nil) (conjugate_neg formula-decl nil arithmetic 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) (- const-decl "[numfield -> numfield]" number_fields nil) (conjugate_plus formula-decl nil arithmetic nil) (minus_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) (numfield nonempty-type-eq-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)) shostak)) (conjugate_times 0 (conjugate_times-1 nil 3294769074 ("" (expand "conjugate") (("" (skosimp) (("" (rewrite "Re_times") (("" (rewrite "Im_times") (("" (assert) (("" (rewrite "associative_mult" :dir rl) (("" (rewrite "associative_mult" :dir rl) (("" (rewrite "associative_mult" :dir rl) (("" (lemma "i_axiom") (("" (expand "sq") (("" (replace -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Im_times formula-decl nil arithmetic nil) (real_plus_real_is_real application-judgement "real" reals nil) (complex_plus_complex_is_complex application-judgement "complex" complex_types 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) (= const-decl "[T, T -> boolean]" equalities nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (associative_mult formula-decl nil number_fields nil) (i_axiom formula-decl nil complex_types nil) (real_minus_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) (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_times formula-decl nil arithmetic nil) (conjugate const-decl "complex" arithmetic nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (Re_is_real application-judgement "real" complex_types nil) (Im_is_real application-judgement "real" complex_types nil) (complex_times_complex_is_complex application-judgement "complex" complex_types nil)) shostak)) (conjugate_inv_TCC1 0 (conjugate_inv_TCC1-1 nil 3294996737 ("" (lemma "conjugate_nz") (("" (propax) nil nil)) nil) ((conjugate_nz formula-decl nil arithmetic nil)) shostak)) (conjugate_inv 0 (conjugate_inv-1 nil 3294997036 ("" (skosimp) (("" (expand "conjugate") (("" (rewrite "Im_div") (("" (rewrite "Re_div") (("" (rewrite "Im_real") (("" (rewrite "Re_real") (("" (assert) (("" (lemma "nz_sq_abs_pos" ("n0z" "n0z!1")) (("" (lemma "complex_is_Re_Im" ("z" "n0z!1")) (("" (lemma "conjugate_nz" ("n0z" "n0z!1")) (("" (name "DRL" "conjugate(n0z!1)") (("" (replace -1) (("" (expand "conjugate" -1) (("" (replace -1) (("" (name-replace "D" "n0z!1 * DRL") (("" (case-replace "1 * Re(n0z!1) / D - -1 * Im(n0z!1) / D * i = n0z!1/D") (("1" (rewrite "cross_mult" 1) (("1" (expand "D" 1) (("1" (rewrite "number_fields_left_identity_mult" 1) nil nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "number_fields_left_identity_mult" 1) (("2" (rewrite "minus_add" 1) (("2" (case-replace "-(-1 * Im(n0z!1) / D * i) = (Im(n0z!1)*i)/D") (("1" (rewrite "div_distributes" 1) (("1" (rewrite "both_sides_div1" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("2" (rewrite "times_div2" 1) (("2" (lemma "div_def") (("2" (inst-cp - "D" "-1 * (Im(n0z!1) * i)") (("1" (replace -2 1) (("1" (rewrite "number_fields_negative_times" 1 :dir rl) (("1" (rewrite "number_fields_negative_times" 1 :dir rl) (("1" (rewrite "number_fields_negate_negate") (("1" (rewrite "number_fields_left_identity_mult" 1) (("1" (inst - "D" "Im(n0z!1) * i") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) 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) (Im_is_real application-judgement "real" complex_types nil) (conjugate const-decl "complex" arithmetic nil) (Re_div formula-decl nil arithmetic 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) (Re_real formula-decl nil arithmetic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nz_sq_abs_pos formula-decl nil arithmetic nil) (conjugate_nz formula-decl nil arithmetic 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 "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (D skolem-const-decl "complex" arithmetic nil) (number_fields_left_identity_mult formula-decl nil number_fields_bis nil) (cross_mult formula-decl nil number_fields_bis nil) (both_sides_div1 formula-decl nil number_fields_bis nil) (div_distributes formula-decl nil number_fields_bis nil) (div_def formula-decl nil number_fields nil) (number_fields_negate_negate formula-decl nil number_fields_bis nil) (number_fields_negative_times formula-decl nil number_fields_bis nil) (times_div2 formula-decl nil number_fields_bis nil) (minus_add formula-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (complex_is_Re_Im formula-decl nil arithmetic nil) (nznum_div_nznum_is_nznum application-judgement "nznum" number_fields_bis nil) (nzcomplex_div_nzcomplex_is_nzcomplex application-judgement "nzcomplex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (Im_real formula-decl nil arithmetic nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (complex_div_nzcomplex_is_complex application-judgement "complex" complex_types nil) (complex_minus_complex_is_complex application-judgement "complex" complex_types nil) (Re_is_real application-judgement "real" complex_types 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) (Im_div formula-decl nil arithmetic nil)) shostak)) (conjugate_div 0 (conjugate_div-1 nil 3294996775 ("" (skosimp) (("" (lemma "conjugate_inv" ("n0z" "n0z!1")) (("" (lemma "div_def") (("" (inst-cp - "n0z!1" "x!1") (("" (inst - "conjugate(n0z!1)" "conjugate(x!1)") (("1" (replace -1 1) (("1" (replace -2 1) (("1" (replace -3 1 rl) (("1" (lemma "conjugate_times" ("z1" "x!1" "z2" "1/n0z!1")) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "conjugate_nz" ("n0z" "n0z!1")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (conjugate_times formula-decl nil arithmetic nil) (conjugate const-decl "complex" arithmetic nil) (div_def formula-decl nil number_fields nil)) shostak)))
¤ 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.0.119Bemerkung: (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26