| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 234 kB |
|
Quelle acos.prfSprache: Lisp |
|||||||||||||||
|
(acos (nnreal_le_pi_TCC1 0 (nnreal_le_pi_TCC1-1 nil 3262275870 ("" (assert) nil nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (acos_TCC1 0 (acos_TCC1-1 nil 3262275879 ("" (skolem 1 ("x")) (("" (typepred "asin(x)") (("" (expand "abs" -1) (("" (case "asin(x) < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((asin const-decl "real_abs_le_pi2" asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi const-decl "posreal" atan 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) (/ 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) (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_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" 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_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil)) shostak)) (acos_neg_TCC1 0 (acos_neg_TCC1-1 nil 3262871574 ("" (grind) nil nil) nil shostak)) (acos_neg 0 (acos_neg-1 nil 3262871521 ("" (skolem 1 ("x")) (("" (expand "acos") (("" (rewrite "asin_neg") (("" (assert) nil nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (acos const-decl "nnreal_le_pi" acos nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (asin_neg formula-decl nil asin nil)) shostak)) (acos_0 0 (acos_0-1 nil 3262276429 ("" (expand "acos") (("" (rewrite "asin_0") (("" (assert) nil nil)) nil)) nil) ((asin_0 formula-decl nil asin nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (acos const-decl "nnreal_le_pi" acos nil)) shostak)) (acos_sqrt_half_TCC1 0 (acos_sqrt_half_TCC1-1 nil 3263920337 ("" (expand "abs") (("" (typepred "sqrt(1/2)") (("" (assert) (("" (lemma "sq_le" ("nna" "sqrt(1/2)" "nnb" "1")) (("" (rewrite "sq_sqrt") (("" (expand "sq" -1) (("" (propax) nil 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) (sq_sqrt formula-decl nil sqrt "reals/") (sq const-decl "nonneg_real" sq "reals/") (sq_le formula-decl nil sq "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)) (acos_sqrt_half 0 (acos_sqrt_half-1 nil 3263920536 ("" (expand "acos") (("" (rewrite "asin_sqrt_half") (("" (assert) nil nil)) nil)) nil) ((asin_sqrt_half formula-decl nil asin nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (acos const-decl "nnreal_le_pi" acos nil)) shostak)) (acos_1 0 (acos_1-1 nil 3262276459 ("" (expand "acos") (("" (rewrite "asin_1") (("" (assert) nil nil)) nil)) nil) ((asin_1 formula-decl nil asin nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (acos const-decl "nnreal_le_pi" acos nil)) shostak)) (acos_minus1 0 (acos_minus1-1 nil 3262276496 ("" (expand "acos") (("" (rewrite "asin_minus1") (("" (assert) nil nil)) nil)) nil) ((asin_minus1 formula-decl nil asin 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_minus_real_is_real application-judgement "real" reals nil) (acos const-decl "nnreal_le_pi" acos nil)) shostak)) (acos_minus_sqrt_half_TCC1 0 (acos_minus_sqrt_half_TCC1-1 nil 3263920463 ("" (lemma "acos_sqrt_half_TCC1") (("" (assert) (("" (mult-by 1 "-1" -) (("" (assert) nil nil)) nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_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" 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields 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) (both_sides_times_neg_le1 formula-decl nil real_props nil) (acos_sqrt_half_TCC1 subtype-tcc nil acos nil)) shostak)) (acos_minus_sqrt_half 0 (acos_minus_sqrt_half-1 nil 3263920585 ("" (expand "acos") (("" (rewrite "asin_minus_sqrt_half") (("" (assert) nil nil)) nil)) nil) ((asin_minus_sqrt_half formula-decl nil asin nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_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_minus_real_is_real application-judgement "real" reals nil) (acos const-decl "nnreal_le_pi" acos nil) (sqrt_pos application-judgement "posreal" sqrt "reals/")) shostak)) (acos_strict_decreasing 0 (acos_strict_decreasing-1 nil 3262276758 ("" (expand "strict_decreasing?") (("" (skolem 1 ("x" "y")) (("" (flatten) (("" (expand "acos") (("" (lemma "asin_strict_increasing") (("" (expand "strict_increasing?") (("" (inst - "x" "y") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((acos const-decl "nnreal_le_pi" acos nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (asin_strict_increasing formula-decl nil asin nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/")) shostak)) (acos_bij 0 (acos_bij-1 nil 3262277267 ("" (lemma "asin_bij") (("" (expand "bijective?") (("" (expand "injective?") (("" (expand "surjective?") (("" (expand "acos") (("" (flatten) (("" (split 1) (("1" (skolem 1 ("x" "y")) (("1" (inst -1 "x" "y") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (skolem 1 ("y")) (("2" (inst - "pi/2-y") (("1" (skolem - ("x")) (("1" (inst + "x") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "y") (("2" (expand "abs") (("2" (case "pi/2-y<0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (surjective? const-decl "bool" functions 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) (real_minus_real_is_real application-judgement "real" 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 const-decl "posreal" atan nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (real_times_real_is_real application-judgement "real" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (acos const-decl "nnreal_le_pi" acos nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (injective? const-decl "bool" functions nil) (asin_bij formula-decl nil asin nil)) shostak)) (acos_sum_TCC1 0 (acos_sum_TCC1-1 nil 3263920917 ("" (skosimp*) (("" (typepred "nnx!1") (("" (assert) nil nil)) nil)) nil) ((<= const-decl "bool" reals 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) (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) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (acos_sum_TCC2 0 (acos_sum_TCC2-1 nil 3263920948 ("" (skosimp*) (("" (typepred "nny!1") (("" (lemma "sq_le" ("nna" "nny!1" "nnb" "1")) (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals 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) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq const-decl "nonneg_real" 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) (real_minus_real_is_real application-judgement "real" reals nil) (sq_le formula-decl nil sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil)) shostak)) (acos_sum_TCC3 0 (acos_sum_TCC3-1 nil 3263921002 ("" (skosimp*) (("" (typepred "nnx!1") (("" (typepred "nny!1") (("" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1")) (("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1")) (("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1")) (("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1")) (("" (rewrite "sq_0") (("" (rewrite "sq_1") (("" (expand ">=") (("" (flatten) (("" (replace -9) (("" (replace -9) (("" (replace -9) (("" (replace -9) (("" (case "0 <= 1 - sq(nny!1)") (("1" (case "0 <= 1 - sq(nnx!1)") (("1" (lemma "sqrt_le" ("nny" "1 - sq(nny!1)" "nnz" "1")) (("1" (lemma "sqrt_le" ("nny" "1 - sq(nnx!1)" "nnz" "1")) (("1" (assert) (("1" (rewrite "sqrt_1") (("1" (typepred "sqrt(1 - sq(nnx!1)) ") (("1" (typepred "sqrt(1 - sq(nny!1)) ") (("1" (hide -2 -4) (("1" (lemma "nnreal_times_nnreal_is_nnreal" ("nnx" "nnx!1" "nny" "nny!1")) (("1" (lemma "nnreal_times_nnreal_is_nnreal" ("nnx" "sqrt(1 - sq(nnx!1))" "nny" "sqrt(1 - sq(nny!1))")) (("1" (lemma "le_times_le_pos" ("nnx" "sqrt(1 - sq(nny!1))" "y" "1" "nnz" "sqrt(1 - sq(nnx!1))" "w" "1")) (("1" (assert) (("1" (lemma "le_times_le_pos" ("nnx" "nnx!1" "y" "1" "nnz" "nny!1" "w" "1")) (("1" (assert) (("1" (lemma "le_minus_le" ("x" "nnx!1 * nny!1" "y" "1" "w" "0" "z" "(sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1)))")) (("1" (lemma "le_minus_le" ("y" "nnx!1 * nny!1" "x" "0" "z" "1" "w" "(sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1)))")) (("1" (expand ">=") (("1" (replace -3) (("1" (replace -4) (("1" (replace -5) (("1" (replace -6) (("1" (expand "abs" 1) (("1" (case "nnx!1 * nny!1 - (sqrt(1 - sq(nny!1))) * (sqrt(1 - sq(nnx!1))) < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq_le formula-decl nil sq "reals/") (sq_0 formula-decl nil sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_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) (sq const-decl "nonneg_real" sq "reals/") (sqrt_le formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_1 formula-decl nil sqrt "reals/") (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (le_times_le_pos formula-decl nil real_props nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sq_1 formula-decl nil sq "reals/")) shostak)) (acos_sum 0 (acos_sum-1 nil 3263922185 ("" (skosimp*) (("" (typepred "nnx!1") (("" (typepred "nny!1") (("" (expand ">=") (("" (lemma "sq_le" ("nna" "0" "nnb" "nnx!1")) (("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1")) (("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1")) (("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1")) (("" (rewrite "sq_0") (("" (rewrite "sq_1") (("" (simplify -1) (("" (simplify -2) (("" (flatten) (("" (replace -7) (("" (replace -8) (("" (expand "<=" -8) (("" (split -8) (("1" (expand "<=" -7) (("1" (split -7) (("1" (expand "<=" -8) (("1" (split -8) (("1" (expand "<=" -8) (("1" (split -8) (("1" (expand "acos" 1) (("1" (lemma "div_cancel1" ("x" "pi" "n0z" "2")) (("1" (replace -1) (("1" (hide -1) (("1" (hide -5 -6 -7 -8) (("1" (lemma "sq_lt" ("nna" "0" "nnb" "nnx!1")) (("1" (lemma "sq_lt" ("nna" "0" "nnb" "nny!1")) (("1" (lemma "sq_lt" ("nnb" "1" "nna" "nnx!1")) (("1" (lemma "sq_lt" ("nnb" "1" "nna" "nny!1")) (("1" (rewrite "sq_0") (("1" (rewrite "sq_1") (("1" (replace -5) (("1" (replace -6) (("1" (replace -7) (("1" (replace -8) (("1" (simplify) (("1" (case "0 < 1-sq(nnx!1)") (("1" (case "0 < 1-sq(nny!1)") (("1" (case "1-sq(nnx!1)<1") (("1" (case "1-sq(nny!1)<1") (("1" (lemma "sqrt_lt" ("nny" "0" "nnz" "1-sq(nnx!1)")) (("1" (lemma "sqrt_lt" ("nny" "0" "nnz" "1-sq(nny!1)")) (("1" (lemma "sqrt_lt" ("nnz" "1" "nny" "1-sq(nnx!1)")) (("1" (lemma "sqrt_lt" ("nnz" "1" "nny" "1-sq(nny!1)")) (("1" (replace -5) (("1" (replace -6) (("1" (replace -7) (("1" (replace -8) (("1" (rewrite "sqrt_1") (("1" (rewrite "sqrt_0") (("1" (simplify) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "nnx!1" "py" "nny!1")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "sqrt(1 - sq(nny!1))" "py" "sqrt(1 - sq(nnx!1))")) (("1" (lemma "lt_times_lt_pos1" ("px" "nnx!1" "y" "1" "nnz" "nny!1" "w" "1")) (("1" (lemma "lt_times_lt_pos1" ("px" "sqrt(1 - sq(nny!1))" "y" "1" "nnz" "sqrt(1 - sq(nnx!1))" "w" "1")) (("1" (assert) (("1" (lemma "lt_minus_lt1" ("x" "nnx!1 * nny!1" "y" "1" "w" "0" "z" "sqrt(1 - sq(nny!1)) * sqrt(1 - sq(nnx!1))")) (("1" (lemma "lt_minus_lt1" ("x" "0" "y" "nnx!1 * nny!1" "w" "sqrt(1 - sq(nny!1)) * sqrt(1 - sq(nnx!1))" "z" "1")) (("1" (replace -3) (("1" (expand ">" -5) (("1" (replace -5) (("1" (split -1) (("1" (split -2) (("1" (simplify (-1 -2)) (("1" (expand "asin") (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (lemma "sq_sqrt" ("x" "1-sq(nnx!1)")) (("1" (lemma "sq_sqrt" ("x" "1-sq(nny!1)")) (("1" (assert) (("1" (name-replace "SX" "sqrt(1 - sq(nnx!1))") (("1" (name-replace "SY" "sqrt(1 - sq(nny!1))") (("1" (rewrite "sq_rew" 1) (("1" (case "1 - sq(nnx!1) * nny!1 * nny!1 - sq(SX) * SY * SY = 1-sq(nnx!1)*sq(nny!1) - sq(SX)*sq(SY)") (("1" (replace -1 1) (("1" (simplify 1) (("1" (hide -1) (("1" (lemma "trich_lt" ("x" "(nnx!1 / SX)*(nny!1 / SY)" "y" "1")) (("1" (case-replace "(1 - sq(SX) * sq(SY) - sq(nnx!1) * sq(nny!1) + 2 * (SX * SY * nnx!1 * nny!1)) = sq(SY*nnx!1+SX*nny!1)") (("1" (rewrite "sqrt_sq" 1) (("1" (hide -1) (("1" (lemma "atan_plus" ("x" "nnx!1/SX" "y" "nny!1/SY")) (("1" (split -2) (("1" (assert) (("1" (rewrite "div_times" -1) (("1" (rewrite "div_mult_pos_lt1" -1) (("1" (rewrite "add_div" -2) (("1" (lemma "minus_div1" ("x" "1" "n0x" "1" "y" "nnx!1 * nny!1" "n0y" "SX * SY")) (("1" (replace -1 -3) (("1" (name-replace "DRL5" "SX * SY") (("1" (rewrite "div_div1" -3) (("1" (rewrite " div_cancel2" -3) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "nnx!1 * SY + nny!1 * SX" "py" "DRL5 - nnx!1 * nny!1")) (("1" (lemma "atan_inv" ("px" "((nnx!1 * SY + nny!1 * SX) / (DRL5 - nnx!1 * nny!1))")) (("1" (rewrite "div_div1" -1) (("1" (name-replace "DRL6" "nnx!1 * SY + nny!1 * SX") (("1" (lemma "atan_neg" ("x" "(DRL5 - nnx!1 * nny!1) / DRL6")) (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "DRL6") (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nnx!1" "py" "SY")) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nny!1" "py" "SX")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (lemma "posreal_times_posreal_is_posreal" ("px" "nnx!1" "py" "SY")) (("3" (lemma "posreal_times_posreal_is_posreal" ("px" "nny!1" "py" "SX")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -2) (("2" (rewrite "div_times" -1) (("2" (lemma "div_cancel3" ("x" "nnx!1*nny!1" "y" "1" "n0z" "SX*SY")) (("2" (replace -2 -1) (("2" (flatten) (("2" (replace -1 1) (("2" (assert) (("2" (assert) (("2" (case-replace "(SX * SY - SY * SX)=0") (("1" (rewrite "atan_0") (("1" (lemma "atan_inv" ("px" "nnx!1/SX")) (("1" (rewrite "div_div1" -1) (("1" (lemma "cross_mult" ("x" "SX" "n0x" "nnx!1" "y" "nny!1" "n0y" "SY")) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "nnx!1" "py" "SX")) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "posreal_div_posreal_is_posreal" ("px" "nny!1" "py" "SY")) (("3" (assert) (("3" (rewrite "div_times" -2) (("3" (rewrite "add_div" -3) (("3" (lemma "minus_div1" ("x" "1" "n0x" "1" "y" "nnx!1 * nny!1" "n0y" "SX * SY")) (("3" (replace -1 -4) (("3" (name-replace "DRL5" "SX * SY") (("3" (rewrite "div_div1" -4) (("3" (rewrite " div_cancel2" -4) (("3" (rewrite "div_mult_pos_lt2" -3) (("3" (lemma "both_sides_div_neg_lt1" ("nz" "DRL5 - nnx!1 * nny!1" "y" "0" "x" "nnx!1 * SY + nny!1 * SX")) (("1" (lemma "atan_inv_neg" ("nx" "(nnx!1 * SY + nny!1 * SX) / (DRL5 - nnx!1 * nny!1)")) (("1" (rewrite "div_div1" -1) (("1" (lemma "atan_neg" ("x" "(DRL5 - nnx!1 * nny!1) / (nnx!1 * SY + nny!1 * SX)")) (("1" (assert) nil nil) ("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nny!1" "py" "SX")) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nnx!1" "py" "SY")) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nnx!1" "py" "SY")) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nny!1" "py" "SX")) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nny!1" "py" "SX")) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nnx!1" "py" "SY")) (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "SX") (("2" (expand "SY") (("2" (rewrite "sq_sqrt") (("2" (rewrite "sq_sqrt") (("2" (rewrite "sq_plus") (("2" (assert) (("2" (rewrite "sq_times") (("2" (rewrite "sq_times") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "sq" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "acos_0") (("2" (rewrite "sq_0") (("2" (rewrite "sqrt_1") (("2" (simplify 1) (("2" (hide -1) (("2" (lemma "acos_neg" ("x" "sqrt(1 - sq(nnx!1))")) (("1" (replace -1 1) (("1" (hide -1) (("1" (expand "acos") (("1" (lemma "div_cancel1" ("x" "pi" "n0z" "2")) (("1" (replace -1) (("1" (lemma "asin_pos_restrict" ("px" "nnx!1")) (("1" (replace -1 1) (("1" (hide -1) (("1" (expand "asin" 1) (("1" (lemma "sq_lt" ("nna" "0" "nnb" "nnx!1")) (("1" (rewrite "sq_0") (("1" (case "1 - sq(nnx!1) < 1") (("1" (lemma "sqrt_lt" ("nny" "1 - sq(nnx!1)" "nnz" "1")) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (simplify 1) (("1" (rewrite "sqrt_sq" 1) (("1" (rewrite "sqrt_1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (hide 2) (("2" (case "1 - sq(nnx!1) <= 1") (("1" (lemma "sqrt_le" ("nny" "1 - sq(nnx!1)" "nnz" "1")) (("1" (rewrite "sqrt_1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "sq_0") (("2" (rewrite "sqrt_1") (("2" (rewrite "acos_0") (("2" (simplify 1) (("2" (lemma "acos_neg" ("x" "sqrt(1 - sq(nny!1))")) (("1" (replace -1) (("1" (hide -1) (("1" (expand "acos") (("1" (lemma "div_cancel1" ("x" "pi" "n0z" "2")) (("1" (replace -1) (("1" (expand "<=" -9) (("1" (split -9) (("1" (lemma "asin_pos_restrict" ("px" "nny!1")) (("1" (replace -1 1) (("1" (expand "asin" 1) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (simplify 1) (("1" (rewrite "sqrt_sq") (("1" (lemma "sq_lt" ("nna" "nny!1" "nnb" "1")) (("1" (rewrite "sq_1") (("1" (case "1 - sq(nny!1) < 1") (("1" (lemma "sqrt_lt" ("nny" "1 - sq(nny!1)" "nnz" "1")) (("1" (rewrite "sqrt_1") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "sq_lt" ("nna" "0" "nnb" "nny!1")) (("2" (rewrite "sq_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (propax) nil nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "asin_0") (("2" (rewrite "sq_0") (("2" (rewrite "sqrt_1") (("2" (rewrite "asin_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (hide 2) (("2" (lemma "sq_le" ("nna" "0" "nnb" "nny!1")) (("2" (rewrite "sq_0") (("2" (lemma "sqrt_le" ("nny" "1-sq(nny!1)" "nnz" "1")) (("2" (rewrite "sqrt_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "acos_1") (("2" (rewrite "sq_1") (("2" (rewrite "sqrt_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "sq_1") (("2" (rewrite "sqrt_0") (("2" (rewrite "acos_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) ((<= const-decl "bool" reals 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) (sq_1 formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (acos_1 formula-decl nil acos nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (asin_0 formula-decl nil asin nil) (asin_1 formula-decl nil asin nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (acos_neg formula-decl nil acos nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (asin_pos_restrict formula-decl nil asin nil) (sqrt_le formula-decl nil sqrt "reals/") (acos_0 formula-decl nil acos nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (acos const-decl "nnreal_le_pi" acos nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (< const-decl "bool" reals 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/") (sqrt_lt formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sqrt_1 formula-decl nil sqrt "reals/") (real_plus_real_is_real application-judgement "real" reals 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/") (lt_minus_lt1 formula-decl nil real_props nil) (asin const-decl "real_abs_le_pi2" asin nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_times formula-decl nil real_props nil) (add_div formula-decl nil real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (div_div1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (atan_neg formula-decl nil atan nil) (minus_real_is_real application-judgement "real" reals nil) (atan_inv formula-decl nil atan nil) (div_cancel2 formula-decl nil real_props nil) (minus_div1 formula-decl nil real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (cross_mult formula-decl nil real_props nil) (atan_0 formula-decl nil atan nil) (both_sides_div_neg_lt1 formula-decl nil real_props nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (atan_inv_neg formula-decl nil atan nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (atan_plus formula-decl nil atan nil) (sqrt_sq formula-decl nil sqrt "reals/") (SX skolem-const-decl "{nnz: nnreal | nnz * nnz = 1 - sq(nnx!1)}" acos nil) (sq_plus formula-decl nil sq "reals/") (sq_times formula-decl nil sq "reals/") (SY skolem-const-decl "{nnz: nnreal | nnz * nnz = 1 - sq(nny!1)}" acos nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (trich_lt formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sq_sqrt formula-decl nil sqrt "reals/") (sq_rew formula-decl nil sq "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (sqrt_0 formula-decl nil sqrt "reals/") (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) (sq_lt formula-decl nil sq "reals/") (pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (div_cancel1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_0 formula-decl nil sq "reals/") (sq_le formula-decl nil sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil)) shostak)) (acos_derivable_TCC1 0 (acos_derivable_TCC1-1 nil 3262873061 ("" (skosimp*) (("" (typepred "x!1") (("" (expand "abs") (("" (case "x!1<0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_abs_lt1 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) (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)) shostak)) (acos_derivable_TCC2 0 (acos_derivable_TCC2-1 nil 3262873116 ("" (lemma deriv_domain_open) (("" (inst - "-1" "1") (("" (expand "deriv_domain?") (("" (propax) nil nil)) nil)) nil)) 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) (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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (deriv_domain_open formula-decl nil deriv_domain "analysis/")) shostak)) (acos_derivable_TCC3 0 (acos_derivable_TCC3-1 nil 3262873369 ("" (expand "not_one_element?") (("" (skosimp*) (("" (case "x!1=0") (("1" (inst + "1/2") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst + "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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_lt1 nonempty-type-eq-decl nil asin nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (acos_derivable 0 (acos_derivable-3 nil 3425656783 ("" (skolem 1 ("z")) (("" (expand "acos") (("" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "pi/2")) (("" (lemma "asin_derivable_fun") (("" (expand "const_fun") (("" (lemma "diff_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): pi / 2" "f2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (assert) (("" (expand "-" -1) (("" (expand "derivable?" -1) (("" (inst - "z") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((acos const-decl "nnreal_le_pi" acos nil) (asin_derivable_fun formula-decl nil asin nil) (real_minus_real_is_real application-judgement "real" reals nil) (derivable? const-decl "bool" derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (<= const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (asin const-decl "real_abs_le_pi2" asin nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (const_derivable_fun formula-decl nil derivatives "analysis/") (/= 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 const-decl "posreal" atan 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_lt1 nonempty-type-eq-decl nil asin nil)) nil) (acos_derivable-2 nil 3352188947 ("" (skolem 1 ("z")) (("" (expand "acos") (("" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "pi/2")) (("" (lemma "asin_derivable2") (("" (expand "const_fun") (("" (lemma "diff_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): pi / 2" "f2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (assert) (("" (expand "-" -1) (("" (expand "derivable?" -1) (("" (inst - "z") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((diff_derivable_fun formula-decl nil derivatives "analysis/") (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (asin const-decl "real_abs_le_pi2" asin nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_derivable_fun formula-decl nil derivatives "analysis/") (pi const-decl "posreal" atan nil) (real_abs_lt1 nonempty-type-eq-decl nil asin nil)) nil) (acos_derivable-1 nil 3262871716 ("" (skolem 1 ("z")) (("" (expand "acos") (("" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "pi/2")) (("" (lemma "asin_derivable2") (("" (expand "const_fun") (("" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt1): pi / 2" "f2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (assert) (("" (expand "-" -1) (("" (expand "derivable?" -1) (("" (inst - "z") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((asin const-decl "real_abs_le_pi2" asin nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (diff_derivable_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_derivable_fun formula-decl nil derivatives "analysis/") (pi const-decl "posreal" atan nil) (real_abs_lt1 nonempty-type-eq-decl nil asin nil)) shostak)) (acos_derivable_fun 0 (acos_derivable_fun-1 nil 3425654686 ("" (lemma "acos_derivable") (("" (expand "derivable?" 1) (("" (propax) nil nil)) nil)) nil) ((derivable? const-decl "bool" derivatives "analysis/") (acos_derivable formula-decl nil acos nil)) nil)) (deriv_acos_fun_TCC1 0 (deriv_acos_fun_TCC1-2 nil 3425656832 ("" (lemma "acos_derivable_fun") (("" (propax) nil nil)) nil) ((acos_derivable_fun formula-decl nil acos nil)) nil) (deriv_acos_fun_TCC1-1 nil 3262873446 ("" (lemma "acos_derivable2") (("" (propax) nil nil)) nil) nil shostak)) (deriv_acos_fun_TCC2 0 (deriv_acos_fun_TCC2-2 nil 3425656848 ("" (lemma "asin_derivable_fun") (("" (propax) nil nil)) nil) ((asin_derivable_fun formula-decl nil asin nil)) nil) (deriv_acos_fun_TCC2-1 nil 3262873481 ("" (lemma "asin_derivable2") (("" (propax) nil nil)) nil) nil shostak)) (deriv_acos_fun 0 (deriv_acos_fun-3 nil 3425656808 ("" (lemma "asin_derivable_fun") (("" (expand "acos" 1) (("" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "pi/2")) (("" (lemma "deriv_const_fun[real_abs_lt1]" ("b" "pi/2")) (("" (expand "const_fun") (("" (lemma "diff_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): pi / 2" "f2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (assert) (("" (expand "-") (("" (lemma "deriv_diff_fun[real_abs_lt1]" ("ff1" "LAMBDA (x: real_abs_lt1): pi / 2" "ff2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (expand "-") (("" (replace -3 -1) (("" (simplify -1) (("" (replace -1 1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((acos const-decl "nnreal_le_pi" acos nil) (deriv_const_fun formula-decl nil derivatives "analysis/") (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (deriv_diff_fun formula-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (<= const-decl "bool" reals nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (asin const-decl "real_abs_le_pi2" asin nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (const_derivable_fun formula-decl nil derivatives "analysis/") (/= 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 const-decl "posreal" atan 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_lt1 nonempty-type-eq-decl nil asin nil) (asin_derivable_fun formula-decl nil asin nil)) nil) (deriv_acos_fun-2 nil 3352188982 ("" (lemma "asin_derivable2") (("" (expand "acos" 1) (("" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "pi/2")) (("" (lemma "deriv_const_fun[real_abs_lt1]" ("b" "pi/2")) (("" (expand "const_fun") (("" (lemma "diff_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): pi / 2" "f2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (assert) (("" (expand "-") (("" (lemma "deriv_diff_fun[real_abs_lt1]" ("ff1" "LAMBDA (x: real_abs_lt1): pi / 2" "ff2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (expand "-") (("" (replace -3 -1) (("" (simplify -1) (("" (replace -1 1) (("" (assert) (("" (apply-extensionality 1 :hide? t) (("" (expand "deriv") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_lt1 nonempty-type-eq-decl nil asin nil) (pi const-decl "posreal" atan nil) (const_derivable_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv const-decl "[T -> real]" derivatives "analysis/") (asin const-decl "real_abs_le_pi2" asin nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (diff_derivable_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/")) nil) (deriv_acos_fun-1 nil 3262871928 ("" (lemma "asin_derivable2") (("" (expand "acos" 1) (("" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "pi/2")) (("" (lemma "deriv_const_fun[real_abs_lt1]" ("b" "pi/2")) (("" (expand "const_fun") (("" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt1): pi / 2" "f2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (assert) (("" (expand "-") (("" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: real_abs_lt1): pi / 2" "ff2" "LAMBDA (x: real_abs_lt1): asin(x)")) (("" (expand "-") (("" (replace -3 -1) (("" (simplify -1) (("" (replace -1 1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv_const_fun formula-decl nil derivatives "analysis/") (asin const-decl "real_abs_le_pi2" asin nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (diff_derivable_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_derivable_fun formula-decl nil derivatives "analysis/") (pi const-decl "posreal" atan nil) (real_abs_lt1 nonempty-type-eq-decl nil asin nil)) shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.153Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26