| products/Sources/formale Sprachen/Coq/clib/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: minisys.ml Sprache: Unknown
|
(polar
(argrng_TCC1 0 (argrng_TCC1-1 nil 3455850866 ("" (subtype-tcc) nil nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (abs_def 0 (abs_def-1 nil 3455850889 ("" (grind) nil nil) ((Re const-decl "real" complex_types nil) (sq const-decl "nonneg_real" sq "reals/") (Im const-decl "real" complex_types nil) (sq_abs const-decl "nnreal" complex_types nil) (abs const-decl "nnreal" polar nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (abs_def2 0 (abs_def2-1 nil 3472820584 ("" (skosimp) (("" (rewrite "abs_def") (("" (expand "sq_abs") (("" (propax) nil nil)) nil)) nil)) nil) ((abs_def formula-decl nil polar nil) (complex type-decl nil complex_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_abs const-decl "nnreal" complex_types nil)) shostak)) (abs_nzcomplex 0 (abs_nzcomplex-1 nil 3455850866 ("" (skosimp) (("" (expand "abs") (("" (assert) nil nil)) nil)) nil) ((abs const-decl "nnreal" polar nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (nz_sq_abs_pos application-judgement "posreal" complex_types nil)) nil)) (abs_nz_iff_nz 0 (abs_nz_iff_nz-1 nil 3455850929 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (rewrite "abs_def") (("1" (expand "Re" -2 2) (("1" (expand "Im" -3 2) (("1" (replace -2) (("1" (replace -3) (("1" (hide -2 -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "abs(z!1)") (("2" (expand ">=") (("2" (expand "<=") (("2" (split) (("1" (assert) nil nil) ("2" (rewrite "abs_def") (("2" (hide 2) (("2" (lemma "sqrt_eq_0" ("nnx" "sq(Im(z!1)) + sq(Re(z!1))")) (("2" (split) (("1" (expand "Re" 1 2) (("1" (expand "Im" 1 2) (("1" (hide -2) (("1" (rewrite "sq_plus_eq_0") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_def formula-decl nil polar nil) (complex type-decl nil complex_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (sqrt_0 formula-decl nil sqrt "reals/") (/= const-decl "bool" complex_types nil) (Re const-decl "real" complex_types nil) (sq const-decl "nonneg_real" sq "reals/") (Im const-decl "real" complex_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (abs const-decl "nnreal" polar nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (<= const-decl "bool" reals nil) (sq_plus_eq_0 formula-decl nil sq "reals/") (sqrt_eq_0 formula-decl nil sqrt "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (c_ne3 formula-decl nil complex_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (abs_is_0 0 (abs_is_0-1 nil 3455851637 ("" (skosimp) (("" (lemma "abs_nz_iff_nz" ("z" "z!1")) (("" (grind) nil nil)) nil)) nil) ((complex type-decl nil complex_types nil) (abs_nz_iff_nz formula-decl nil polar nil) (= const-decl "bool" complex_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (/= const-decl "bool" complex_types nil) (abs const-decl "nnreal" polar nil) (sq_abs const-decl "nnreal" complex_types nil) (Im const-decl "real" complex_types nil) (sq const-decl "nonneg_real" sq "reals/") (Re const-decl "real" complex_types nil)) shostak)) (abs_neg 0 (abs_neg-1 nil 3455851750 ("" (grind) nil nil) ((Re const-decl "real" complex_types nil) (Im const-decl "real" complex_types nil) (- const-decl "complex" complex_types nil) (sq const-decl "nonneg_real" sq "reals/") (sq_abs const-decl "nnreal" complex_types nil) (abs const-decl "nnreal" polar nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (abs_mult 0 (abs_mult-1 nil 3455851754 ("" (skosimp) (("" (rewrite "abs_def") (("" (rewrite "abs_def") (("" (rewrite "abs_def") (("" (rewrite "sqrt_times" 1 :dir rl) (("" (rewrite "sqrt_eq") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_def formula-decl nil polar nil) (complex type-decl nil complex_types nil) (* const-decl "complex" complex_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Re_mul1 formula-decl nil complex_types nil) (Im_mul1 formula-decl nil complex_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt_eq formula-decl nil sqrt "reals/") (Re const-decl "real" complex_types nil) (Im const-decl "real" complex_types nil) (sq const-decl "nonneg_real" sq "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sqrt_times formula-decl nil sqrt "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (abs_inv 0 (abs_inv-1 nil 3455851970 ("" (skosimp) (("" (rewrite "abs_def") (("" (rewrite "abs_def") (("" (rewrite "sqrt_lem") (("1" (rewrite "sq_rew") (("1" (rewrite "sq_div") (("1" (rewrite "div_cancel3") (("1" (expand "c_div") (("1" (expand "c_div") (("1" (expand "Im") (("1" (expand "Re") (("1" (expand "sq_abs") (("1" (typepred "n0z!1") (("1" (expand "Im") (("1" (expand "Re") (("1" (rewrite "sq_rew") (("1" (rewrite "sq_rew") (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (rewrite "sq_times") (("1" (rewrite "sq_times") (("1" (assert) (("1" (rewrite "sq_neg") (("1" (assert) (("1" (name "DRL" "sq(sq(x(n0z!1)) + sq(y(n0z!1)))") (("1" (replace -1) (("1" (assert) (("1" (name-replace "XX" "sq(x(n0z!1))") (("1" (name-replace "YY" "sq(y(n0z!1))") (("1" (hide -2) (("1" (expand "sq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/=") (("2" (rewrite "sq_plus_eq_0") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "/=") (("2" (hide 1) (("2" (rewrite "sq_plus_eq_0") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/=") (("2" (hide 1) (("2" (lemma "sqrt_eq_0" ("nnx" "sq(Im(n0z!1)) + sq(Re(n0z!1))")) (("2" (split) (("1" (hide -2) (("1" (rewrite "sq_plus_eq_0") (("1" (flatten) (("1" (typepred "n0z!1") (("1" (split) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "sqrt(sq(Im(n0z!1)) + sq(Re(n0z!1)))")) (("1" (assert) nil nil) ("2" (hide 2) (("2" (rewrite "sqrt_pos") (("2" (hide 2) (("2" (typepred "n0z!1") (("2" (split) (("1" (assert) (("1" (lemma "sq_nz_pos" ("nz" "Re(n0z!1)")) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "sq_nz_pos" ("nz" "Im(n0z!1)")) (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_def formula-decl nil polar nil) (complex type-decl nil 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (Re const-decl "real" complex_types nil) (Im const-decl "real" complex_types nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (/ const-decl "complex" complex_types nil) (abs_nzcomplex application-judgement "posreal" polar nil) (nz_sq_abs_pos application-judgement "posreal" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_nzcomplex2 application-judgement "nzcomplex" complex_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Re_div2 formula-decl nil complex_types nil) (Im_div2 formula-decl nil complex_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sqrt_lem formula-decl nil sqrt "reals/") (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (sq_abs const-decl "nnreal" complex_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sq_div formula-decl nil sq "reals/") (sq_1 formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (y adt-accessor-decl "[complex -> real]" complex_types nil) (x adt-accessor-decl "[complex -> real]" complex_types nil) (sq_plus_eq_0 formula-decl nil sq "reals/") (sq_times formula-decl nil sq "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (sqrt_eq_0 formula-decl nil sqrt "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_rew formula-decl nil sq "reals/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_pos judgement-tcc nil sqrt "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (sq_nz_pos judgement-tcc nil sq "reals/")) shostak)) (abs_div 0 (abs_div-1 nil 3455853159 ("" (skosimp) (("" (lemma "abs_inv" ("n0z" "n0z!1")) (("" (lemma "abs_mult" ("z1" "z!1" "z2" "1/n0z!1")) (("" (replace -2) (("" (hide -2) (("" (replace -1 1 rl) (("" (hide -1) (("" (expand "abs") (("" (rewrite "sqrt_eq") (("" (expand "sq_abs") (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nzcomplex nonempty-type-eq-decl nil complex_types nil) (Im const-decl "real" complex_types nil) (Re const-decl "real" complex_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (/= const-decl "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (complex type-decl nil complex_types nil) (abs_inv formula-decl nil polar nil) (abs_nzcomplex application-judgement "posreal" polar nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (abs const-decl "nnreal" polar nil) (Im_div1 formula-decl nil complex_types nil) (Re_div1 formula-decl nil complex_types nil) (Re_div2 formula-decl nil complex_types nil) (Im_div2 formula-decl nil complex_types nil) (Im_mul1 formula-decl nil complex_types nil) (Re_mul1 formula-decl nil complex_types nil) (nz_sq_abs_pos application-judgement "posreal" complex_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (div_nzcomplex2 application-judgement "nzcomplex" complex_types nil) (* const-decl "complex" complex_types nil) (/ const-decl "complex" complex_types nil) (sq_abs const-decl "nnreal" complex_types nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (sqrt_eq formula-decl nil sqrt "reals/") (abs_mult formula-decl nil polar nil) (/ const-decl "complex" complex_types nil)) shostak)) (abs_triangle 0 (abs_triangle-1 nil 3455853469 ("" (skosimp) (("" (expand "abs") (("" (rewrite "sq_le" 1 :dir rl) (("" (assert) (("" (rewrite "sq_plus") (("" (rewrite "sqrt_times" 1 :dir rl) (("" (expand "sq_abs") (("" (assert) (("" (rewrite "sq_plus") (("" (rewrite "sq_plus") (("" (assert) (("" (case "Im(z1!1) * Im(z2!1)+Re(z1!1) * Re(z2!1) <=sqrt(sq(Im(z1!1)) * sq(Im(z2!1)) + sq(Im(z1!1)) * sq(Re(z2!1)) + (sq(Im(z2!1)) * sq(Re(z1!1)) + sq(Re(z1!1)) * sq(Re(z2!1))))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (rewrite "sq_times" 1 :dir rl) (("2" (rewrite "sq_times" 1 :dir rl) (("2" (rewrite "sq_times" 1 :dir rl) (("2" (rewrite "sq_times" 1 :dir rl) (("2" (rewrite "sq_le" 1 :dir rl) (("2" (rewrite "sq_plus") (("2" (assert) (("2" (case "2*(Im(z1!1) * Im(z2!1) * Re(z1!1) * Re(z2!1)) <= sq(Im(z1!1) * Re(z2!1)) + sq(Im(z2!1) * Re(z1!1))") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "sq_minus" ("a" "Im(z1!1) * Re(z2!1)" "b" "Im(z2!1) * Re(z1!1)")) (("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) ((abs const-decl "nnreal" polar nil) (sq_sqrt formula-decl nil sqrt "reals/") (sqrt_times formula-decl nil sqrt "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (Im_add1 formula-decl nil complex_types nil) (Re_add1 formula-decl nil complex_types nil) (Re const-decl "real" complex_types nil) (<= const-decl "bool" reals nil) (sq const-decl "nonneg_real" sq "reals/") (sq_times formula-decl nil sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (sq_minus formula-decl nil sq "reals/") (real_times_real_is_real application-judgement "real" reals nil) (Im const-decl "real" complex_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_plus formula-decl nil sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "complex" complex_types nil) (sq_abs const-decl "nnreal" complex_types nil) (complex type-decl nil complex_types nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (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) (sq_le formula-decl nil sq "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (abs_abs 0 (abs_abs-1 nil 3455851919 ("" (skosimp) (("" (rewrite "abs_def") (("" (expand "abs" 1) (("" (propax) nil nil)) nil)) nil)) nil) ((abs_def formula-decl nil polar nil) (complex type-decl nil complex_types nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) shostak)) (abs_i 0 (abs_i-1 nil 3455851913 ("" (grind) nil nil) ((complex_i const-decl "nzcomplex" complex_types nil) (Re const-decl "real" complex_types nil) (sq const-decl "nonneg_real" sq "reals/") (Im const-decl "real" complex_types nil) (sq_abs const-decl "nnreal" complex_types nil) (sqrt_1 formula-decl nil sqrt "reals/") (abs const-decl "nnreal" polar nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_nzcomplex application-judgement "posreal" polar nil)) shostak)) (abs_div2 0 (abs_div2-1 nil 3455991712 ("" (skosimp) (("" (rewrite "abs_def") (("" (rewrite "abs_def") (("" (rewrite "sq_eq" 1 :dir rl) (("" (assert) (("" (rewrite "sq_div") (("" (rewrite "sq_div") (("" (rewrite "sq_div") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_def formula-decl nil polar nil) (complex type-decl nil 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (/ const-decl "complex" complex_types nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Re_div3 formula-decl nil complex_types nil) (Im_div3 formula-decl nil complex_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_eq formula-decl nil sq "reals/") (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (Im const-decl "real" complex_types nil) (Re const-decl "real" complex_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_div formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_abs formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/")) shostak)) (abs_div3 0 (abs_div3-1 nil 3455991811 ("" (skosimp) (("" (rewrite "abs_def") (("" (rewrite "abs_def") (("" (rewrite "sq_eq" 1 :dir rl) (("1" (assert) (("1" (rewrite "sq_div") (("1" (rewrite "sq_div") (("1" (typepred "sq_abs(n0z!1)") (("1" (name "SQ" "sq_abs(n0z!1)") (("1" (expand "sq_abs") (("1" (replace -1) (("1" (rewrite "sq_times") (("1" (rewrite "sq_times") (("1" (rewrite "sq_neg") (("1" (lemma "sqrt_pos" ("px" "SQ")) (("1" (rewrite "sq_div" 1) (("1" (assert) (("1" (case-replace "(sq(x!1) * SQ)/sq(SQ) = sq(x!1) / SQ") (("1" (expand "SQ" -1 1) (("1" (assert) (("1" (expand "sq_abs") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "sq_abs(n0z!1)") (("2" (assert) (("2" (expand "sq_abs") (("2" (lemma "sqrt_pos" ("px" "sq(Im(n0z!1)) + sq(Re(n0z!1))")) (("1" (lemma "both_sides_div_pos_le1" ("pz" "sqrt(sq(Im(n0z!1)) + sq(Re(n0z!1)))" "x" "0" "y" "abs(x!1)")) (("1" (assert) nil nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abs_def formula-decl nil polar nil) (complex type-decl nil 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (Re const-decl "real" complex_types nil) (Im const-decl "real" complex_types nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (/ const-decl "complex" complex_types nil) (abs_nzcomplex application-judgement "posreal" polar nil) (minus_real_is_real application-judgement "real" reals nil) (nz_sq_abs_pos application-judgement "posreal" complex_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (Re_div2 formula-decl nil complex_types nil) (Im_div2 formula-decl nil complex_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_eq formula-decl nil sq "reals/") (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sq_abs const-decl "nnreal" complex_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sq_div formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (sq_times formula-decl nil sq "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_neg formula-decl nil sq "reals/") (sq_abs formula-decl nil sq "reals/") (SQ skolem-const-decl "posreal" polar nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_pos judgement-tcc nil sqrt "reals/") (posreal nonempty-type-eq-decl nil real_types nil) (sq_sqrt formula-decl nil sqrt "reals/") (both_sides_div_pos_le1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (arg_TCC1 0 (arg_TCC1-1 nil 3455854430 ("" (subtype-tcc) nil nil) ((Im const-decl "real" complex_types nil) (Re const-decl "real" complex_types nil) (= const-decl "bool" complex_types nil)) nil)) (arg_TCC2 0 (arg_TCC2-1 nil 3455854430 ("" (skosimp) (("" (expand "Re" 1 2) (("" (expand "Im" 1 2) (("" (assert) (("" (lemma "atan2_0_2pi" ("x" "Re(z!1)" "y" "Im(z!1)")) (("" (assert) (("" (case-replace "Re(z!1) < 0") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nil application-judgement "nnreal_lt_2pi" atan2 "trig/") (real_minus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (c_eq3 formula-decl nil complex_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (atan2_0_2pi formula-decl nil atan2 "trig/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (complex type-decl nil complex_types nil) (Re const-decl "real" complex_types nil) (Im const-decl "real" complex_types nil)) nil)) (arg_TCC3 0 (arg_TCC3-1 nil 3455854430 ("" (subtype-tcc) nil nil) ((Im const-decl "real" complex_types nil) (Re const-decl "real" complex_types nil) (= const-decl "bool" complex_types nil)) nil)) (arg_TCC4 0 (arg_TCC4-1 nil 3455854430 ("" (skosimp) (("" (expand "Re" 2 2) (("" (expand "Im" 2 2) (("" (lemma "atan2_0_2pi" ("x" "Re(z!1)" "y" "Im(z!1)")) (("" (assert) (("" (case-replace "Im(z!1)=0") (("1" (assert) (("1" (flatten) (("1" (case-replace "Re(z!1) >= 0") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (case-replace "Re(z!1) >= 0") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Im const-decl "real" complex_types nil) (Re const-decl "real" complex_types nil) (complex type-decl nil complex_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (atan2_0_2pi formula-decl nil atan2 "trig/") (= const-decl "[T, T -> boolean]" equalities nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (c_eq3 formula-decl nil complex_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nil application-judgement "nnreal_lt_2pi" atan2 "trig/")) nil)) (arg_is_0_nz 0 (arg_is_0_nz-1 nil 3455855531 ("" (skosimp) (("" (expand "arg") (("" (expand "Re" 1 2) (("" (expand "Im" 1 2) (("" (lemma "atan2_0_2pi" ("x" "Re(n0z!1)" "y" "Im(n0z!1)")) (("" (case-replace "Im(n0z!1) =0") (("1" (assert) (("1" (typepred "n0z!1") (("1" (assert) (("1" (flatten) (("1" (case-replace "Re(n0z!1) >= 0") (("1" (flatten) (("1" (assert) (("1" (expand "atan2") (("1" (rewrite "atan_0") (("1" (expand "Re") (("1" (expand "Im") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (hide -2) (("2" (expand "atan2") (("2" (rewrite "atan_0") (("2" (assert) (("2" (expand "Im") (("2" (expand "Re") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "Im(n0z!1) < 0") (("1" (flatten) (("1" (case-replace "Re(n0z!1) >= 0") (("1" (flatten) (("1" (assert) (("1" (expand "Im") (("1" (expand "Re") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Re") (("2" (expand "Im") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (case-replace "Re(n0z!1) >= 0") (("1" (flatten) (("1" (assert) (("1" (expand "atan2") (("1" (expand ">=" -1) (("1" (expand "<=" -1) (("1" (split) (("1" (assert) (("1" (lemma "atan_strict_increasing") (("1" (expand "strict_increasing?") (("1" (inst - "0" "Im(n0z!1) / Re(n0z!1)") (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "Im(n0z!1)" "py" "Re(n0z!1)")) (("1" (assert) (("1" (rewrite "atan_0") (("1" (assert) (("1" (expand "Im") (("1" (expand "Re") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Re") (("2" (expand "Im") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "Re") (("2" (expand "Im") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((arg const-decl "argrng" polar nil) (Im const-decl "real" complex_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (nil application-judgement "nnreal_lt_2pi" atan2 "trig/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (atan2 const-decl "real" atan2 "trig/") (atan_0 formula-decl nil atan "trig/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (c_eq3 formula-decl nil complex_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (<= const-decl "bool" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (atan_strict_increasing formula-decl nil atan "trig/") (atan2_0_2pi formula-decl nil atan2 "trig/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (complex type-decl nil complex_types nil) (bool nonempty-type-eq-decl nil booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil) (Re const-decl "real" complex_types nil)) shostak)) (arg_is_0 0 (arg_is_0-1 nil 3455856156 ("" (skosimp) (("" (case-replace "z!1=0") (("1" (expand "arg") (("1" (replace -1 1) (("1" (expand "Re") (("1" (expand "Im") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "Re") (("1" (expand "Im") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "arg_is_0_nz" ("n0z" "z!1")) (("1" (replace -1) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil) ("2" (hide 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ((complex type-decl nil 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (= const-decl "bool" complex_types nil) (Im const-decl "real" complex_types nil) (c_eq3 formula-decl nil complex_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Re const-decl "real" complex_types nil) (arg const-decl "argrng" polar nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (arg_is_0_nz formula-decl nil polar nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (nzcomplex nonempty-type-eq-decl nil complex_types nil)) shostak)) (arg_is_pi2 0 (arg_is_pi2-1 nil 3455856760 ("" (skosimp) (("" (typepred "arg(z!1)") (("" (expand "arg") (("" (case-replace "Re(z!1)=0") (("1" (case-replace "Im(z!1)>0") (("1" (assert) (("1" (expand "atan2") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (case-replace "Im(z!1)=0") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "atan2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "Im(z!1) < 0") (("1" (assert) (("1" (expand "atan2") (("1" (assert) (("1" (case-replace "Re(z!1)>0") (("1" (assert) (("1" (typepred "atan(Im(z!1) / Re(z!1))") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "atan(Im(z!1) / Re(z!1))") (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "atan2") (("2" (typepred "atan(Im(z!1) / Re(z!1))") (("2" (expand "abs") (("2" (assert) (("2" (case-replace "Re(z!1) > 0") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "atan(Im(z!1) / Re(z!1)) < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((arg const-decl "argrng" polar nil) (argrng nonempty-type-eq-decl nil polar nil) (<= const-decl "bool" reals nil) (complex type-decl nil complex_types nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic "trig/") (pi_ub const-decl "posreal" trig_basic "trig/") (pi_lb const-decl "posreal" trig_basic "trig/") (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Re const-decl "real" complex_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nil application-judgement "nnreal_lt_2pi" atan2 "trig/") (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (c_eq3 formula-decl nil complex_types nil) (atan2 const-decl "real" atan2 "trig/") (Im const-decl "real" complex_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (atan const-decl "real_abs_lt_pi2" atan "trig/") (real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) shostak)) (arg_is_pi 0 (arg_is_pi-1 nil 3455857439 ("" (skosimp) (("" (expand "arg") (("" (case-replace "Im(z!1)=0") (("1" (assert) (("1" (case-replace "Re(z!1)=0") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "atan2") (("2" (rewrite "atan_0") (("2" (assert) (("2" (case-replace "Re(z!1) > 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "atan2") (("2" (case-replace "Re(z!1)=0") (("1" (assert) (("1" (lift-if -2) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (typepred "atan(Im(z!1) / Re(z!1))") (("2" (lift-if -3) (("2" (assert) (("2" (prop) (("2" (lemma "atan_strict_increasing") (("2" (expand "strict_increasing?") (("2" (inst - "Im(z!1) / Re(z!1)" "0") (("2" (rewrite "atan_0") (("2" (lemma "both_sides_div_neg_lt1" ("nz" "Re(z!1)" "y" "0" "x" "Im(z!1)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((arg const-decl "argrng" polar nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (atan const-decl "real_abs_lt_pi2" atan "trig/") (real_abs_lt_pi2 nonempty-type-eq-decl nil atan "trig/") (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic "trig/") (pi_ub const-decl "posreal" trig_basic "trig/") (pi_lb const-decl "posreal" trig_basic "trig/") (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (atan_strict_increasing formula-decl nil atan "trig/") (both_sides_div_neg_lt1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (c_eq3 formula-decl nil complex_types nil) (atan_0 formula-decl nil atan "trig/") (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (atan2 const-decl "real" atan2 "trig/") (Re const-decl "real" complex_types nil) (nil application-judgement "nnreal_lt_2pi" atan2 "trig/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (Im const-decl "real" complex_types nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (complex type-decl nil complex_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (arg_is_mpi2 0 (arg_is_mpi2-1 nil 3455857932 ("" (skosimp) --> -------------------- --> maximum size reached --> -------------------- [ zur Elbe Produktseite wechseln0.50Quellennavigators Analyse erneut starten ] |