| 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 1 MB |
|
Quellcode-Bibliothek asin.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(asin (real_abs_le_pi2_TCC1 0 (real_abs_le_pi2_TCC1-1 nil 3323022558 ("" (typepred "pi") (("" (rewrite "abs_0") (("" (assert) nil nil)) nil)) 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_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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (pi const-decl "posreal" atan nil)) nil)) (noa_abs_lt1 0 (noa_abs_lt1-1 nil 3477835992 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "1/4") (("" (inst + "1/2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_abs_lt1 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) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (noa_nnreal_lt1 0 (noa_nnreal_lt1-1 nil 3477836409 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "x!1/2") (("" (inst + "1/2") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals 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) (nnreal 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) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (deriv_domain_abs_lt1 0 (deriv_domain_abs_lt1-1 nil 3477836032 ("" (lemma "deriv_domain_open") (("" (inst - "-1" "1") 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)) (deriv_domain_nnreal_lt_1 0 (deriv_domain_nnreal_lt_1-1 nil 3477836434 ("" (lemma "deriv_domain_co") (("" (inst - "0" "1") (("" (assert) (("" (expand "deriv_domain?") (("" (skosimp*) (("" (inst - "e!1" "x!1") (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (real_plus_real_is_real application-judgement "real" reals nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (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) (bool nonempty-type-eq-decl nil booleans 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) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (deriv_domain_co formula-decl nil deriv_domain "analysis/")) shostak)) (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" (assert) nil nil) ("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) ((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) (sqrt_pos judgement-tcc nil sqrt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_lt_abs formula-decl nil sq "reals/") (minus_real_is_real application-judgement "real" reals nil) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan nil) (sq const-decl "nonneg_real" sq "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (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) (sq_nz_pos application-judgement "posreal" sq "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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 const-decl "posreal" atan 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) (pi const-decl "posreal" atan 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-1 nil 3262251992 ("" (skolem 1 ("nx")) (("" (typepred "nx") (("" (expand "abs") (("" (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_value" ("nx" "sqrt(1 - nx * nx) / nx")) (("1" (expand "pi" 1) (("1" (expand "atan" 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)) 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)) 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_value 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/") (atan const-decl "real_abs_lt_pi2" atan nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_div1 formula-decl nil real_props nil) (pi const-decl "posreal" atan nil) (minus_real_is_real application-judgement "real" reals 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)) shostak)) (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 3262251279 ("" (skolem 1 ("px")) (("" (typepred "px") (("" (expand "<=" -2) (("" (split -2) (("1" (hide -2) (("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" (expand "pi" 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)) 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) ((< 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) (asin const-decl "real_abs_le_pi2" asin nil) (sq_nz_pos judgement-tcc nil sq "reals/") (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil 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) (sqrt_lt formula-decl nil sqrt "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (atan_inv_value formula-decl nil atan 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/") (atan const-decl "real_abs_lt_pi2" atan nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi const-decl "posreal" atan nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_div1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (sqrt_0 formula-decl nil sqrt "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (real_lt_is_strict_total_order name-judgement "(strict_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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (atan_0 formula-decl nil atan nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (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-1 nil 3263819956 ("" (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/")) shostak)) (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-1 nil 3262232341 ("" (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" (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)")) (("2" (replace -1 1) (("2" (hide -1 -2) (("2" (lemma "trichotomy" ("x" "x")) (("2" (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)" "x" "y * sqrt(1 - x * x)")) (("1" (replace -1 1 rl) (("1" (lemma "sq_lt" ("nna" "(-1 *y) * sqrt(1 - x * x)" "nnb" "(-1*x) * sqrt(1 - y * y)")) (("1" (replace -1 1 rl) (("1" (rewrite "sq_times" 1) (("1" (expand "sq" 1 1) (("1" (rewrite "sq_times" 1) (("1" (rewrite "sq_times" 1) (("1" (expand "sq" 1) (("1" (hide -1 -2) (("1" (assert) (("1" (lemma "sq_lt" ("nna" "-1*y" "nnb" "-1*x")) (("1" (expand "sq" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_times_posreal_is_posreal" ("px" "-1*x" "py" "sqrt(1-y*y)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "-1*y" "py" "sqrt(1-x*x)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "nnreal_times_nnreal_is_nnreal" ("nnx" "y" "nny" "sqrt(1 - x * x)")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "x" "y" "0" "pz" "sqrt(1 - y * y)")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" -1) (("2" (lemma "trichotomy" ("x" "y")) (("2" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "trichotomy" ("x" "x")) (("2" (expand "abs" -2) (("2" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) (("3" (case "y <1") (("1" (assert) nil nil) ("2" (inst - "y") (("2" (split -4) (("1" (assert) nil nil) ("2" (typepred "atan(y / sqrt(1 - y * y))") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (hide 2) (("2" (hide -2 -3 -4 -5) (("2" (expand "abs") (("2" (lift-if) (("2" (ground) (("1" (mult-ineq -2 -2) (("1" (assert) nil nil)) nil) ("2" (mult-ineq -1 -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (assert) (("3" (hide 2) (("3" (hide -2 -3 -4 -5) (("3" (grind) (("1" (mult-ineq -2 -2) (("1" (assert) nil nil)) nil) ("2" (mult-ineq -1 -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "y") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "x") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strict_increasing? const-decl "bool" real_fun_preds "reals/") (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) (- 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) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (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) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (sqrt_1 formula-decl nil sqrt "reals/") (sq_lt formula-decl nil sq "reals/") (sq_times formula-decl nil sq "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sq_sqrt formula-decl nil sqrt "reals/") (sq const-decl "nonneg_real" sq "reals/") (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trichotomy formula-decl nil real_axioms nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (pi const-decl "posreal" atan nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (lt_times_lt_any1 formula-decl nil extra_real_props nil) (asin const-decl "real_abs_le_pi2" asin nil) (real_times_real_is_real application-judgement "real" reals nil) (atan_strict_increasing formula-decl nil atan nil)) shostak)) (asin_bij 0 (asin_bij-1 nil 3262233550 ("" (expand "bijective?") (("" (split 1) (("1" (expand "injective?") (("1" (skolem 1 ("x" "y")) (("1" (flatten) (("1" (lemma "asin_strict_increasing") (("1" (expand "strict_increasing?") (("1" (lemma "trich_lt" ("x" "x" "y" "y")) (("1" (split -1) (("1" (inst - "x" "y") (("1" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (inst - "y" "x") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "atan_bij") (("2" (expand "bijective?") (("2" (flatten) (("2" (hide -1) (("2" (expand "surjective?") (("2" (skosimp*) (("2" (expand "asin") (("2" (case "abs(y!1) <= pi/2") (("1" (expand "<=" -1) (("1" (split -1) (("1" (inst - "y!1") (("1" (skosimp*) (("1" (inst + "x!1/sqrt(1+x!1*x!1)") (("1" (lemma "sq_pos" ("a" "x!1")) (("1" (expand "sq" -1) (("1" (lemma "sqrt_pos" ("px" "1+x!1*x!1")) (("1" (case "abs(x!1 / sqrt(1 + x!1 * x!1)) < 1") (("1" (case "x!1 / sqrt(1 + x!1 * x!1) /= -1") (("1" (assert) (("1" (case "x!1 / sqrt(1 + x!1 * x!1) * (x!1 / sqrt(1 + x!1 * x!1)) = sq(x!1)/(1+sq(x!1))") (("1" (replace -1 1) (("1" (case "sqrt(1 - sq(x!1) / (1 + sq(x!1))) = 1/sqrt(1+x!1*x!1)") (("1" (replace -1 1) (("1" (lemma "div_div2" ("x" "x!1" "n0y" "sqrt(1 + x!1 * x!1)" "n0z" "1 / sqrt(1 + x!1 * x!1)")) (("1" (replace -1 1) (("1" (lemma "sq_sqrt" ("x" "sqrt(1 + x!1 * x!1)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "minus_div1" ("x" "1" "n0x" "1" "y" "sq(x!1)" "n0y" "1+sq(x!1)")) (("2" (replace -1 1) (("2" (simplify 1) (("2" (rewrite "sqrt_div" 1) (("2" (expand "sq" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "div_mult_pos_le1" ("z" "sq(x!1)" "py" "1+sq(x!1)" "x" "1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "sq_rew" 1) (("2" (rewrite "sq_rew" 1) (("2" (rewrite "sq_div" 1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide 2) (("2" (rewrite "abs_div" 1) (("2" (expand "abs" 1 2) (("2" (lemma "div_mult_pos_lt1" ("z" "abs(x!1)" "py" "sqrt(1 + x!1 * x!1)" "x" " 1")) (("1" (replace -1 1) (("1" (lemma "sq_lt" ("nna" "abs(x!1)" "nnb" "sqrt(1 + x!1 * x!1)")) (("1" (replace -1 1 rl) (("1" (rewrite "sq_sqrt" 1) (("1" (expand "abs" 1) (("1" (case "x!1<0") (("1" (assert) (("1" (expand "sq" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (lemma "sq_pos" ("a" "x!1")) (("2" (expand "sq" -1) (("2" (lemma "sqrt_pos" ("px" "1+x!1*x!1")) (("2" (case "abs(x!1) / sqrt(1 + x!1 * x!1) < 1") (("1" (cross-mult -1) (("1" (prop) (("1" (cross-mult 1) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "div_mult_pos_lt1" ("z" "abs(x!1)" "py" "sqrt(1 + x!1 * x!1)" "x" " 1")) (("1" (replace -1 1) (("1" (lemma "sq_lt" ("nna" "abs(x!1)" "nnb" "sqrt(1 + x!1 * x!1)")) (("1" (replace -1 1 rl) (("1" (rewrite "sq_sqrt" 1) (("1" (expand "abs" 1) (("1" (case "x!1<0") (("1" (assert) (("1" (expand "sq" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "sq_pos" ("a" "x!1")) (("3" (expand "sq" -1) (("3" (lemma "sqrt_pos" ("px" "1+x!1*x!1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pi" -1) (("2" (hide 2) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" -1) (("2" (case "y!1<0") (("1" (assert) (("1" (inst + "-1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (inst + "1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (typepred "y!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((asin_strict_increasing formula-decl nil asin 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) (trich_lt formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (injective? const-decl "bool" functions nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (pi const-decl "posreal" atan nil) (posreal 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (Integral const-decl "real" integral_def "analysis/") (atan_value const-decl "real" atan nil) (div_mult_pos_le2 formula-decl nil real_props nil) (sq_pos formula-decl nil sq "reals/") (sqrt_pos judgement-tcc nil sqrt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (sq_abs formula-decl nil sq "reals/") (sq_lt formula-decl nil sq "reals/") (div_mult_pos_lt1 formula-decl nil real_props nil) (abs_div formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (sq_sqrt formula-decl nil sqrt "reals/") (minus_div1 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqrt_1 formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (sqrt_div formula-decl nil sqrt "reals/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (sq_rew formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_div formula-decl nil sq "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (x!1 skolem-const-decl "real" 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) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (y!1 skolem-const-decl "real_abs_le_pi2" asin nil) (< const-decl "bool" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (asin const-decl "real_abs_le_pi2" asin nil) (real_times_real_is_real application-judgement "real" reals nil) (surjective? const-decl "bool" functions nil) (atan_bij formula-decl nil atan nil) (bijective? const-decl "bool" functions nil)) shostak)) (asin_diff_TCC1 0 (asin_diff_TCC1-1 nil 3263658797 ("" (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)) (asin_diff_TCC2 0 (asin_diff_TCC2-1 nil 3263658941 ("" (skosimp*) (("" (typepred "nny!1") (("" (lemma "sq_le" ("nna" "0" "nnb" "nny!1")) (("" (lemma "sq_le" ("nnb" "1" "nna" "nny!1")) (("" (rewrite "sq_0") (("" (rewrite "sq_1") (("" (assert) 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/") (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) (real_minus_real_is_real application-judgement "real" reals 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)) (asin_diff_TCC3 0 (asin_diff_TCC3-1 nil 3263820296 ("" (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" "nny!1")) (("" (lemma "sq_le" ("nnb" "1" "nna" "nnx!1")) (("" (rewrite "sq_0") (("" (rewrite "sq_1") (("" (replace -5 -3) (("" (simplify -3) (("" (replace -6 -2) (("" (replace -7 -4) (("" (replace -8 -1) (("" (simplify -1) (("" (simplify -2) (("" (flatten -4) (("" (typepred "sqrt(1-sq(nnx!1))") (("1" (typepred "sqrt(1-sq(nny!1))") (("1" (lemma "sqrt_le" ("nny" "1-sq(nnx!1)" "nnz" "1")) (("1" (lemma "sqrt_le" ("nny" "1-sq(nny!1)" "nnz" "1")) (("1" (assert) (("1" (rewrite "sqrt_1") (("1" (lemma "le_times_le_pos" ("nnx" "nnx!1" "y" "1" "nnz" "sqrt(1 - sq(nny!1))" "w" "1")) (("1" (lemma "le_times_le_pos" ("nnx" "nny!1" "y" "1" "nnz" "sqrt(1 - sq(nnx!1))" "w" "1")) (("1" (assert) (("1" (lemma "nnreal_times_nnreal_is_nnreal" ("nnx" "nnx!1" "nny" "(sqrt(1 - sq(nny!1)))")) (("1" (lemma "nnreal_times_nnreal_is_nnreal" ("nnx" "nny!1" "nny" "(sqrt(1 - sq(nnx!1)))")) (("1" (lemma "le_minus_le" ("z" "nny!1 * sqrt(1 - sq(nnx!1))" "w" "0" "x" "nnx!1 * sqrt(1 - sq(nny!1))" "y" "1")) (("1" (lemma "le_minus_le" ("w" "nny!1 * sqrt(1 - sq(nnx!1))" "z" "1" "y" "nnx!1 * sqrt(1 - sq(nny!1))" "x" "0")) (("1" (expand "abs" 1) (("1" (case "nnx!1 * (sqrt(1 - sq(nny!1))) - 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) ("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)) 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/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_times_le_pos formula-decl nil real_props nil) (sqrt_1 formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (sqrt_le formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (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/") (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)) (asin_diff 0 (asin_diff-1 nil 3263664160 ("" (skolem 1 ("nnx" "nny")) (("" (typepred "nnx") (("" (typepred "nny") (("" (expand ">=") (("" (expand "<=" (-4 -1)) (("" (split -4) (("1" (expand "<=" -4) (("1" (split -4) (("1" (split -3) (("1" (expand "<=" -4) (("1" (split -4) (("1" (expand "asin") (("1" (lemma "sq_lt" ("nna" "nnx" "nnb" "1")) (("1" (lemma "sq_lt" ("nna" "nny" "nnb" "1")) (("1" (rewrite "sq_1") (("1" (lemma "sq_lt" ("nnb" "nnx" "nna" "0")) (("1" (lemma "sq_lt" ("nnb" "nny" "nna" "0")) (("1" (rewrite "sq_0") (("1" (assert) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_sqrt" 1) (("1" (rewrite "sq_sqrt" 1) (("1" (simplify 1) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (lemma "sqrt_pos" ("px" "1-sq(nnx)")) (("1" (lemma "sqrt_pos" ("px" "1-sq(nny)")) (("1" (lemma "sqrt_lt" ("nny" "1-sq(nnx)" "nnz" "1")) (("1" (lemma "sqrt_lt" ("nny" "1-sq(nny)" "nnz" "1")) (("1" (rewrite "sqrt_1") (("1" (assert) (("1" (lemma "lt_times_lt_pos1" ("px" "nny" "y" "1" "nnz" "(sqrt(1 - sq(nnx)))" "w" "1")) (("1" (assert) (("1" (lemma "lt_times_lt_pos1" ("px" "nnx" "y" "1" "nnz" "(sqrt(1 - sq(nny)))" "w" "1")) (("1" (assert) (("1" (lemma "atan_minus" ("x" "nnx / sqrt(1 - sq(nnx))" "y" "nny / sqrt(1 - sq(nny))")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "nnx" "py" "sqrt(1-sq(nnx))")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "nny" "py" "sqrt(1-sq(nny))")) (("1" (assert) (("1" (flatten -3) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "nnx / sqrt(1 - sq(nnx))" "py" "nny / sqrt(1 - sq(nny))")) (("1" (assert) (("1" (hide -5) (("1" (name-replace "SQX" "sqrt(1 - sq(nnx))") (("1" (name-replace "SQY" "sqrt(1 - sq(nny))") (("1" (lemma "minus_div1" ("x" "nnx" "n0x" "SQX" "y" "nny" "n0y" "SQY")) (("1" (replace -1 -5) (("1" (rewrite "div_div2" -5) (("1" (lemma "div_cancel1" ("n0z" "SQX*SQY" "x" "nnx*nny")) (("1" (replace -1 -6) (("1" (case "sq(SQX * SQY + nnx * nny) = 1 - sq(nnx) - sq(nny) + sq(nnx) * nny * nny + sq(nny) * nnx * nnx + 2 * (SQX * SQY * nnx * nny)") (("1" (replace -1 1 rl) (("1" (rewrite "sqrt_sq" 1) nil nil)) nil) ("2" (hide 2) (("2" (expand "SQX" 1) (("2" (expand "SQY" 1) (("2" (expand "sq" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "SQX" "py" "SQY")) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "nnx / SQX" "py" "nny/SQY")) (("2" (lemma "lt_plus_lt1" ("x" "0" "y" "1" "z" "0" "w" "nnx / SQX * (nny / SQY)")) (("2" (name-replace "K1" "nnx / SQX * (nny / SQY)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "SQX" "py" "SQY")) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "asin_1") (("2" (rewrite "sq_1") (("2" (rewrite "sqrt_0") (("2" (simplify 1) (("2" (hide -1 -2) (("2" (lemma "asin_neg" ("x" "sqrt(1 - sq(nnx))")) (("1" (replace -1 1) (("1" (expand "asin") (("1" (hide -1) (("1" (lemma "sq_lt" ("nna" "0" "nnb" "nnx")) (("1" (lemma "sq_lt" ("nnb" "1" "nna" "nnx")) (("1" (rewrite "sq_0") (("1" (rewrite "sq_1") (("1" (assert) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_sqrt") (("1" (simplify 1) (("1" (lemma "sqrt_lt" ("nny" "1-sq(nnx)" "nnz" "1")) (("1" (rewrite "sqrt_1") (("1" (assert) (("1" (expand "pi" 1) (("1" (expand "atan" 1) (("1" (rewrite "sqrt_sq" 1) (("1" (lemma "sq_lt" ("nna" "0" "nnb" "nnx")) (("1" (rewrite "sq_0") (("1" (lemma "sqrt_pos" ("px" "1-sq(nnx)")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "sqrt(1-sq(nnx))" "py" "nnx")) (("1" (lemma "atan_inv_value" ("px" "sqrt(1 - sq(nnx)) / nnx")) (("1" (rewrite "div_div1" -1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "abs") (("2" (lemma "sqrt_le") (("2" (inst - "1-sq(nnx)" "1") (("2" (rewrite "sqrt_1") (("2" (lemma "sq_le" ("nna" "0" "nnb" "nnx")) (("2" (rewrite "sq_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "asin_0") (("2" (rewrite "sq_0") (("2" (rewrite "sqrt_1") (("2" (simplify 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "asin_0") (("2" (rewrite "sq_0") (("2" (rewrite "sqrt_1") (("2" (simplify 1) (("2" (lemma "asin_neg" ("x" "nny")) (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "sq_1") (("2" (rewrite "sqrt_0") (("2" (rewrite "asin_1") (("2" (lemma "sq_le" ("nna" "nny" "nnb" "1")) (("2" (expand "sq" -1 2) (("2" (expand "asin") (("2" (expand "<=" -4) (("2" (split -4) (("1" (assert) (("1" (typepred "sqrt(1 - sq(nny))") (("1" (assert) (("1" (split -6) (("1" (hide -5 -6 -7 -3 -2) (("1" (lemma "sq_lt" ("nna" "0" "nnb" "nny")) (("1" (lemma "sq_lt" ("nnb" "1" "nna" "nny")) (("1" (assert) (("1" (rewrite "sq_0") (("1" (rewrite "sq_1") (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_rew" 1) (("1" (rewrite "sq_sqrt" 1) (("1" (simplify 1) (("1" (rewrite "sqrt_sq" 1) (("1" (lemma "sqrt_lt") (("1" (inst - "1-sq(nny)" "1") (("1" (rewrite "sqrt_1" -1) (("1" (assert) (("1" (expand "pi") (("1" (expand "atan") (("1" (lemma "atan_inv_value" ("px" "(sqrt(1 - sq(nny))) / nny")) (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "sqrt_lt") (("2" (inst - "0" "1-sq(nny)") (("2" (rewrite "sqrt_0" -1) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "sqrt(1 - sq(nny))" "py" "nny")) (("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) ("2" (replace -1 * rl) (("2" (rewrite "sq_0" 1) (("2" (rewrite "sqrt_1") (("2" (rewrite "atan_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "sq_1") (("2" (simplify 1) (("2" (rewrite "sqrt_0") (("2" (rewrite "sqrt_1") (("2" (rewrite "atan_0") (("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) (asin_0 formula-decl nil asin nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (asin_neg formula-decl nil asin nil) (minus_real_is_real application-judgement "real" reals nil) (atan const-decl "real_abs_lt_pi2" atan nil) (div_div1 formula-decl nil real_props nil) (atan_inv_value formula-decl nil atan nil) (pi const-decl "posreal" atan nil) (sqrt_le formula-decl nil sqrt "reals/") (sq_le formula-decl nil sq "reals/") (sqrt_0 formula-decl nil sqrt "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (asin_1 formula-decl nil asin nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (asin const-decl "real_abs_le_pi2" asin nil) (sq_0 formula-decl nil sq "reals/") (sq_rew formula-decl nil sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (- 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) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (sq_sqrt formula-decl nil sqrt "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (div_cancel1 formula-decl nil real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sqrt_sq formula-decl nil sqrt "reals/") (SQX skolem-const-decl "{nnz: nnreal | nnz * nnz = 1 - sq(nnx)}" asin nil) (SQY skolem-const-decl "{nnz: nnreal | nnz * nnz = 1 - sq(nny)}" asin nil) (div_div2 formula-decl nil real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (minus_div1 formula-decl nil real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (atan_minus formula-decl nil atan nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (sqrt_1 formula-decl nil sqrt "reals/") (sqrt_lt formula-decl nil sqrt "reals/") (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (sqrt_pos judgement-tcc nil sqrt "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sq_1 formula-decl nil sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types nil) (sq_lt formula-decl nil sq "reals/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (atan_0 formula-decl nil atan nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (asin_derivable_TCC1 0 (asin_derivable_TCC1-1 nil 3262783212 ("" (grind) nil nil) nil shostak)) (asin_derivable_TCC2 0 (asin_derivable_TCC2-1 nil 3262782944 ("" (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)) (asin_derivable_TCC3 0 (asin_derivable_TCC3-1 nil 3262783234 ("" (assert) nil nil) ((noa_abs_lt1 formula-decl nil asin nil)) shostak)) (asin_derivable 0 (asin_derivable-3 nil 3445346806 ("" (skolem 1 ("z")) (("" (expand "asin") (("" (lemma "extensionality" ("f" "(LAMBDA (x: real_abs_lt1): IF x = -1 THEN -pi / 2 ELSIF x < 1 THEN atan(x / sqrt(1 - x * x)) ELSE pi / 2 ENDIF)" "g" "LAMBDA (x:real_abs_lt1): atan(x / sqrt(1 - x * x))")) (("1" (split -1) (("1" (hide -1) (("1" (lemma "identity_derivable_fun[real_abs_lt1]") (("1" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "1")) (("1" (expand "I") (("1" (lemma "prod_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): x" "f2" "LAMBDA (x: real_abs_lt1): x")) (("1" (assert) (("1" (expand "*") (("1" (lemma "diff_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x_1: real_abs_lt1): x_1 * x_1")) (("1" (assert) (("1" (expand "-") (("1" (lemma "sqrt_derivable_fun") (("1" (expand "restrict") (("1" (lemma "composition_derivable_fun[real_abs_lt1,posreal]" ("f" "LAMBDA (x_1: real_abs_lt1): 1 - x_1 * x_1" "g" "LAMBDA (s: posreal): sqrt(s)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "div_derivable_fun[real_abs_lt1]" ("f" "LAMBDA (x:real_abs_lt1): x" "g" "LAMBDA (x: real_abs_lt1): sqrt(1 - x * x)")) (("1" (assert) (("1" (expand "/") (("1" (lemma "deriv_atan_fun") (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real_abs_lt1,real]" ("f" "LAMBDA (x_1: real_abs_lt1): x_1 / sqrt(1 - x_1 * x_1)" "g" "atan")) (("1" (assert) (("1" (expand "o" -1) (("1" (expand "derivable?" -1) (("1" (inst - "z") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (assert) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma deriv_domain_real) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (mult-ineq -2 -2) (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (assert) (("3" (expand "not_one_element?") (("3" (skosimp*) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (lemma deriv_domain_posreal) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (case "x!1=-1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "x!1<1") (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("2" (expand "sq" -1) (("2" (expand "abs" -1 2) (("2" (lemma "sqrt_pos" ("px" "1-x!1*x!1")) (("1" (mult-ineq -4 -4) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (expand "sq") (("3" (expand "abs" -1 2) (("3" (assert) (("3" (hide-all-but 1) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (expand "sq") (("3" (assert) (("3" (hide-all-but 1) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (expand "abs" -1 2) (("3" (expand "sq") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "x!1") (("4" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("4" (expand "sq") (("4" (case-replace "abs(x!1) < 1") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (typepred "x!1") (("5" (mult-ineq -2 -2) (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (asin const-decl "real_abs_le_pi2" asin nil) (sq const-decl "nonneg_real" sq "reals/") (sqrt_pos judgement-tcc nil sqrt "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq_lt_abs formula-decl nil sq "reals/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (diff_derivable_fun formula-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (restrict const-decl "R" restrict nil) (NOT const-decl "[bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_times_lt_any1 formula-decl nil extra_real_props 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) (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) (sqrt_pos application-judgement "posreal" sqrt "reals/") (div_derivable_fun formula-decl nil derivatives "analysis/") (nzreal nonempty-type-eq-decl nil reals nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_atan_fun formula-decl nil atan nil) (O const-decl "T3" function_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (sqrt_derivable_fun formula-decl nil sqrt_derivative "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (extensionality formula-decl nil functions nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities 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_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 "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (asin_derivable-2 nil 3352189213 ("" (skolem 1 ("z")) (("" (expand "asin") (("" (lemma "extensionality" ("f" "(LAMBDA (x: real_abs_lt1): IF x = -1 THEN -pi / 2 ELSIF x < 1 THEN atan(x / sqrt(1 - x * x)) ELSE pi / 2 ENDIF)" "g" "LAMBDA (x:real_abs_lt1): atan(x / sqrt(1 - x * x))")) (("1" (split -1) (("1" (hide -1) (("1" (lemma "identity_derivable_fun[real_abs_lt1]") (("1" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): x" "f2" "LAMBDA (x: real_abs_lt1): x")) (("1" (assert) (("1" (expand "*") (("1" (lemma "diff_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x_1: real_abs_lt1): x_1 * x_1")) (("1" (assert) (("1" (expand "-") (("1" (lemma "sqrt_derivable_fun") (("1" (expand "restrict") (("1" (lemma "composition_derivable_fun[real_abs_lt1,posreal]" ("f" "LAMBDA (x_1: real_abs_lt1): 1 - x_1 * x_1" "g" "LAMBDA (s: posreal): sqrt(s)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "div_derivable_fun[real_abs_lt1]" ("f" "LAMBDA (x:real_abs_lt1): x" "g" "LAMBDA (x: real_abs_lt1): sqrt(1 - x * x)")) (("1" (assert) (("1" (expand "/") (("1" (lemma "deriv_atan_fun") (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real_abs_lt1,real]" ("f" "LAMBDA (x_1: real_abs_lt1): x_1 / sqrt(1 - x_1 * x_1)" "g" "atan")) (("1" (assert) (("1" (expand "o" -1) (("1" (expand "derivable" -1) (("1" (inst - "z") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (mult-ineq -2 -2) (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (grind) nil nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (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) ("6" (assert) (("6" (hide-all-but 1) (("6" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (case "x!1=-1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "x!1<1") (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("2" (expand "sq" -1) (("2" (expand "abs" -1 2) (("2" (lemma "sqrt_pos" ("px" "1-x!1*x!1")) (("1" (mult-ineq -4 -4) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (expand "sq") (("3" (expand "abs" -1 2) (("3" (assert) (("3" (hide-all-but 1) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (expand "sq") (("3" (assert) (("3" (hide-all-but 1) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (expand "abs" -1 2) (("3" (expand "sq") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "x!1") (("4" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("4" (expand "sq") (("4" (case-replace "abs(x!1) < 1") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (typepred "x!1") (("5" (mult-ineq -2 -2) (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq const-decl "nonneg_real" sq "reals/") (sqrt_pos judgement-tcc nil sqrt "reals/") (sq_lt_abs formula-decl nil sq "reals/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (sqrt_derivable_fun formula-decl nil sqrt_derivative "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_atan_fun formula-decl nil atan nil) (div_derivable_fun formula-decl nil derivatives "analysis/") (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_lt_pi2 nonempty-type-eq-decl nil atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")) nil) (asin_derivable-1 nil 3262868738 ("" (skolem 1 ("z")) (("" (expand "asin") (("" (lemma "extensionality" ("f" "(LAMBDA (x: real_abs_lt1): IF x = -1 THEN -pi / 2 ELSIF x < 1 THEN atan(x / sqrt(1 - x * x)) ELSE pi / 2 ENDIF)" "g" "LAMBDA (x:real_abs_lt1): atan(x / sqrt(1 - x * x))")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "identity_derivable_fun[real_abs_lt1]") (("1" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt1): x" "f2" "LAMBDA (x: real_abs_lt1): x")) (("1" (assert) (("1" (expand "*") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x_1: real_abs_lt1): x_1 * x_1")) (("1" (assert) (("1" (expand "-") (("1" (lemma "sqrt_derivable_fun") (("1" (expand "restrict") (("1" (lemma "composition_derivable_fun[real_abs_lt1,posreal]" ("f" "LAMBDA (x_1: real_abs_lt1): 1 - x_1 * x_1" "g" "LAMBDA (s: posreal): sqrt(s)")) (("1" (assert) (("1" (expand "o") (("1" (lemma "div_derivable_fun" ("f" "LAMBDA (x:real_abs_lt1): x" "g" "LAMBDA (x: real_abs_lt1): sqrt(1 - x * x)")) (("1" (assert) (("1" (expand "/") (("1" (lemma "deriv_atan_fun") (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real_abs_lt1,real]" ("f" "LAMBDA (x_1: real_abs_lt1): x_1 / sqrt(1 - x_1 * x_1)" "g" "atan")) (("1" (assert) (("1" (expand "o" -1) (("1" (expand "derivable" -1) (("1" (inst - "z") nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("2" (expand "abs" -1 2) (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (grind) nil nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (case "x!1=0") (("1" (inst + "1/2") (("1" (assert) nil nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide-all-but 1) (("6" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (case "x!1=-1") (("1" (replace -1) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (case "x!1<1") (("1" (assert) nil nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("2" (expand "sq" -1) (("2" (expand "abs" -1 2) (("2" (lemma "sqrt_pos" ("px" "1-x!1*x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (expand "sq") (("3" (expand "abs" -1 2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "x!1") (("4" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("4" (expand "sq") (("4" (expand "abs" -1 2) (("4" (lemma "sqrt_pos" ("px" "1-x!1*x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (typepred "x!1") (("5" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("5" (expand "abs" -1 2) (("5" (expand "sq") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sqrt_pos judgement-tcc nil sqrt "reals/") (const_derivable_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (sq const-decl "nonneg_real" sq "reals/") (sq_lt_abs formula-decl nil sq "reals/") (div_derivable_fun formula-decl nil derivatives "analysis/") (deriv_atan_fun formula-decl nil atan nil) (composition_derivable_fun formula-decl nil chain_rule "analysis/") (sqrt_derivable_fun formula-decl nil sqrt_derivative "analysis/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (pi const-decl "posreal" atan nil) (atan_value const-decl "real" atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")) shostak)) (asin_derivable_fun 0 (asin_derivable_fun-1 nil 3425654727 ("" (expand "derivable?") (("" (lemma "asin_derivable") (("" (propax) nil nil)) nil)) nil) ((asin_derivable formula-decl nil asin nil) (derivable? const-decl "bool" derivatives "analysis/")) nil)) (deriv_asin_fun_TCC1 0 (deriv_asin_fun_TCC1-2 nil 3425656962 ("" (lemma "asin_derivable_fun") (("" (propax) nil nil)) nil) ((asin_derivable_fun formula-decl nil asin nil)) nil) (deriv_asin_fun_TCC1-1 nil 3262783379 ("" (lemma "asin_derivable2") (("" (propax) nil nil)) nil) nil shostak)) (deriv_asin_fun_TCC2 0 (deriv_asin_fun_TCC2-1 nil 3262783401 ("" (skosimp*) (("" (typepred "x!1") (("" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("" (expand "abs" -1 2) (("" (expand "sq" -1 2) (("" (assert) (("" (expand "abs") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_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) (minus_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (sq_lt_abs formula-decl nil sq "reals/")) shostak)) (deriv_asin_fun_TCC3 0 (deriv_asin_fun_TCC3-1 nil 3262784007 ("" (skosimp*) (("" (typepred "x!1") (("" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("" (expand "abs" -1 2) (("" (expand "sq" -1 2) (("" (lemma "sqrt_pos" ("px" "1 - sq(x!1)")) (("1" (assert) nil nil) ("2" (assert) (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) 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) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (sqrt_pos judgement-tcc nil sqrt "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_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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (sq_lt_abs formula-decl nil sq "reals/")) shostak)) (deriv_asin_fun 0 (deriv_asin_fun-2 nil 3352189359 ("" (expand "asin") (("" (lemma "extensionality" ("f" "(LAMBDA (x: real_abs_lt1): IF x = -1 THEN -pi / 2 ELSIF x < 1 THEN atan(x / sqrt(1 - x * x)) ELSE pi / 2 ENDIF)" "g" "LAMBDA (x: real_abs_lt1): atan(x / sqrt(1 - x * x))")) (("1" (split -1) (("1" (lemma "identity_derivable_fun[real_abs_lt1]") (("1" (lemma "deriv_id_fun[real_abs_lt1]") (("1" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "1")) (("1" (lemma "deriv_const_fun[real_abs_lt1]" ("b" "1")) (("1" (expand "I") (("1" (lemma "prod_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): x" "f2" "LAMBDA (x: real_abs_lt1): x")) (("1" (assert) (("1" (expand "*" -1) (("1" (lemma "deriv_prod_fun[real_abs_lt1]" ("ff1" "LAMBDA (x: real_abs_lt1): x" "ff2" "LAMBDA (x: real_abs_lt1): x")) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (expand "+") (("1" (lemma "diff_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x_1: real_abs_lt1): x_1 * x_1")) (("1" (assert) (("1" (expand "-" -1) (("1" (lemma "deriv_diff_fun[real_abs_lt1]" ("ff1" "LAMBDA (x: real_abs_lt1): 1" "ff2" "LAMBDA (x_1: real_abs_lt1): x_1 * x_1")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "-" -1) (("1" (lemma "sqrt_derivable_fun") (("1" (lemma "deriv_sqrt_fun") (("1" (expand "restrict" (-1 -2)) (("1" (lemma "composition_derivable_fun[real_abs_lt1,posreal]" ("g" "LAMBDA (x: posreal): sqrt(x)" "f" "LAMBDA (x_1: real_abs_lt1): 1 - x_1 * x_1")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[real_abs_lt1,posreal]" ("gg" "LAMBDA (x: posreal): sqrt(x)" "ff" "LAMBDA (x_1: real_abs_lt1): 1 - x_1 * x_1")) (("1" (expand "o" -1) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (lemma "div_derivable_fun[real_abs_lt1]" ("f" "LAMBDA (x: real_abs_lt1): x" "g" "LAMBDA (x_1: real_abs_lt1): sqrt(1 - x_1 * x_1)")) (("1" (assert) (("1" (expand "/" -1) (("1" (lemma "deriv_div_fun[real_abs_lt1]" ("ff" "LAMBDA (x: real_abs_lt1): x" "gg" "LAMBDA (x_1: real_abs_lt1): sqrt(1 - x_1 * x_1)")) (("1" (replace -13 -1) (("1" (replace -3 -1) (("1" (expand "/" -1) (("1" (expand "*" -1) (("1" (expand "-" -1) (("1" (lemma "deriv_atan_fun") (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real_abs_lt1,real]" ("f" "LAMBDA (x_1: real_abs_lt1): x_1 / sqrt(1 - x_1 * x_1)" "g" "atan")) (("1" (expand "o" -1) (("1" (assert) (("1" (lemma "deriv_comp_fun[real_abs_lt1,real]" ("ff" "LAMBDA (x_1: real_abs_lt1): x_1 / sqrt(1 - x_1 * x_1)" "gg" "atan")) (("1" (replace -4 -1) (("1" (replace -5 -1) (("1" (expand "o" -1) (("1" (expand "*" -1) (("1" (replace -1 1) (("1" (hide-all-but 1) (("1" (lemma "extensionality" ("f" "(LAMBDA (x: real_abs_lt1): 1 / (1 + x / sqrt(1 - x * x) * (x / sqrt(1 - x * x))) * ((sqrt(1 - x * x) + 2 * (x * x * (1 / (2 * sqrt(1 - x * x))))) / (sqrt(1 - x * x) * sqrt(1 - x * x))))" "g" "(LAMBDA (x: real_abs_lt1): 1 / sqrt(1 - sq(x)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("z")) (("2" (typepred "z") (("2" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("2" (expand "abs" -1 2) (("2" (expand "sq") (("2" (lemma "sqrt_pos" ("px" "1-z*z")) (("1" (lemma "sq_sqrt" ("x" "1-z*z")) (("1" (expand "sq") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skolem 1 ("z")) (("2" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("2" (expand "sq") (("2" (typepred "z") (("2" (lemma "sqrt_pos" ("px" "1-z*z")) (("1" (assert) nil nil) ("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skolem 1 ("z")) (("3" (typepred "z") (("3" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("3" (expand "abs" -1 2) (("3" (expand "sq") (("3" (assert) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skolem 1 ("z")) (("4" (typepred "z") (("4" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("4" (expand "abs" -1 2) (("4" (expand "sq") (("4" (lemma "sq_sqrt" ("x" "1-z*z")) (("4" (expand "sq") (("4" (assert) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skolem 1 ("z")) (("5" (typepred "z") (("5" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("5" (expand "abs" -1 2) (("5" (expand "sq") (("5" (lemma "sqrt_pos" ("px" "1-z*z")) (("1" (assert) nil nil) ("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skolem 1 ("z")) (("6" (typepred "z") (("6" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("6" (expand "abs" -1 2) (("6" (expand "sq") (("6" (lemma "sqrt_pos" ("px" "1-z*z")) (("1" (lemma "sq_sqrt" ("x" "1-z*z")) (("1" (expand "sq" -1) (("1" (lemma "div_times" ("x" "z" "y" "z" "n0x" "sqrt(1 - z * z)" "n0y" "sqrt(1 - z * z)")) (("1" (replace -1 1) (("1" (split -2) (("1" (replace -1) (("1" (lemma "div_mult_pos_lt2" ("x" "-1" "z" "z*z" "py" "1-z*z")) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) 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" (hide-all-but 1) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma deriv_domain_real) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (assert) (("3" (expand "not_one_element?") (("3" (skosimp*) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (lemma deriv_domain_posreal) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (case "x!1 = -1") (("1" (assert) nil nil) ("2" (case "x!1<1") (("1" (assert) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("2" (typepred "x!1") (("2" (expand "sq") (("2" (lemma "sqrt_pos" ("px" "1-x!1*x!1")) (("1" (assert) nil nil) ("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (case "abs(x!1) < 1") (("1" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("1" (expand "abs" -1 2) (("1" (expand "sq" -1) (("1" (lemma "sqrt_pos" ("px" "1-x!1*x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (typepred "x!1") (("5" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("5" (expand "abs" -1 2) (("5" (expand "sq") (("5" (assert) (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_lt1 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) (- 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) (atan const-decl "real_abs_lt_pi2" atan nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan 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, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (extensionality formula-decl nil functions nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (deriv_prod_fun formula-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (deriv_sqrt_fun formula-decl nil sqrt_derivative "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (deriv_div_fun formula-decl nil derivatives "analysis/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_atan_fun formula-decl nil atan nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sq const-decl "nonneg_real" sq "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sqrt_pos judgement-tcc nil sqrt "reals/") (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) (sq_sqrt formula-decl nil sqrt "reals/") (sq_lt_abs formula-decl nil 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) (div_times formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (div_derivable_fun formula-decl nil derivatives "analysis/") (O const-decl "T3" function_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (restrict const-decl "R" restrict nil) (sqrt_derivable_fun formula-decl nil sqrt_derivative "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (asin const-decl "real_abs_le_pi2" asin nil) (real_times_real_is_real application-judgement "real" reals nil)) nil) (deriv_asin_fun-1 nil 3262784313 ("" (expand "asin") (("" (lemma "extensionality" ("f" "(LAMBDA (x: real_abs_lt1): IF x = -1 THEN -pi / 2 ELSIF x < 1 THEN atan(x / sqrt(1 - x * x)) ELSE pi / 2 ENDIF)" "g" "LAMBDA (x: real_abs_lt1): atan(x / sqrt(1 - x * x))")) (("1" (split -1) (("1" (replace -1 1) (("1" (lemma "identity_derivable_fun[real_abs_lt1]") (("1" (lemma "deriv_id_fun[real_abs_lt1]") (("1" (lemma "const_derivable_fun[real_abs_lt1]" ("b" "1")) (("1" (lemma "deriv_const_fun[real_abs_lt1]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt1): x" "f2" "LAMBDA (x: real_abs_lt1): x")) (("1" (assert) (("1" (expand "*" -1) (("1" (lemma "deriv_prod_fun" ("ff1" "LAMBDA (x: real_abs_lt1): x" "ff2" "LAMBDA (x: real_abs_lt1): x")) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (expand "+") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: real_abs_lt1): 1" "f2" "LAMBDA (x_1: real_abs_lt1): x_1 * x_1")) (("1" (assert) (("1" (expand "-" -1) (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: real_abs_lt1): 1" "ff2" "LAMBDA (x_1: real_abs_lt1): x_1 * x_1")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "-" -1) (("1" (lemma "sqrt_derivable_fun") (("1" (lemma "deriv_sqrt_fun") (("1" (expand "restrict" (-1 -2)) (("1" (lemma "composition_derivable_fun[real_abs_lt1,posreal]" ("g" "LAMBDA (x: posreal): sqrt(x)" "f" "LAMBDA (x_1: real_abs_lt1): 1 - x_1 * x_1")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[real_abs_lt1,posreal]" ("gg" "LAMBDA (x: posreal): sqrt(x)" "ff" "LAMBDA (x_1: real_abs_lt1): 1 - x_1 * x_1")) (("1" (expand "o" -1) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "*" -1) (("1" (lemma "div_derivable_fun" ("f" "LAMBDA (x: real_abs_lt1): x" "g" "LAMBDA (x_1: real_abs_lt1): sqrt(1 - x_1 * x_1)")) (("1" (assert) (("1" (expand "/" -1) (("1" (lemma "deriv_div_fun" ("ff" "LAMBDA (x: real_abs_lt1): x" "gg" "LAMBDA (x_1: real_abs_lt1): sqrt(1 - x_1 * x_1)")) (("1" (replace -13 -1) (("1" (replace -3 -1) (("1" (expand "/" -1) (("1" (expand "*" -1) (("1" (expand "-" -1) (("1" (lemma "deriv_atan_fun") (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real_abs_lt1,real]" ("f" "LAMBDA (x_1: real_abs_lt1): x_1 / sqrt(1 - x_1 * x_1)" "g" "atan")) (("1" (expand "o" -1) (("1" (assert) (("1" (lemma "deriv_comp_fun[real_abs_lt1,real]" ("ff" "LAMBDA (x_1: real_abs_lt1): x_1 / sqrt(1 - x_1 * x_1)" "gg" "atan")) (("1" (replace -4 -1) (("1" (replace -5 -1) (("1" (expand "o" -1) (("1" (expand "*" -1) (("1" (replace -1 1) (("1" (hide-all-but 1) (("1" (lemma "extensionality" ("f" "(LAMBDA (x: real_abs_lt1): 1 / (1 + x / sqrt(1 - x * x) * (x / sqrt(1 - x * x))) * ((sqrt(1 - x * x) + 2 * (x * x * (1 / (2 * sqrt(1 - x * x))))) / (sqrt(1 - x * x) * sqrt(1 - x * x))))" "g" "(LAMBDA (x: real_abs_lt1): 1 / sqrt(1 - sq(x)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("z")) (("2" (typepred "z") (("2" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("2" (expand "abs" -1 2) (("2" (expand "sq") (("2" (lemma "sqrt_pos" ("px" "1-z*z")) (("1" (lemma "sq_sqrt" ("x" "1-z*z")) (("1" (expand "sq") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skolem 1 ("z")) (("2" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("2" (expand "sq") (("2" (typepred "z") (("2" (expand "abs" -2 2) (("2" (lemma "sqrt_pos" ("px" "1-z*z")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skolem 1 ("z")) (("3" (typepred "z") (("3" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("3" (expand "abs" -1 2) (("3" (expand "sq") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skolem 1 ("z")) (("4" (typepred "z") (("4" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("4" (expand "abs" -1 2) (("4" (expand "sq") (("4" (lemma "sq_sqrt" ("x" "1-z*z")) (("4" (expand "sq") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skolem 1 ("z")) (("5" (typepred "z") (("5" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("5" (expand "abs" -1 2) (("5" (expand "sq") (("5" (lemma "sqrt_pos" ("px" "1-z*z")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (skolem 1 ("z")) (("6" (typepred "z") (("6" (lemma "sq_lt_abs" ("a" "z" "b" "1")) (("6" (expand "abs" -1 2) (("6" (expand "sq") (("6" (lemma "sqrt_pos" ("px" "1-z*z")) (("1" (lemma "sq_sqrt" ("x" "1-z*z")) (("1" (expand "sq" -1) (("1" (lemma "div_times" ("x" "z" "y" "z" "n0x" "sqrt(1 - z * z)" "n0y" "sqrt(1 - z * z)")) (("1" (replace -1 1) (("1" (split -2) (("1" (replace -1) (("1" (lemma "div_mult_pos_lt2" ("x" "-1" "z" "z*z" "py" "1-z*z")) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) 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" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (grind) nil nil)) nil) ("5" (hide-all-but 1) (("5" (skosimp*) (("5" (typepred "x!1") (("5" (case "x!1=0") (("1" (inst + "1/2") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide-all-but 1) (("6" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (expand "abs") (("2" (case "x!1 = -1") (("1" (assert) nil nil) ("2" (case "x!1<1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("2" (typepred "x!1") (("2" (expand "abs" -2 2) (("2" (expand "sq") (("2" (lemma "sqrt_pos" ("px" "1-x!1*x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (case "abs(x!1) < 1") (("1" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("1" (expand "abs" -1 2) (("1" (expand "sq" -1) (("1" (lemma "sqrt_pos" ("px" "1-x!1*x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (typepred "x!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (skosimp*) (("5" (typepred "x!1") (("5" (lemma "sq_lt_abs" ("a" "x!1" "b" "1")) (("5" (expand "abs" -1 2) (("5" (expand "sq") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (atan const-decl "real_abs_lt_pi2" atan nil) (atan_value const-decl "real" atan nil) (pi const-decl "posreal" atan nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_prod_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (deriv_sqrt_fun formula-decl nil sqrt_derivative "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (deriv_div_fun formula-decl nil derivatives "analysis/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_atan_fun formula-decl nil atan nil) (sq const-decl "nonneg_real" sq "reals/") (sqrt_pos judgement-tcc nil sqrt "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sq_lt_abs formula-decl nil sq "reals/") (div_derivable_fun formula-decl nil derivatives "analysis/") (sqrt_derivable_fun formula-decl nil sqrt_derivative "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/")) shostak)) (asin_pos_bnds_TCC1 0 (asin_pos_bnds_TCC1-1 nil 3263659929 ("" (skosimp*) (("" (typepred "px!1") (("" (expand "abs" -1) (("" (expand "abs" 1) (("" (assert) (("" (lemma "posreal_times_posreal_is_posreal" ("px" "px!1" "py" "px!1")) (("" (case "px!1 = 1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "px!1 * px!1" "py" "6")) (("2" (lemma "both_sides_minus_lt2" ("z" "1" "y" "0" "x" "px!1*px!1/6")) (("2" (expand ">" -2) (("2" (replace -2 -1) (("2" (flatten -1) (("2" (lemma "lt_times_lt_pos1" ("px" "px!1" "y" "1" "nnz" "1 - px!1 * px!1 / 6" "w" "1")) (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "px!1 - px!1 * px!1 / 6 * px!1" "py" "px!1")) (("2" (lemma "minus_div2" ("x" "px!1" "y" "px!1*px!1/6*px!1" "n0x" "px!1")) (("2" (replace -1 -2 rl) (("2" (hide -1) (("2" (rewrite "div_simp" -1) (("2" (case "px!1 * px!1 / 6 * px!1 / px!1 = px!1 * px!1 / 6") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide 2 4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((< 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) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> 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) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_simp formula-decl nil real_props nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (both_sides_minus_lt2 formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities 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) (minus_nzreal_is_nzreal application-judgement "nzreal" real_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) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) shostak)) (asin_pos_bnds 0 (asin_pos_bnds-3 nil 3425656930 ("" (skosimp*) (("" (split) (("1" (lemma "asin_derivable_fun") (("1" (lemma "deriv_asin_fun") (("1" (lemma "identity_derivable_fun[real_abs_lt1]") (("1" (lemma "deriv_id_fun[real_abs_lt1]") (("1" (expand "I") (("1" (lemma "diff_derivable_fun[real_abs_lt1]" ("f1" "LAMBDA (x: real_abs_lt1): asin(x)" "f2" "LAMBDA (x: real_abs_lt1): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun[real_abs_lt1]" ("ff1" "LAMBDA (x: real_abs_lt1): asin(x)" "ff2" "LAMBDA (x: real_abs_lt1): x")) (("1" (replace -5 -1) (("1" (replace -3 -1) (("1" (expand "-") (("1" (typepred "px!1") (("1" (hide -1) (("1" (expand "<=" -1) (("1" (split -1) (("1" (lemma "minimum_derivative[{x:nnreal| x < 1}]" ("g" "LAMBDA (x_1:{x:nnreal| x < 1} ): asin(x_1) - x_1" "x" "0" "y1" "px!1")) (("1" (split -1) (("1" (simplify -1) (("1" (rewrite "asin_0") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "restrict2_deriv[{x: nnreal | x < 1},real_abs_lt1]" ("f" "LAMBDA (x_1: real_abs_lt1): asin(x_1) - x_1" "a" "0")) (("1" (replace -4 -1) (("1" (simplify -1) (("1" (expand "restrict2" -1) (("1" (replace -1 1 rl) (("1" (expand "sq" 1) (("1" (rewrite "sqrt_1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp*) (("3" (inst + "x!1") nil nil)) nil)) nil) ("3" (assert) nil nil) ("4" (skosimp*) (("4" (typepred "y!1") (("4" (expand ">=" -1) (("4" (expand "<=" -1) (("4" (split -1) (("1" (lemma "restrict2_deriv[{x: nnreal | x < 1},real_abs_lt1]" ("f" "LAMBDA (x_1: real_abs_lt1): asin(x_1) - x_1" "a" "y!1")) (("1" (replace -6 -1) (("1" (simplify -1) (("1" (expand "restrict2" -1) (("1" (replace -1 2 rl) (("1" (hide -1 -6 3 1 -7 -8 -9 -10 -11) (("1" (lemma "sq_lt" ("nna" "0" "nnb" "y!1")) (("1" (lemma "sq_lt" ("nna" "y!1" "nnb" "1")) (("1" (expand "sq" -1 2) (("1" (expand "sq" -2 1) (("1" (assert) (("1" (lemma "sqrt_pos" ("px" "1-sq(y!1)")) (("1" (lemma "div_mult_pos_gt2" ("z" "1" "py" "sqrt(1-sq(y!1))" "x" "1")) (("1" (lemma "sqrt_lt" ("nny" "1-sq(y!1)" "nnz" "1")) (("1" (rewrite "sqrt_1") (("1" (assert) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "1 / sqrt(1 - sq(y!1))-1" "py" "y!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp*) (("3" (inst + "x!1") nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (lemma "restrict2_derivable[{x: nnreal | x < 1},real_abs_lt1]" ("f" "LAMBDA (x_1: real_abs_lt1): asin(x_1) - x_1")) (("1" (expand "restrict2" -1) (("1" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (skosimp*) (("3" (typepred "x!1") (("3" (inst + "x!1") nil nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand "connected?") (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "asin_1") (("2" (lemma "pi_bnds") (("2" (flatten) (("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" (flatten) (("2" (case "px!1 < sqrt(6)") (("1" (typepred "px!1") (("1" (lemma "identity_derivable_fun[{x:nnreal| x <= 1}]") (("1" (lemma "deriv_id_fun[{x:nnreal| x <= 1}]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[{x:nnreal| x <= 1}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x:nnreal| x <= 1}]" ("b" "1")) (("1" (lemma "prod_derivable_fun[{x:nnreal| x <= 1}]" ("f1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "f2" "LAMBDA (x: {x: nnreal | x <= 1}): x")) (("1" (assert) (("1" (expand "*" -1) (("1" (lemma "deriv_prod_fun[{x:nnreal| x <= 1}]" ("ff1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "ff2" "LAMBDA (x: {x: nnreal | x <= 1}): x")) (("1" (replace -5 -1) (("1" (expand "*") (("1" (expand "+") (("1" (lemma "scal_derivable_fun[{x:nnreal| x <= 1}]" ("f" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 * x_1" "b" "1/6")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_scal_fun[{x:nnreal| x <= 1}]" ("ff" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 * x_1" "b" "1/6")) (("1" (replace -3 -1) (("1" (expand "*" -1) (("1" (lemma "diff_derivable_fun[{x:nnreal| x <= 1}]" ("f1" "LAMBDA (x: {x: nnreal | x <= 1}): 1" "f2" "LAMBDA (x: {x: nnreal | x <= 1}): 1 / 6 * (x * x)")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun[{x:nnreal| x <= 1}]" ("ff1" "LAMBDA (x: {x: nnreal | x <= 1}): 1" "ff2" "LAMBDA (x: {x: nnreal | x <= 1}): 1 / 6 * (x * x)")) (("1" (replace -7 -1) (("1" (replace -3 -1) (("1" (expand "-") (("1" (lemma "prod_derivable_fun[{x:nnreal| x <= 1}]" ("f1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "f2" "LAMBDA (x_1: {x: nnreal | x <= 1}): 1 - 1 / 6 * (x_1 * x_1)")) (("1" (assert) (("1" (expand "*") (("1" (lemma "deriv_prod_fun[{x:nnreal| x <= 1}]" ("ff1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "ff2" "LAMBDA (x_1: {x: nnreal | x <= 1}): 1 - 1 / 6 * (x_1 * x_1)")) (("1" (replace -3 -1) (("1" (replace -11 -1) (("1" (expand "*") (("1" (expand "+") (("1" (lemma "asin_derivable_fun") (("1" (lemma "deriv_asin_fun") (("1" (tccs-step (lemma "composition_derivable_fun[{x: nnreal | x <= 1},real_abs_lt1]" ("f" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 - x_1 * x_1 * x_1 * (1 / 6)" "g" "LAMBDA (x: real_abs_lt1): asin(x)")) :label "TCC" :hide? t) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: nnreal | x <= 1},real_abs_lt1]" ("ff" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 - x_1 * x_1 * x_1 * (1 / 6)" "gg" "LAMBDA (x: real_abs_lt1): asin(x)")) (("1" (replace -3 -1) (("1" (replace -5 -1) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "diff_derivable_fun[{x:nnreal| x <= 1}]" ("f1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "f2" "LAMBDA (x_1: {x: nnreal | x <= 1}): asin(x_1 - x_1 * x_1 * x_1 * (1 / 6))")) (("1" (expand "-") (("1" (assert) (("1" (lemma "deriv_diff_fun[{x:nnreal| x <= 1}]" ("ff1" "LAMBDA (x: {x: nnreal | x <= 1}): x" "ff2" "LAMBDA (x_1: {x: nnreal | x <= 1}): asin(x_1 - x_1 * x_1 * x_1 * (1 / 6))")) (("1" (replace -3 -1) (("1" (replace -17 -1) (("1" (expand "-") (("1" (lemma "minimum_derivative[{x: nnreal | x <= 1}]" ("g" "LAMBDA (x_1: {x: nnreal | x <= 1}): x_1 - asin(x_1 - x_1 * x_1 * x_1 * (1 / 6))" "x" "0" "y1" "px!1")) (("1" (split -1) (("1" (simplify -1) (("1" (assert) (("1" (rewrite "asin_0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -1 1) (("2" (simplify 1) (("2" (rewrite "sq_0") (("2" (rewrite "sqrt_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (replace -1 1) (("4" (hide-all-but 1) (("4" (skosimp*) (("4" (typepred "y!1") (("4" (expand ">=" -1) (("4" (expand "<=" -1) (("4" (split -1) (("1" (hide 1) (("1" (name "AP" "y!1 - y!1 * y!1 * y!1 * (1 / 6)") (("1" (replace -1) (("1" (lemma "sq_le" ("nna" "y!1" "nnb" "1")) (("1" (expand "sq" -1) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1" "py" "1-y!1 * y!1 / 6")) (("1" (expand "<=" -5) (("1" (split -5) (("1" (lemma "sq_lt" ("nna" "y!1" "nnb" "1")) (("1" (rewrite "sq_rew") (("1" (rewrite "sq_1") (("1" (flatten -1) (("1" (replace -3 -2) (("1" (hide -1) (("1" (hide -4) (("1" (lemma "lt_times_lt_pos1" ("px" "y!1" "y" "1" "nnz" "1 - sq(y!1) / 6" "w" "1")) (("1" (split -1) (("1" (replace -5) (("1" (lemma "sq_lt" ("nna" "AP" "nnb" "1")) (("1" (expand "sq" -1) (("1" (assert) (("1" (rewrite "sq_rew" -1) (("1" (lemma "sq_lt" ("nna" "0" "nnb" "AP")) (("1" (rewrite "sq_0") (("1" (assert) (("1" (case "1-sq(AP) > 0") (("1" (lemma "sqrt_lt" ("nny" "0" "nnz" "1-sq(AP)")) (("1" (rewrite "sqrt_0") (("1" (flatten -1) (("1" (expand ">" -3) (("1" (replace -3 -2) (("1" (hide -1) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "(sq(y!1)/2-1)/sqrt(1 - sq(AP))+1" "py" "y!1")) (("1" (assert) nil nil) ("2" (hide 2) (("2" (case "1-sq(y!1)/2 > 0") (("1" (lemma "div_mult_pos_lt1" ("x" "1" "z" "1 - sq(y!1) / 2" "py" "sqrt(1 - sq(AP))")) (("1" (lemma "sq_lt" ("nna" "1 - sq(y!1) / 2" "nnb" "sqrt(1 - sq(AP))")) (("1" (rewrite "sq_sqrt" -1) (("1" (case "sq(1 - sq(y!1) / 2) < 1 - sq(AP)") (("1" (assert) nil nil) ("2" (hide 2 -1 -2) (("2" (expand "AP" 1) (("2" (expand "sq" 1 1) (("2" (simplify 1) (("2" (expand "sq" --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.764 Sekunden (vorverarbeitet am 2026-05-01) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26