| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 396 kB |
|
Quelle asin.prf Sprache: Lisp |
|||||||||
|
(asin (real_abs_le_pi2_TCC1 0
(real_abs_le_pi2_TCC1-1 nil 3323019118 ("" (subtype-tcc) nil nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types 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)) nil)) (asin_TCC1 0 (asin_TCC1-1 nil 3262199128 ("" (skolem 1 ("x")) (("" (flatten) (("" (typepred "x") (("" (expand "abs") (("" (assert) (("" (lemma "le_times_le_pos" ("nnx" "-x" "y" "1" "nnz" "-x" "w" "1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil)) shostak)) (asin_TCC2 0 (asin_TCC2-1 nil 3262199262 ("" (grind) (("1" (lemma "sq_lt_abs" ("a" "-x!1" "b" "1")) (("1" (grind) nil nil)) nil) ("2" (rewrite "sq_rew") (("2" (lemma "sq_lt" ("nna" "x!1" "nnb" "1")) (("2" (grind) nil nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (sq_lt_abs formula-decl nil sq "reals/") (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sq const-decl "nonneg_real" sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (asin_TCC3 0 (asin_TCC3-1 nil 3262199449 ("" (skolem 1 ("x")) (("" (flatten) (("" (typepred "x") (("" (expand "abs") (("" (case "x < 0") (("1" (assert) (("1" (lemma "lt_times_lt_pos1" ("px" "-x" "y" "1" "nnz" "-x" "w" "1")) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (lemma "lt_times_lt_pos1" ("px" "x" "y" "1" "nnz" "x" "w" "1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" reals nil) (minus_real_is_real application-judgement "real" reals nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (asin_TCC4 0 (asin_TCC4-1 nil 3262199280 ("" (skolem 1 ("x")) (("" (flatten) (("" (typepred "x") (("" (assert) (("" (typepred "atan(x / sqrt(1 - x * x))") (("1" (rewrite "pi_value" 2) (("1" (expand "atan" 2 4) (("1" (assert) (("1" (expand "atan" -2 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "sqrt_pos" ("px" "1-x*x")) (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "sq_lt_abs" ("a" "x" "b" "1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sq const-decl "nonneg_real" sq "reals/") (sq_lt_abs formula-decl nil sq "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_pos judgement-tcc nil sqrt "reals/") (pi_value formula-decl nil atan nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi_lb const-decl "posreal" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities 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) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (asin_TCC5 0 (asin_TCC5-1 nil 3262199369 ("" (expand "abs") (("" (skolem!) (("" (flatten) (("" (typepred "pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (asin_neg_restrict_TCC1 0 (asin_neg_restrict_TCC1-1 nil 3262231650 ("" (skolem!) (("" (typepred "nx!1") (("" (expand "abs") (("" (lemma "sq_le_abs" ("a" "-nx!1" "b" "1")) (("" (grind) nil nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sq const-decl "nonneg_real" sq "reals/") (sq_le_abs formula-decl nil sq "reals/") (minus_real_is_real application-judgement "real" reals nil)) shostak)) (asin_neg_restrict_TCC2 0 (asin_neg_restrict_TCC2-1 nil 3262231879 ("" (grind) nil nil) nil shostak)) (asin_neg_restrict 0 (asin_neg_restrict-2 nil 3322498655 ("" (skolem 1 ("nx")) (("" (typepred "nx") (("" (expand "<=") (("" (expand "asin") (("" (split -1) (("1" (assert) (("1" (lemma "both_sides_times_neg_lt1" ("nz" "-1" "x" "nx" "y" "-1")) (("1" (lemma "lt_times_lt_neg1" ("x" "-1" "ny" "nx" "z" "-1" "npw" "nx")) (("1" (assert) (("1" (lemma "sqrt_lt" ("nny" "0" "nnz" "1-nx*nx")) (("1" (rewrite "sqrt_0" -1) (("1" (lemma "atan_inv_neg" ("nx" "sqrt(1 - nx * nx) / nx")) (("1" (rewrite "pi_value" 1) (("1" (lemma "div_div1" ("x" "1" "n0y" "sqrt(1-nx*nx)" "n0z" "nx")) (("1" (replace -1 -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "both_sides_div_neg_lt1" ("y" "0" "x" "sqrt(1-nx*nx)" "nz" "nx")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "nx = -1") (("1" (replace -1) (("1" (rewrite "sqrt_0") (("1" (rewrite "atan_0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (asin const-decl "real_abs_le_pi2" asin nil) (atan_0 formula-decl nil atan nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_times_lt_neg1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_lt formula-decl nil sqrt "reals/") (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (atan_inv_neg formula-decl nil atan nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (div_div1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (minus_real_is_real application-judgement "real" reals nil) (pi_value formula-decl nil atan nil) (both_sides_div_neg_lt1 formula-decl nil real_props nil) (sqrt_0 formula-decl nil sqrt "reals/") (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (asin_pos_restrict_TCC1 0 (asin_pos_restrict_TCC1-1 nil 3262251224 ("" (skosimp*) (("" (typepred "px!1") (("" (expand "abs") (("" (lemma "le_times_le_pos" ("nnx" "px!1" "y" "1" "nnz" "px!1" "w" "1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (le_times_le_pos formula-decl nil real_props nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil)) shostak)) (asin_pos_restrict_TCC2 0 (asin_pos_restrict_TCC2-1 nil 3262251224 ("" (grind) nil nil) nil shostak)) (asin_pos_restrict 0 (asin_pos_restrict-1 nil 3408901117 ("" (skolem 1 ("px")) (("" (case "abs(px) <= 1") (("1" (expand "<=") (("1" (split -1) (("1" (expand "asin") (("1" (assert) (("1" (lemma "sq_nz_pos" ("nz" "px")) (("1" (expand "sq") (("1" (lemma "lt_times_lt_pos1" ("px" "px" "y" "1" "nnz" "px" "w" "1")) (("1" (assert) (("1" (lemma "sqrt_lt" ("nny" "0" "nnz" "1-px*px")) (("1" (rewrite "sqrt_0") (("1" (lemma "atan_inv" ("px" "sqrt(1 - px * px) / px")) (("1" (lemma "div_div1" ("x" "1" "n0y" "sqrt(1-px*px)" "n0z" "px")) (("1" (replace -1 -2) (("1" (rewrite "pi_value" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "sqrt(1-px*px)" "py" "px")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "asin") (("2" (assert) (("2" (lift-if) (("2" (expand "abs") (("2" (assert) (("2" (replace -1) (("2" (assert) (("2" (rewrite "atan_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "px") (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_0 formula-decl nil sqrt "reals/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (div_div1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (pi_value formula-decl nil atan nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (atan_inv formula-decl nil atan nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt_lt formula-decl nil sqrt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (sq_nz_pos judgement-tcc nil sq "reals/") (asin const-decl "real_abs_le_pi2" asin nil) (atan_0 formula-decl nil atan nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil)) nil) (asin_pos_restrict-2 nil 3322498693 ("" (skolem 1 ("px")) (("" (typepred "px") (("" (expand "abs" -1) (("" (expand "<=" -1) (("" (split -1) (("1" (expand "asin") (("1" (assert) (("1" (lemma "sq_nz_pos" ("nz" "px")) (("1" (expand "sq") (("1" (lemma "lt_times_lt_pos1" ("px" "px" "y" "1" "nnz" "px" "w" "1")) (("1" (assert) (("1" (lemma "sqrt_lt" ("nny" "0" "nnz" "1-px*px")) (("1" (rewrite "sqrt_0") (("1" (lemma "atan_inv_value" ("px" "sqrt(1 - px * px) / px")) (("1" (lemma "div_div1" ("x" "1" "n0y" "sqrt(1-px*px)" "n0z" "px")) (("1" (replace -1 -2) (("1" (rewrite "pi_value" 1) (("1" (expand "atan" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "sqrt(1-px*px)" "py" "px")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "asin") (("2" (replace -1) (("2" (hide -1 -2) (("2" (rewrite "sqrt_0") (("2" (rewrite "atan_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq const-decl "nonneg_real" sq "reals/") (sqrt_0 formula-decl nil sqrt "reals/") (pi_value formula-decl nil atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sqrt_lt formula-decl nil sqrt "reals/") (sq_nz_pos judgement-tcc nil sq "reals/") (atan_0 formula-decl nil atan nil)) nil)) (asin_0 0 (asin_0-1 nil 3262232045 ("" (expand "asin") (("" (rewrite "sqrt_1") (("" (rewrite "atan_0") nil nil)) nil)) nil) ((sqrt_1 formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (atan_0 formula-decl nil atan nil) (asin const-decl "real_abs_le_pi2" asin nil)) shostak)) (asin_sqrt_half_TCC1 0 (asin_sqrt_half_TCC1-1 nil 3263820156 ("" (expand "abs") (("" (typepred "sqrt(1/2)") (("" (assert) (("" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1")) (("" (rewrite "sqrt_1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_1 formula-decl nil sqrt "reals/") (sqrt_le formula-decl nil sqrt "reals/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (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 "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (> const-decl "bool" reals nil)) shostak)) (asin_sqrt_half 0 (asin_sqrt_half-2 nil 3322498751 ("" (expand "asin") (("" (typepred "sqrt(1/2)") (("" (lemma "sqrt_lt" ("nny" "1/2" "nnz" "1")) (("" (rewrite "sqrt_1" -1) (("" (assert) (("" (rewrite "sq_rew" 1) (("" (rewrite "div_simp" 1) (("" (rewrite "pi_value") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((> const-decl "bool" reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal 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) (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) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_1 formula-decl nil sqrt "reals/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_rew formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (pi_value formula-decl nil atan nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_simp formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_lt formula-decl nil sqrt "reals/") (asin const-decl "real_abs_le_pi2" asin nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/")) nil)) (asin_1 0 (asin_1-1 nil 3262276037 ("" (expand "asin") (("" (propax) nil nil)) nil) ((asin const-decl "real_abs_le_pi2" asin nil)) shostak)) (asin_neg_TCC1 0 (asin_neg_TCC1-1 nil 3262231915 ("" (grind) nil nil) nil shostak)) (asin_neg 0 (asin_neg-1 nil 3262232085 ("" (skolem 1 ("x")) (("" (expand "asin") (("" (case "x = -1") (("1" (assert) nil nil) ("2" (case "x = 1") (("1" (assert) nil nil) ("2" (case "-1 < x & x < 1") (("1" (flatten -1) (("1" (assert) (("1" (lemma "atan_neg" ("x" "x / sqrt(1 - -x * -x)")) (("1" (assert) nil nil) ("2" (hide 4) (("2" (lemma "asin_TCC3" ("x" "x")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (assert) (("2" (typepred "x") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (asin const-decl "real_abs_le_pi2" asin 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) (nnreal 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, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (atan_neg formula-decl nil atan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (< const-decl "bool" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (minus_odd_is_odd application-judgement "odd_int" integers 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) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil)) shostak)) (asin_minus1 0 (asin_minus1-1 nil 3262276084 ("" (expand "asin") (("" (propax) nil nil)) nil) ((asin const-decl "real_abs_le_pi2" asin nil)) shostak)) (asin_minus_sqrt_half_TCC1 0 (asin_minus_sqrt_half_TCC1-1 nil 3263821369 ("" (expand "abs") (("" (typepred "sqrt(1/2)") (("" (assert) (("" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1")) (("" (rewrite "sqrt_1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_1 formula-decl nil sqrt "reals/") (sqrt_le formula-decl nil sqrt "reals/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (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 "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (> const-decl "bool" reals nil)) shostak)) (asin_minus_sqrt_half 0 (asin_minus_sqrt_half-1 nil 3263819795 ("" (lemma "asin_sqrt_half") (("" (rewrite "asin_neg" 1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (lemma "sqrt_le" ("nny" "1/2" "nnz" "1")) (("2" (rewrite "sqrt_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (asin_neg formula-decl nil asin nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (asin_sqrt_half formula-decl nil asin nil)) shostak)) (asin_strict_increasing 0 (asin_strict_increasing-3 nil 3322498826 ("" (lemma "atan_strict_increasing") (("" (expand "strict_increasing?") (("" (skolem 1 ("x" "y")) (("" (flatten) (("" (expand "asin") (("" (case "abs(x) <= 1") (("1" (case "abs(y) <= 1") (("1" (case "FORALL (z:real): abs(z) < 1 => 0 < sqrt(1-z*z)") (("1" (expand "<=" (-2 -3)) (("1" (split -3) (("1" (inst-cp -2 "x") (("1" (assert) (("1" (case "y = -1") (("1" (hide 1) (("1" (lemma "trichotomy" ("x" "x")) (("1" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (expand "abs" -3) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "y < 1") (("1" (assert) (("1" (case "x= -1") (("1" (assert) nil nil) ("2" (expand "abs" -3) (("2" (assert) (("2" (inst -3 "y") (("2" (split -5) (("1" (assert) (("1" (inst - "x / sqrt(1 - x * x)" "y / sqrt(1 - y * y)") (("1" (split -6) (("1" (propax) nil nil) ("2" (hide 4) (("2" (lemma "div_mult_pos_lt1" ("z" "x" "py" "sqrt(1-x*x)" "x" "y / sqrt(1 - y * y)")) (("2" (replace -1 1) (("2" (lemma "div_mult_pos_lt2" ("x" "x" "z" "y*sqrt(1-x*x)" "py" "sqrt(1-y*y)")) (("1" (replace -1 1) (("1" (hide -1 -2) (("1" (lemma "trichotomy" ("x" "x")) (("1" (split -1) (("1" (lemma "sq_lt" ("nna" "x * sqrt(1 - y * y)" "nnb" "y * sqrt(1 - x * x)")) (("1" (replace -1 1 rl) (("1" (rewrite "sq_times" 1) (("1" (rewrite "sq_times" 1) (("1" (expand "sq" 1) (("1" (lemma "sq_lt" ("nna" "x" "nnb" "y")) (("1" (expand "sq" -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_times_posreal_is_posreal" ("px" "y" "py" "sqrt(1-x*x)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "x" "py" "sqrt(1-y*y)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "sqrt_1" 1) (("2" (assert) nil nil)) nil)) nil) ("3" (case "y < 0") (("1" (lemma "both_sides_times_neg_lt1" ("nz" "-1" "y" "x * sqrt(1 - y * y)" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28