| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/exact_real_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 MB |
|
Quelle sincosx.prfSprache: Lisp |
|||||||||||||||
|
(sincosx (real_3pi16_TCC1 0 (real_3pi16_TCC1-1 nil 3393563994 ("" (lemma "pi_bnds") (("" (flatten) (("" (assert) nil nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bnds formula-decl nil atan "trig_fnd/")) nil)) (cauchy_real_3pi16_TCC1 0 (cauchy_real_3pi16_TCC1-1 nil 3393563994 ("" (expand "cauchy_real_3pi16?") (("" (inst + "0") (("1" (expand "cauchy_prop") (("1" (propax) nil nil)) nil) ("2" (lemma "pi_bnds") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" 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) (pi const-decl "posreal" atan "trig_fnd/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_3pi16 nonempty-type-eq-decl nil sincosx nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (pi_bnds formula-decl nil atan "trig_fnd/") (cauchy_real_3pi16? const-decl "bool" sincosx nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (cauchy_nnsreal_TCC1 0 (cauchy_nnsreal_TCC1-1 nil 3393747713 ("" (expand "cauchy_nnsreal?") (("" (inst + "0") (("" (expand "cauchy_prop") (("" (propax) 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) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (nnsreal nonempty-type-eq-decl nil sincosx nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil) (cauchy_nnsreal? const-decl "bool" sincosx nil)) nil)) (subtype_TCC1 0 (subtype_TCC1-1 nil 3393563994 ("" (grind) nil nil) nil nil)) (subtype_TCC2 0 (subtype_TCC2-1 nil 3393747713 ("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_real?") (("" (expand "cauchy_nnsreal?") (("" (skosimp) (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_nnsreal nonempty-type-eq-decl nil sincosx nil) (cauchy_nnsreal? const-decl "bool" sincosx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (nnsreal nonempty-type-eq-decl nil sincosx nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (cauchy_real? const-decl "bool" cauchy nil)) nil)) (subtype_TCC3 0 (subtype_TCC3-1 nil 3393747713 ("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_real_3pi16?") (("" (expand "cauchy_real?") (("" (skosimp) (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real_3pi16 nonempty-type-eq-decl nil sincosx nil) (cauchy_real_3pi16? const-decl "bool" sincosx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (cauchy_real? const-decl "bool" cauchy 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 "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields 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 "trig_fnd/") (real_3pi16 nonempty-type-eq-decl nil sincosx nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (cauchy_sin_series_TCC1 0 (cauchy_sin_series_TCC1-1 nil 3393414809 ("" (skosimp) (("" (expand "cauchy_nzreal?") (("" (inst + "factorial(1+2*n!1)") (("" (rewrite "int_lemma") nil nil)) nil)) nil)) nil) ((int_times_int_is_int application-judgement "int" integers 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) (mult_divides2 application-judgement "(divides(m))" divides nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (int_lemma formula-decl nil int nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil)) nil)) (cauchy_cos_series_TCC1 0 (cauchy_cos_series_TCC1-1 nil 3393414809 ("" (skosimp) (("" (expand "cauchy_nzreal?") (("" (inst + "factorial(2*n!1)") (("" (rewrite "int_lemma") nil nil)) nil)) nil)) nil) ((cauchy_nzreal? const-decl "bool" cauchy nil) (int_lemma formula-decl nil int nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (int_times_int_is_int application-judgement "int" integers 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) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (sin_series_lemma 0 (sin_series_lemma-1 nil 3393414810 ("" (skosimp) (("" (expand "cauchy_sin_series") (("" (expand "sin_term") (("" (lemma "div_lemma" ("x" "(-1) ^ n!1" "cx" "cauchy_int((-1) ^ n!1)" "nzy" "factorial(1 + 2 * n!1)" "nzcy" "cauchy_int(factorial(1 + 2 * n!1))")) (("" (rewrite "expt_1i") (("" (rewrite "int_lemma") (("" (rewrite "int_lemma") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_sin_series const-decl "cauchy_real" sincosx nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (div_lemma formula-decl nil div nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_lemma formula-decl nil int nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_int_is_int application-judgement "int" integers nil) (expt_1i formula-decl nil exponentiation nil) (sin_term const-decl "real" trig_approx "trig_fnd/")) shostak)) (cos_series_lemma 0 (cos_series_lemma-1 nil 3393414930 ("" (skosimp) (("" (expand "cauchy_cos_series") (("" (expand "cos_term") (("" (rewrite "expt_1i") (("" (case-replace "n!1=0") (("1" (rewrite "expt_x0") (("1" (expand "factorial") (("1" (lemma "div_lemma" ("x" "1" "cx" "cauchy_int(1)" "nzy" "1" "nzcy" "cauchy_int(1)")) (("1" (rewrite "int_lemma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "div_lemma" ("x" "(-1) ^ n!1" "nzy" "factorial(2 * n!1)" "cx" "cauchy_int((-1) ^ n!1)" "nzcy" "cauchy_int(factorial(2 * n!1))")) (("2" (rewrite "int_lemma") (("2" (rewrite "int_lemma") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_cos_series const-decl "cauchy_real" sincosx nil) (int_times_int_is_int application-judgement "int" integers 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) (mult_divides2 application-judgement "(divides(m))" divides nil) (expt_1i formula-decl nil exponentiation 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (expt_x0 formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (div_lemma formula-decl nil div nil) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (int_lemma formula-decl nil int nil) (factorial def-decl "posnat" factorial "ints/") (= const-decl "[T, T -> boolean]" equalities nil) (cos_term const-decl "real" trig_approx "trig_fnd/")) shostak)) (cauchy_sin_drx_TCC1 0 (cauchy_sin_drx_TCC1-1 nil 3393418937 ("" (expand "cauchys_real?") (("" (lemma "sin_series_lemma") (("" (expand "cauchys_prop") (("" (inst + "sin_term(1)") nil nil)) nil)) nil)) nil) ((sin_series_lemma formula-decl nil sincosx 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sin_term const-decl "real" trig_approx "trig_fnd/") (cauchys_prop const-decl "bool" sum nil) (cauchys_real? const-decl "bool" sum nil)) nil)) (cauchy_sin_drx_TCC2 0 (cauchy_sin_drx_TCC2-2 nil 3508597737 ("" (skosimp) (("" (typepred "csnx!1") (("" (expand "cauchy_nnsreal?") (("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_real?") (("" (expand "<=" -1) (("" (split -1) (("1" (lemma "powerseries_lemma" ("x" "x!1" "cx" "csnx!1" "xs" "sin_term(1)" "cxs" "cauchy_sin_series")) (("1" (replace -4) (("1" (lemma "sin_series_lemma") (("1" (replace -1) (("1" (hide -1) (("1" (inst + "sin(sqrt(x!1))/sqrt(x!1)") (("1" (hide -4) (("1" (expand "cauchy_prop") (("1" (skosimp) (("1" (inst - "2+p!1") (("1" (inst - "2+p!1") (("1" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_sin_series, 2 + p!1)(2 + p!1)") (("1" (flatten) (("1" (expand "powerseries") (("1" (lemma "sin_approx_sin" ("a" "sqrt(x!1)" "n" "2+p!1")) (("1" (expand "sin_approx") (("1" (expand "sin_term" -1 2) (("1" (rewrite "abs_div") (("1" (rewrite "abs_mult") (("1" (expand "abs" -1 4) (("1" (assert) (("1" (typepred "factorial(7 + 2 * p!1)") (("1" (assert) (("1" (hide -1) (("1" (rewrite "abs_expt" -1 :dir rl) (("1" (expand "abs" -1 2) (("1" (rewrite "expt_1i") (("1" (lemma "expt_plus" ("n0x" "sqrt(x!1)" "i" "1" "j" "6+2*p!1")) (("1" (lemma "expt_times" ("n0x" "sqrt(x!1)" "i" "2" "j" "3+p!1")) (("1" (rewrite "expt_x2") (("1" (rewrite "sq_rew") (("1" (replace -1 -2) (("1" (rewrite "expt_x1") (("1" (replace -2 -3) (("1" (expand "abs" -3 2) (("1" (assert) (("1" (hide -1 -2) (("1" (case-replace "sigma(0, 2 + p!1, LAMBDA (i:nat): IF i = 0 THEN sin_term(1)(i) ELSE sin_term(1)(i) * x!1 ^ i ENDIF)=sigma(0, 2 + p!1, sin_term(sqrt(x!1)))/sqrt(x!1)") (("1" (hide -1) (("1" (lemma "div_mult_pos_le1" ("py" "sqrt(x!1)" "x" "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1)" "z" "abs(sin(sqrt(x!1)) - sigma(0, 2 + p!1, sin_term(sqrt(x!1))))")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (lemma "abs_div" ("x" "sin(sqrt(x!1)) - sigma(0, 2 + p!1, sin_term(sqrt(x!1)))" "n0y" "sqrt(x!1)")) (("1" (expand "abs" -1 3) (("1" (replace -1 -2 rl) (("1" (assert) (("1" (hide -1) (("1" (rewrite "minus_div2" -1 :dir rl) (("1" (name-replace "SIN_APPROX" "sigma(0, 2 + p!1, sin_term(sqrt(x!1))) / sqrt(x!1)") (("1" (name-replace "SIN_" "sin(sqrt(x!1)) / sqrt(x!1)") (("1" (case "abs(SIN_APPROX-CPS/2 ^ (2 + p!1))<2^-(2+p!1)") (("1" (case "abs(SIN_-CPS / 2 ^ (2 + p!1)) < 2 ^ -(1 + p!1)") (("1" (hide -2 -3 -4 -5) (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (rewrite "expt_inverse") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x1") (("1" (name-replace "P2" "2^p!1") (("1" (lemma "div_mult_pos_lt2" ("py" "P2" "z" "1/2" "x" "abs(SIN_ - CPS / (4 * P2))")) (("1" (replace -1 -4) (("1" (hide -1) (("1" (lemma "abs_mult" ("x" "SIN_ - CPS / (4 * P2)" "y" "P2")) (("1" (expand "abs" -1 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1) < 2^-(2+p!1)") (("1" (name-replace "DRL1" "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1)") (("1" (case-replace "2 ^ -(1 + p!1)=2*2 ^ -(2 + p!1)") (("1" (rewrite "expt_inverse" 1) (("1" (name-replace "P2" "2 ^ (2 + p!1)") (("1" (hide-all-but (-2 -3 -4 1)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "expt_x2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 -6 1)) (("2" (lemma "both_sides_expt_pos_lt" ("px" "x!1" "py" "1/2" "pm" "3+p!1")) (("2" (assert) (("2" (rewrite "div_mult_pos_lt1") (("2" (lemma "inv_expt") (("2" (inst -1 "3+p!1" "2") (("2" (replaces -1) (("2" (rewrite "expt_inverse" 1) (("2" (name-replace "DRL1" "x!1 ^ (3 + p!1)") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x2") (("2" (rewrite "expt_x3") (("2" (assert) (("2" (lemma "factorial_incr" ("k" "3" "n" "7 + 2 * p!1")) (("2" (rewrite "factorial_3") (("2" (assert) (("2" (lemma "both_sides_times_pos_lt1" ("pz" "1/(4*2^p!1)" "x" "1/2" "y" "factorial(7 + 2 * p!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (lemma "div_mult_pos_lt1" ("py" "2^(2+p!1)" "x" "SIN_APPROX" "z" "CPS - 1")) (("2" (lemma "div_mult_pos_lt2" ("py" "2^(2+p!1)" "x" "SIN_APPROX" "z" "CPS+1")) (("2" (assert) (("2" (rewrite "expt_inverse" 1) (("2" (name-replace "P2" "2^(2+p!1)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -5 1)) (("2" (case-replace "(LAMBDA (i_1: nat): IF i_1 = 0 THEN sin_term(1)(i_1) ELSE sin_term(1)(i_1) * x!1 ^ i_1 ENDIF) =(LAMBDA (i: nat): 1 / sqrt(x!1) * sin_term(sqrt(x!1))(i))") (("1" (hide -1 2) (("1" (assert) (("1" (rewrite "sigma_scal") (("1" (expand "sin_term") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "sin_term") (("2" (typepred "factorial(1 + 2 * x!2)") (("2" (name-replace "FACTORIAL" "factorial(1 + 2 * x!2)") (("2" (rewrite "expt_1i") (("2" (rewrite "expt_plus") (("2" (name-replace "SIGN" "(-1) ^ x!2") (("2" (rewrite "expt_x1") (("2" (case-replace "sqrt(x!1) ^ (2 * x!2)=x!1^x!2") (("1" (case-replace "x!2=0") (("1" (assert) (("1" (rewrite "expt_x0") (("1" (replace -2 1 rl) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (lemma "expt_times" ("i" "2" "j" "x!2" "n0x" "sqrt(x!1)")) (("2" (rewrite "expt_x2") (("2" (rewrite "sq_rew") 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/=" 1) (("2" (lemma "sqrt_eq_0" ("nnx" "x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (hide -1 -2) (("2" (inst + "1") (("2" (lemma "powerseries_lemma" ("x" "0" "cx" "csnx!1" "xs" "sin_term(1)" "cxs" "cauchy_sin_series")) (("2" (lemma "sin_series_lemma") (("2" (replace -1) (("2" (replace -3) (("2" (hide -1 -3) (("2" (expand "cauchy_prop") (("2" (skosimp) (("2" (inst - "2+p!1") (("2" (inst - "2+p!1") (("2" (flatten) (("2" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_sin_series, 2 + p!1)(2 + p!1)") (("2" (case-replace "powerseries(0, sin_term(1), 2 + p!1)=1") (("1" (hide -1) (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (lemma "div_mult_pos_lt2" ("z" "1+CPS" "x" "2^p!1" "py" "4")) (("1" (lemma "div_mult_pos_lt1" ("z" "CPS-1" "x" "2^p!1" "py" "4")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "powerseries") (("2" (case-replace "(LAMBDA (i:nat): IF i = 0 THEN sin_term(1)(i) ELSE sin_term(1)(i) * 0 ^ i ENDIF)=(LAMBDA (i:na (("1" (hide -1) (("1" (assert) (("1" (rewrite "sigma_first") (("1" (lemma "sigma_eq[nat]" ("low" "1" "high" "2+p!1" "F" "(LAMBDA (i: nat): IF i = 0 THEN 1 ELSE 0 ENDIF)" "G" "(LAMBDA (i:nat): 0)")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_zero") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) (("2" (apply-extensionality :hide? t) (("2" (case-replace "x!2=0") (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_nnsreal nonempty-type-eq-decl nil sincosx nil) (cauchy_nnsreal? const-decl "bool" sincosx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (cauchy_real? const-decl "bool" cauchy nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal 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/") (x!1 skolem-const-decl "nnsreal" sincosx nil) (sin const-decl "real" sincos_def "trig_fnd/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (posint_exp application-judgement "posint" exponentiation nil) (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (cauchy_prop const-decl "bool" cauchy nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (cauchy_powerseries const-decl "cauchy_real" powerseries nil) (cauchys_real nonempty-type-eq-decl nil sum nil) (cauchys_real? const-decl "bool" sum nil) (powerseries const-decl "real" powerseries nil) (sin_approx const-decl "real" trig_approx "trig_fnd/") (- const-decl "[numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (abs_div formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (expt_plus formula-decl nil exponentiation nil) (expt_x2 formula-decl nil inv nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (div_mult_pos_le1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_div2 formula-decl nil real_props nil) (round const-decl "int" prelude_aux nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posint nonempty-type-eq-decl nil integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (expt_inverse formula-decl nil exponentiation nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (minus_real_is_real application-judgement "real" reals nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (both_sides_expt_pos_lt formula-decl nil exponentiation nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (factorial_3 formula-decl nil factorial "ints/") (both_sides_times_pos_lt1 formula-decl nil real_props nil) (factorial_incr formula-decl nil factorial "ints/") (expt_x3 formula-decl nil exponentiation nil) (inv_expt formula-decl nil exponentiation nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sigma_scal formula-decl nil sigma "reals/") (expt_x0 formula-decl nil exponentiation nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (expt_x1 formula-decl nil exponentiation nil) (sq_sqrt formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_rew formula-decl nil sq "reals/") (expt_times formula-decl nil exponentiation nil) (expt_1i formula-decl nil exponentiation nil) (abs_expt formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (real_gt_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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_mult formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_int_is_int application-judgement "int" integers nil) (sin_approx_sin formula-decl nil trig_approx "trig_fnd/") (real_minus_real_is_real application-judgement "real" reals nil) (sqrt_eq_0 formula-decl nil sqrt "reals/") (sin_series_lemma formula-decl nil sincosx nil) (powerseries_lemma formula-decl nil powerseries nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_sin_series const-decl "cauchy_real" sincosx nil) (sin_term const-decl "real" trig_approx "trig_fnd/") (sigma_nat application-judgement "nat" sum nil) (sigma_nnreal application-judgement "nnreal" sum nil) (sigma_eq formula-decl nil sigma "reals/") (sigma_zero formula-decl nil sigma "reals/") (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_first formula-decl nil sigma "reals/") (expt def-decl "real" exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (int_expt application-judgement "int" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nnsreal nonempty-type-eq-decl nil sincosx nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil)) nil) (cauchy_sin_drx_TCC2-1 nil 3393418937 ("" (skosimp) (("" (typepred "csnx!1") (("" (expand "cauchy_nnsreal?") (("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_real?") (("" (expand "<=" -1) (("" (split -1) (("1" (lemma "powerseries_lemma" ("x" "x!1" "cx" "csnx!1" "xs" "sin_term(1)" "cxs" "cauchy_sin_series")) (("1" (replace -4) (("1" (lemma "sin_series_lemma") (("1" (replace -1) (("1" (hide -1) (("1" (inst + "sin(sqrt(x!1))/sqrt(x!1)") (("1" (hide -4) (("1" (expand "cauchy_prop") (("1" (skosimp) (("1" (inst - "2+p!1") (("1" (inst - "2+p!1") (("1" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_sin_series, 2 + p!1)(2 + p!1)") (("1" (flatten) (("1" (expand "powerseries") (("1" (lemma "sin_approx_sin" ("a" "sqrt(x!1)" "n" "2+p!1")) (("1" (expand "sin_approx") (("1" (expand "sin_term" -1 2) (("1" (rewrite "abs_div") (("1" (rewrite "abs_mult") (("1" (expand "abs" -1 4) (("1" (rewrite "abs_expt" -1 :dir rl) (("1" (expand "abs" -1 2) (("1" (rewrite "expt_1i") (("1" (lemma "expt_plus" ("n0x" "sqrt(x!1)" "i" "1" "j" "6+2*p!1")) (("1" (lemma "expt_times" ("n0x" "sqrt(x!1)" "i" "2" "j" "3+p!1")) (("1" (rewrite "expt_x2") (("1" (rewrite "sq_rew") (("1" (replace -1 -2) (("1" (rewrite "expt_x1") (("1" (replace -2 -3) (("1" (expand "abs" -3 2) (("1" (assert) (("1" (hide -1 -2) (("1" (case-replace "sigma(0, 2 + p!1, LAMBDA (i:nat): IF i = 0 THEN sin_term(1)(i) ELSE sin_term(1)(i) * x!1 ^ i ENDIF)=sigma(0, 2 + p!1, sin_term(sqrt(x!1)))/sqrt(x!1)") (("1" (hide -1) (("1" (lemma "div_mult_pos_le1" ("py" "sqrt(x!1)" "x" "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1)" "z" "abs(sin(sqrt(x!1)) - sigma(0, 2 + p!1, sin_term(sqrt(x!1))))")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (lemma "abs_div" ("x" "sin(sqrt(x!1)) - sigma(0, 2 + p!1, sin_term(sqrt(x!1)))" "n0y" "sqrt(x!1)")) (("1" (expand "abs" -1 3) (("1" (replace -1 -2 rl) (("1" (assert) (("1" (hide -1) (("1" (rewrite "minus_div2" -1 :dir rl) (("1" (name-replace "SIN_APPROX" "sigma(0, 2 + p!1, sin_term(sqrt(x!1))) / sqrt(x!1)") (("1" (name-replace "SIN" "sin(sqrt(x!1)) / sqrt(x!1)") (("1" (case "abs(SIN_APPROX-CPS/2 ^ (2 + p!1))<2^-(2+p!1)") (("1" (case "abs(SIN-CPS / 2 ^ (2 + p!1)) < 2 ^ -(1 + p!1)") (("1" (hide -2 -3 -4 -5) (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (rewrite "expt_inverse") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x1") (("1" (name-replace "P2" "2^p!1") (("1" (lemma "div_mult_pos_lt2" ("py" "P2" "z" "1/2" "x" "abs(SIN - CPS / (4 * P2))")) (("1" (rewrite "div_div2") (("1" (replace -1 -4) (("1" (hide -1) (("1" (lemma "abs_mult" ("x" "SIN - CPS / (4 * P2)" "y" "P2")) (("1" (expand "abs" -1 3) (("1" (replace -1 -4 rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1) < 2^-(2+p!1)") (("1" (name-replace "DRL1" "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1)") (("1" (case-replace "2 ^ -(1 + p!1)=2*2 ^ -(2 + p!1)") (("1" (rewrite "expt_inverse" 1) (("1" (name-replace "P2" "2 ^ (2 + p!1)") (("1" (hide-all-but (-2 -3 -4 1)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "expt_x2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 -6 1)) (("2" (lemma "both_sides_expt_pos_lt" ("px" "x!1" "py" "1/2" "pm" "3+p!1")) (("2" (assert) (("2" (rewrite "div_mult_pos_lt1") (("2" (rewrite "inv_expt" -1) (("2" (rewrite "expt_inverse" 1) (("2" (name-replace "DRL1" "x!1 ^ (3 + p!1)") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x2") (("2" (rewrite "expt_x3") (("2" (assert) (("2" (lemma "factorial_incr" ("k" "3" "n" "7 + 2 * p!1")) (("2" (rewrite "factorial_3") (("2" (assert) (("2" (lemma "both_sides_times_pos_lt1" ("pz" "1/(4*2^p!1)" "x" "1/2" "y" "factorial(7 + 2 * p!1)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (lemma "div_mult_pos_lt1" ("py" "2^(2+p!1)" "x" "SIN_APPROX" "z" "CPS - 1")) (("2" (lemma "div_mult_pos_lt2" ("py" "2^(2+p!1)" "x" "SIN_APPROX" "z" "CPS+1")) (("2" (assert) (("2" (rewrite "expt_inverse" 1) (("2" (name-replace "P2" "2^(2+p!1)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -5 1)) (("2" (case-replace "(LAMBDA (i_1: nat): IF i_1 = 0 THEN sin_term(1)(i_1) ELSE sin_term(1)(i_1) * x!1 ^ i_1 ENDIF) =(LAMBDA (i: nat): 1 / sqrt(x!1) * sin_term(sqrt(x!1))(i))") (("1" (hide -1 2) (("1" (assert) (("1" (rewrite "sigma_scal") (("1" (expand "sin_term") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "sin_term") (("2" (typepred "factorial(1 + 2 * x!2)") (("2" (name-replace "FACTORIAL" "factorial(1 + 2 * x!2)") (("2" (rewrite "expt_1i") (("2" (rewrite "expt_plus") (("2" (name-replace "SIGN" "(-1) ^ x!2") (("2" (rewrite "expt_x1") (("2" (case-replace "sqrt(x!1) ^ (2 * x!2)=x!1^x!2") (("1" (case-replace "x!2=0") (("1" (assert) (("1" (rewrite "expt_x0") (("1" (replace -2 1 rl) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (lemma "expt_times" ("i" "2" "j" "x!2" "n0x" "sqrt(x!1)")) (("2" (rewrite "expt_x2") (("2" (rewrite "sq_rew") 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" (expand "/=" 1) (("2" (lemma "sqrt_eq_0" ("nnx" "x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/=") (("2" (lemma "sqrt_eq_0" ("nnx" "x!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (hide -1 -2) (("2" (inst + "1") (("2" (lemma "powerseries_lemma" ("x" "0" "cx" "csnx!1" "xs" "sin_term(1)" "cxs" "cauchy_sin_series")) (("2" (lemma "sin_series_lemma") (("2" (replace -1) (("2" (replace -3) (("2" (hide -1 -3) (("2" (expand "cauchy_prop") (("2" (skosimp) (("2" (inst - "2+p!1") (("2" (inst - "2+p!1") (("2" (flatten) (("2" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_sin_series, 2 + p!1)(2 + p!1)") (("2" (case-replace "powerseries(0, sin_term(1), 2 + p!1)=1") (("1" (hide -1) (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (lemma "div_mult_pos_lt2" ("z" "1+CPS" "x" "2^p!1" "py" "4")) (("1" (lemma "div_mult_pos_lt1" ("z" "CPS-1" "x" "2^p!1" "py" "4")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "powerseries") (("2" (case-replace "(LAMBDA (i:nat): IF i = 0 THEN sin_term(1)(i) ELSE sin_term(1)(i) * 0 ^ i ENDIF)=(LAMBDA (i:na (("1" (hide -1) (("1" (assert) (("1" (rewrite "sigma_first") (("1" (lemma "sigma_eq[nat]" ("low" "1" "high" "2+p!1" "F" "(LAMBDA (i: nat): IF i = 0 THEN 1 ELSE 0 ENDIF)" "G" "(LAMBDA (i:nat): 0)")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "sigma_zero") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (case-replace "x!2=0") (("1" (expand "sin_term") (("1" (grind) nil nil)) nil) ("2" (assert) (("2" (expand "^") (("2" (expand "expt") (("2" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real? const-decl "bool" cauchy nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sin const-decl "real" sincos_def "trig_fnd/") (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (cauchy_prop const-decl "bool" cauchy nil) (cauchy_powerseries const-decl "cauchy_real" powerseries nil) (cauchys_real nonempty-type-eq-decl nil sum nil) (cauchys_real? const-decl "bool" sum nil) (powerseries const-decl "real" powerseries nil) (sin_approx const-decl "real" trig_approx "trig_fnd/") (factorial def-decl "posnat" factorial "ints/") (expt_x2 formula-decl nil inv nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (round const-decl "int" prelude_aux nil) (factorial_3 formula-decl nil factorial "ints/") (factorial_incr formula-decl nil factorial "ints/") (sigma_scal formula-decl nil sigma "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sq_rew formula-decl nil sq "reals/") (sqrt_eq_0 formula-decl nil sqrt "reals/") (sin_approx_sin formula-decl nil trig_approx "trig_fnd/") (powerseries_lemma formula-decl nil powerseries nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (sin_term const-decl "real" trig_approx "trig_fnd/") (sigma_nat application-judgement "nat" sum nil) (sigma_eq formula-decl nil sigma "reals/") (sigma_zero formula-decl nil sigma "reals/") (sigma_first formula-decl nil sigma "reals/")) nil)) (cauchy_cos_drx_TCC1 0 (cauchy_cos_drx_TCC1-1 nil 3393418937 ("" (expand "cauchys_real?") (("" (inst + "cos_term(1)") (("" (expand "cauchys_prop") (("" (skosimp) (("" (rewrite "cos_series_lemma") 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (cos_term const-decl "real" trig_approx "trig_fnd/") (cos_series_lemma formula-decl nil sincosx nil) (cauchys_prop const-decl "bool" sum nil) (cauchys_real? const-decl "bool" sum nil)) nil)) (cauchy_cos_drx_TCC2 0 (cauchy_cos_drx_TCC2-2 nil 3508597821 ("" (skosimp) (("" (typepred "csnx!1") (("" (expand "cauchy_nnsreal?") (("" (skosimp) (("" (expand "cauchy_real?") (("" (typepred "x!1") (("" (inst + "cos(sqrt(x!1))") (("" (lemma "powerseries_lemma" ("x" "x!1" "cx" "csnx!1" "cxs" "cauchy_cos_series" "xs" "cos_term(1)")) (("" (lemma "cos_series_lemma") (("" (replace -1 -2) (("" (replace -5 -2) (("" (hide -1 -5) (("" (expand "cauchy_prop") (("" (skosimp) (("" (inst - "2+p!1") (("" (inst - "2+p!1") (("" (flatten) (("" (case-replace "powerseries(x!1, cos_term(1), 2 + p!1)=cos_approx(sqrt(x!1),2+p!1)") (("1" (hide -1) (("1" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_cos_series, 2 + p!1)(2 + p!1)") (("1" (lemma "cos_approx_cos" ("a" "sqrt(x!1)" "n" "2+p!1")) (("1" (name-replace "COS_APPROX" "cos_approx(sqrt(x!1), 2 + p!1)") (("1" (name-replace "COS_" "cos(sqrt(x!1))") (("1" (expand "cos_term") (("1" (rewrite "abs_div") (("1" (rewrite "abs_mult") (("1" (expand "abs" -1 4) (("1" (typepred "factorial(6 + 2 * p!1)") (("1" (assert) (("1" (hide -1) (("1" (lemma "abs_expt" ("n0x" "-1" "i" "3+p!1")) (("1" (expand "abs" -1 1) (("1" (rewrite "expt_1i" -1) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (lemma "expt_times" ("n0x" "sqrt(x!1)" "i" "2" "j" "3+p!1")) (("1" (rewrite "expt_x2") (("1" (rewrite "sq_rew") (("1" (replace -1) (("1" (hide -1) (("1" (expand "abs" -1 2) (("1" (assert) (("1" (lemma "nnreal_exp" ("x" "x!1" "i" "3+p!1")) (("1" (assert) (("1" (case "abs(COS_APPROX-CPS/2^(2+p!1)) < 1/2^(2+p!1)") (("1" (case "x!1 ^ (3 + p!1)/ factorial(6 + 2 * p!1) < 2^-(2+p!1)") (("1" (rewrite "expt_inverse" -2 :dir rl) (("1" (case "abs(COS_*2^p!1-CPS/4) < 1/2") (("1" (hide-all-but (-1 -8 -9 1)) (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (name-replace "DRL1" "COS_ * 2 ^ p!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "abs_mult" ("x" "COS_-CPS/2^(2+p!1)" "y" "2^p!1")) (("2" (expand "abs" -1 3) (("2" (rewrite "expt_plus" -1) (("2" (rewrite "expt_x2") (("2" (lemma "div_cancel1" ("n0z" "2^p!1" "x" "CPS/4")) (("2" (rewrite "div_div2" -1) (("2" (replace -1) (("2" (replace -2 1) (("2" (hide -1 -2) (("2" (lemma "div_mult_pos_lt2" ("z" "1/2" "py" "2^p!1" "x" "abs(COS_ - (CPS / (4 * 2 ^ p!1)))")) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (case "abs(COS_ - (CPS / (4 * 2 ^ p!1))) < 2*2^-(2+p!1)") (("1" (case-replace "2 * 2 ^ -(2 + p!1)=1/2 / 2 ^ p!1") (("1" (hide-all-but 1) (("1" (rewrite "expt_inverse") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name-replace "DRL1" "CPS / (4 * 2 ^ p!1)") (("2" (name-replace "DRL2" "x!1 ^ (3 + p!1) / factorial(6 + 2 * p!1)") (("2" (assert) (("2" (name-replace "DRL3" "2 ^ (-(2 + p!1))") (("2" (hide-all-but (-1 -2 -4 1)) (("2" (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) ("2" (hide-all-but (-6 -7 1)) (("2" (expand "<=" -1) (("2" (split) (("1" (lemma "both_sides_expt_pos_lt" ("px" "x!1" "pm" "2+p!1" "py" "1/2")) (("1" (assert) (("1" (lemma "inv_expt") (("1" (inst -1 "(2+p!1)" "2") (("1" (replaces -1) (("1" (rewrite "expt_inverse" 1) (("1" (assert) (("1" (lemma "expt_plus" ("n0x" "2" "i" "1" "j" "2+p!1")) (("1" (rewrite "expt_x1") (("1" (rewrite "div_mult_pos_lt1" 1) (("1" (lemma "factorial_incr" ("k" "2" "n" "6 + 2 * p!1")) (("1" (assert) (("1" (rewrite "factorial_2") (("1" (assert) (("1" (lemma "expt_plus" ("n0x" "x!1" "i" "1" "j" "2+p!1")) (("1" (rewrite "expt_x1") (("1" (replace -1) (("1" (assert) (("1" (lemma "lt_times_lt_pos1" ("px" "x!1" "y" "1/2" "nnz" "x!1 ^ (2 + p!1)" "w" "1 / 2 ^ (2 + p!1)")) (("1" (assert) (("1" (name-replace "LHS" "x!1 * x!1 ^ (2 + p!1)") (("1" (lemma "both_sides_times_pos_le1" ("pz" "1 / 2 * (1 / 2 ^ (2 + p!1))" "x" "2" "y" "factorial(6 + 2 * p!1)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (expand "^" 1 1) (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -4 1)) (("2" (rewrite "div_mult_pos_lt2" 1) (("2" (lemma "abs_mult" ("x" "COS_APPROX - CPS / 2 ^ (2 + p!1)" "y" "2 ^ (2 + p!1)")) (("2" (expand "abs" -1 3) (("2" (rewrite "div_cancel1") (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (name-replace "P2" "2^(2+p!1)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/=" 1) (("2" (replace -1) (("2" (expand "COS_") (("2" (replace -1) (("2" (rewrite "cos_0") (("2" (expand "COS_APPROX") (("2" (replace -1) (("2" (rewrite "cos_approx_a0") (("2" (hide-all-but (-3 -4 1 -1)) (("2" (expand "round") (("2" (typepred "floor(1 / 2 + CPS / 4)") (("2" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("2" (lemma "both_sides_div_pos_lt1" ("pz" "4" "x" "CPS-1" "y" "2^(2+p!1)")) (("2" (lemma "both_sides_div_pos_lt1" ("pz" "4" "y" "CPS+1" "x" "2^(2+p!1)")) (("2" (flatten) (("2" (hide -1 -3) (("2" (split -1) (("1" (split -2) (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -4 1)) (("2" (expand "cos_approx") (("2" (expand "powerseries") (("2" (expand "cos_term") (("2" (case-replace "(LAMBDA (i:nat): IF i = 0 THEN 1 ELSE (-1) ^ i * 1 ^ (2 * i) / factorial(2 * i) * x!1 ^ i ENDIF)=(LAMBDA (n:nat): IF n = 0 THEN 1 ELSE (-1) ^ n * sqrt(x!1) ^ (2 * n) / factorial(2 * n) ENDIF)") (("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (case-replace "x!2=0") (("2" (assert) (("2" (rewrite "expt_1i") (("2" (rewrite "expt_times") (("1" (rewrite "expt_x2") (("1" (rewrite "sq_rew") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "/=" 1) (("2" (replace -1) (("2" (lemma "sqrt_eq_0" ("nnx" "x!1")) (("2" (split -1) (("1" (replace -1) (("1" (expand "^" 2 4) (("1" (expand "^" 2 2) (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_nnsreal nonempty-type-eq-decl nil sincosx nil) (cauchy_nnsreal? const-decl "bool" sincosx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (nnsreal nonempty-type-eq-decl nil sincosx nil) (powerseries_lemma formula-decl nil powerseries nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_cos_series const-decl "cauchy_real" sincosx nil) (cos_term const-decl "real" trig_approx "trig_fnd/") (cos_approx const-decl "real" trig_approx "trig_fnd/") (powerseries const-decl "real" powerseries nil) (cauchy_powerseries const-decl "cauchy_real" powerseries nil) (cauchys_real nonempty-type-eq-decl nil sum nil) (cauchys_real? const-decl "bool" sum nil) (abs_mult formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (expt_times formula-decl nil exponentiation nil) (sq_rew formula-decl nil sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_sqrt formula-decl nil sqrt "reals/") (posint nonempty-type-eq-decl nil integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (round const-decl "int" prelude_aux nil) (minus_real_is_real application-judgement "real" reals nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (expt_plus formula-decl nil exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (div_cancel1 formula-decl nil real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (posrat nonempty-type-eq-decl nil rationals nil) (posreal nonempty-type-eq-decl nil real_types nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (div_div2 formula-decl nil real_props nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (expt_inverse formula-decl nil exponentiation nil) (expt def-decl "real" exponentiation nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nat_expt application-judgement "nat" exponentiation nil) (both_sides_expt_pos_lt formula-decl nil exponentiation nil) (inv_expt formula-decl nil exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (factorial_incr formula-decl nil factorial "ints/") (factorial_2 formula-decl nil factorial "ints/") (lt_times_lt_pos1 formula-decl nil real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (div_mult_pos_lt1 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 "[numfield, numfield -> numfield]" number_fields nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nnreal_exp judgement-tcc nil exponentiation nil) (expt_x2 formula-decl nil inv nil) (nat_exp application-judgement "nat" exponentiation nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (COS_APPROX skolem-const-decl "real" sincosx nil) (cos_approx_a0 formula-decl nil trig_approx "trig_fnd/") (both_sides_div_pos_lt1 formula-decl nil real_props nil) (cos_0 formula-decl nil trig_basic "trig_fnd/") (COS_ skolem-const-decl "trig_range" sincosx nil) (expt_1i formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (abs_expt formula-decl nil exponentiation nil) (real_gt_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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_times_int_is_int application-judgement "int" integers 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) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (abs_div formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/") (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (trig_range type-eq-decl nil sincos_def "trig_fnd/") (cos_approx_cos formula-decl nil trig_approx "trig_fnd/") (real_minus_real_is_real application-judgement "real" reals nil) (sqrt_eq_0 formula-decl nil sqrt "reals/") (sqrt_0 formula-decl nil sqrt "reals/") (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (cauchy_prop const-decl "bool" cauchy nil) (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (posint_exp application-judgement "posint" exponentiation nil) (cos_series_lemma formula-decl nil sincosx nil) (cos const-decl "real" sincos_def "trig_fnd/") (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/") (cauchy_real? const-decl "bool" cauchy nil)) nil) (cauchy_cos_drx_TCC2-1 nil 3393418937 ("" (skosimp) (("" (typepred "csnx!1") (("" (expand "cauchy_nnsreal?") (("" (skosimp) (("" (expand "cauchy_real?") (("" (typepred "x!1") (("" (inst + "cos(sqrt(x!1))") (("" (lemma "powerseries_lemma" ("x" "x!1" "cx" "csnx!1" "cxs" "cauchy_cos_series" "xs" "cos_term(1)")) (("" (lemma "cos_series_lemma") (("" (replace -1 -2) (("" (replace -5 -2) (("" (hide -1 -5) (("" (expand "cauchy_prop") (("" (skosimp) (("" (inst - "2+p!1") (("" (inst - "2+p!1") (("" (flatten) (("" (case-replace "powerseries(x!1, cos_term(1), 2 + p!1)=cos_approx(sqrt(x!1),2+p!1)") (("1" (hide -1) (("1" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_cos_series, 2 + p!1)(2 + p!1)") (("1" (lemma "cos_approx_cos" ("a" "sqrt(x!1)" "n" "2+p!1")) (("1" (name-replace "COS_APPROX" "cos_approx(sqrt(x!1), 2 + p!1)") (("1" (name-replace "COS" "cos(sqrt(x!1))") (("1" (expand "cos_term") (("1" (rewrite "abs_div") (("1" (rewrite "abs_mult") (("1" (expand "abs" -1 4) (("1" (lemma "abs_expt" ("n0x" "-1" "i" "3+p!1")) (("1" (expand "abs" -1 1) (("1" (rewrite "expt_1i" -1) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (lemma "expt_times" ("n0x" "sqrt(x!1)" "i" "2" "j" "3+p!1")) (("1" (rewrite "expt_x2") (("1" (rewrite "sq_rew") (("1" (replace -1) (("1" (hide -1) (("1" (expand "abs" -1 2) (("1" (assert) (("1" (lemma "nnreal_exp" ("x" "x!1" "i" "3+p!1")) (("1" (assert) (("1" (case "abs(COS_APPROX-CPS/2^(2+p!1)) < 1/2^(2+p!1)") (("1" (case "x!1 ^ (3 + p!1)/ factorial(6 + 2 * p!1) < 2^-(2+p!1)") (("1" (rewrite "expt_inverse" -2 :dir rl) (("1" (case "abs(COS*2^p!1-CPS/4) < 1/2") (("1" (hide-all-but (-1 -8 -9 1)) (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (name-replace "DRL1" "COS * 2 ^ p!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "abs_mult" ("x" "COS-CPS/2^(2+p!1)" "y" "2^p!1")) (("2" (expand "abs" -1 3) (("2" (rewrite "expt_plus" -1) (("2" (rewrite "expt_x2") (("2" (lemma "div_cancel1" ("n0z" "2^p!1" "x" "CPS/4")) (("2" (rewrite "div_div2" -1) (("2" (replace -1) (("2" (replace -2 1) (("2" (hide -1 -2) (("2" (lemma "div_mult_pos_lt2" ("z" "1/2" "py" "2^p!1" "x" "abs(COS - (CPS / (4 * 2 ^ p!1)))")) (("2" (replace -1 1 rl) (("2" (rewrite "div_div2" 1) (("2" (hide -1) (("2" (case "abs(COS - (CPS / (4 * 2 ^ p!1))) < 2*2^-(2+p!1)") (("1" (case-replace "2 * 2 ^ -(2 + p!1)=1 / (2 * 2 ^ p!1)") (("1" (hide-all-but 1) (("1" (rewrite "expt_inverse") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name-replace "DRL1" "CPS / (4 * 2 ^ p!1)") (("2" (name-replace "DRL2" "x!1 ^ (3 + p!1) / factorial(6 + 2 * p!1)") (("2" (assert) (("2" (name-replace "DRL3" "2 ^ (-(2 + p!1))") (("2" (hide-all-but (-1 -2 -4 1)) (("2" (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) ("2" (hide-all-but (-6 -7 1)) (("2" (expand "<=" -1) (("2" (split) (("1" (lemma "both_sides_expt_pos_lt" ("px" "x!1" "pm" "2+p!1" "py" "1/2")) (("1" (assert) (("1" (rewrite "inv_expt") (("1" (rewrite "expt_inverse" 1) (("1" (assert) (("1" (lemma "expt_plus" ("n0x" "2" "i" "1" "j" "2+p!1")) (("1" (rewrite "expt_x1") (("1" (rewrite "div_mult_pos_lt1" 1) (("1" (lemma "factorial_incr" ("k" "2" "n" "6 + 2 * p!1")) (("1" (assert) (("1" (rewrite "factorial_2") (("1" (assert) (("1" (lemma "expt_plus" ("n0x" "x!1" "i" "1" "j" "2+p!1")) (("1" (rewrite "expt_x1") (("1" (replace -1) (("1" (assert) (("1" (lemma "lt_times_lt_pos1" ("px" "x!1" "y" "1/2" "nnz" "x!1 ^ (2 + p!1)" "w" "1 / 2 ^ (2 + p!1)")) (("1" (assert) (("1" (name-replace "LHS" "x!1 * x!1 ^ (2 + p!1)") (("1" (lemma "both_sides_times_pos_le1" ("pz" "1 / 2 * (1 / 2 ^ (2 + p!1))" "x" "2" "y" "factorial(6 + 2 * p!1)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (expand "^" 1 1) (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -4 1)) (("2" (rewrite "div_mult_pos_lt2" 1) (("2" (lemma "abs_mult" ("x" "COS_APPROX - CPS / 2 ^ (2 + p!1)" "y" "2 ^ (2 + p!1)")) (("2" (expand "abs" -1 3) (("2" (rewrite "div_cancel1") (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (name-replace "P2" "2^(2+p!1)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "/=" 1) (("2" (replace -1) (("2" (expand "COS") (("2" (replace -1) (("2" (rewrite "cos_0") (("2" (expand "COS_APPROX") (("2" (replace -1) (("2" (rewrite "cos_approx_a0") (("2" (hide-all-but (-3 -4 1 -1)) (("2" (expand "round") (("2" (typepred "floor(1 / 2 + CPS / 4)") (("2" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("2" (lemma "both_sides_div_pos_lt1" ("pz" "4" "x" "CPS-1" "y" "2^(2+p!1)")) (("2" (lemma "both_sides_div_pos_lt1" ("pz" "4" "y" "CPS+1" "x" "2^(2+p!1)")) (("2" (flatten) (("2" (hide -1 -3) (("2" (split -1) (("1" (split -2) (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -4 1)) (("2" (expand "cos_approx") (("2" (expand "powerseries") (("2" (expand "cos_term") (("2" (case-replace "(LAMBDA (i:nat): IF i = 0 THEN 1 ELSE (-1) ^ i * 1 ^ (2 * i) / factorial(2 * i) * x!1 ^ i ENDIF)=(LAMBDA (n:nat): IF n = 0 THEN 1 ELSE (-1) ^ n * sqrt(x!1) ^ (2 * n) / factorial(2 * n) ENDIF)") (("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (case-replace "x!2=0") (("2" (assert) (("2" (rewrite "expt_1i") (("2" (rewrite "expt_times") (("1" (rewrite "expt_x2") (("1" (rewrite "sq_rew") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "/=" 1) (("2" (replace -1) (("2" (lemma "sqrt_eq_0" ("nnx" "x!1")) (("2" (split -1) (("1" (replace -1) (("1" (expand "^" 2 4) (("1" (expand "^" 2 2) (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((powerseries_lemma formula-decl nil powerseries nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cos_term const-decl "real" trig_approx "trig_fnd/") (cos_approx const-decl "real" trig_approx "trig_fnd/") (powerseries const-decl "real" powerseries nil) (cauchy_powerseries const-decl "cauchy_real" powerseries nil) (cauchys_real nonempty-type-eq-decl nil sum nil) (cauchys_real? const-decl "bool" sum nil) (cos_0 formula-decl nil trig_basic "trig_fnd/") (cos_approx_a0 formula-decl nil trig_approx "trig_fnd/") (expt_x2 formula-decl nil inv nil) (factorial_2 formula-decl nil factorial "ints/") (factorial_incr formula-decl nil factorial "ints/") (round const-decl "int" prelude_aux nil) (sq_sqrt formula-decl nil sqrt "reals/") (sq_rew formula-decl nil sq "reals/") (factorial def-decl "posnat" factorial "ints/") (trig_range type-eq-decl nil sincos_def "trig_fnd/") (cos_approx_cos formula-decl nil trig_approx "trig_fnd/") (sqrt_eq_0 formula-decl nil sqrt "reals/") (sqrt_0 formula-decl nil sqrt "reals/") (cauchy_prop const-decl "bool" cauchy nil) (cos_range application-judgement "trig_range" sincos_def "trig_fnd/") (cos const-decl "real" sincos_def "trig_fnd/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (cauchy_real? const-decl "bool" cauchy nil)) nil)) (sin_drx_lemma_TCC1 0 (sin_drx_lemma_TCC1-1 nil 3393767043 ("" (subtype-tcc) nil 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) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (cauchy_nnsreal? const-decl "bool" sincosx nil) (cauchy_nnsreal nonempty-type-eq-decl nil sincosx nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (nnsreal nonempty-type-eq-decl nil sincosx 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) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (cauchy_prop const-decl "bool" cauchy nil) (posnat_expt application-judgement "posnat" exponentiation nil)) nil)) (sin_drx_lemma 0 (sin_drx_lemma-5 nil 3508598816 ("" (skosimp) (("" (typepred "snx!1") (("" (expand "<=" -1) (("" (split -1) (("1" (hide 1) (("1" (expand "cauchy_sin_drx") (("1" (lemma "powerseries_lemma" ("x" "snx!1" "cx" "csnx!1" "xs" "sin_term(1)" "cxs" "cauchy_sin_series")) (("1" (lemma "sin_series_lemma") (("1" (replace -1) (("1" (replace -5) (("1" (hide -1) (("1" (expand "cauchy_prop" (-1 1)) (("1" (skosimp) (("1" (inst - "2+p!1") (("1" (inst - "2+p!1") (("1" (flatten) (("1" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_sin_series, 2 + p!1)(2 + p!1)") (("1" (lemma "sin_approx_sin" ("a" "sqrt(snx!1)" "n" "2+p!1")) (("1" (lemma "both_sides_div_pos_le1" ("pz" "sqrt(snx!1)" "x" "abs(sin(sqrt(snx!1)) - sin_approx(sqrt(snx!1), 2 + p!1))" "y" "abs(sin_term(sqrt(snx!1))(2 + p!1 + 1))")) (("1" (assert) (("1" (hide -2) (("1" (lemma "abs_div" ("x" "sin(sqrt(snx!1)) - sin_approx(sqrt(snx!1), 2 + p!1)" "n0y" "sqrt(snx!1)")) (("1" (expand "abs" -1 3) (("1" (rewrite "minus_div2" -1 :dir rl) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (case-replace "sin_approx(sqrt(snx!1), 2 + p!1) / sqrt(snx!1)=powerseries(snx!1, sin_term(1), 2 + p!1)" (("1" (hide -1) (("1" (name-replace "SIN_APPROX" "powerseries(snx!1, sin_term(1), 2 + p!1)") (("1" (name-replace "SIN_" "sin(sqrt(snx!1)) / sqrt(snx!1)") (("1" (case "abs((SIN_ - SIN_APPROX)) <=2^-(2+p!1)") (("1" (hide -2) (("1" (case "abs(SIN_APPROX-CPS/2^(2+p!1))<2^-(2+p!1)") (("1" (case "abs(SIN_-CPS / 2 ^ (2 + p!1)) < 2 ^ -(1 + p!1)") (("1" (hide -2 -3 -4 -5 -8) (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (lemma "abs_mult" ("x" "SIN_ - CPS / 2 ^ (2 + p!1)" "y" "2^p!1")) (("1" (expand "abs" -1 3) (("1" (lemma "div_cancel1" ("n0z" "2^p!1" "x" "CPS/4")) (("1" (rewrite "div_div2") (("1" (rewrite "expt_plus" -2) (("1" (rewrite "expt_x2") (("1" (replace -1 -2) (("1" (case "abs(2 ^ p!1 * SIN_ - CPS / 4)<1/2") (("1" (hide -2 -3 -6 -7 -8) (("1" (name-replace "P2" "2^p!1") (("1" (grind) nil nil)) nil)) nil) ("2" (replace -2) (("2" (name-replace "LHS" "abs(SIN_ - CPS / (4 * 2 ^ p!1))") (("2" (hide-all-but (-5 1)) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "div_mult_pos_lt2") (("2" (grind) (("2" (grind-reals) 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" (name-replace "DRL1" "CPS / 2 ^ (2 + p!1)") (("2" (hide-all-but (-1 -2 1)) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "expt_x2") (("2" (name-replace "P2" "2^p!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1 -4 -5)) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x2") (("2" (lemma "div_mult_pos_lt1" ("py" "4*2^p!1" "z" "CPS-1" "x" "SIN_APPROX")) (("2" (lemma "div_mult_pos_lt2" ("py" "4*2^p!1" "z" "CPS+1" "x" "SIN_APPROX")) (("2" (assert) (("2" (name-replace "P2" "2^p!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "abs(sin_term(sqrt(snx!1))(3 + p!1)) / sqrt(snx!1)<2 ^ -(2 + p!1)") (("1" (assert) nil nil) ("2" (hide-all-but (-4 -5 1)) (("2" (expand "sin_term") (("2" (rewrite "abs_div") (("2" (rewrite "abs_mult") (("2" (rewrite "abs_expt" 1 :dir rl) (("2" (expand "abs" 1 1) (("2" (rewrite "expt_1i" 1) (("2" (expand "abs" 1 2) (("2" (typepred "factorial(7 + 2 * p!1)") (("2" (assert) (("2" (hide -1) (("2" (lemma "expt_plus" ("n0x" "sqrt(snx!1)" "i" "1" "j" "6+2*p!1")) (("2" (rewrite "expt_x1") (("2" (lemma "expt_times" ("n0x" "sqrt(snx!1)" "i" "2" "j" "3+p!1")) (("2" (rewrite "expt_x2") (("2" (rewrite "sq_rew") (("2" (replace -1) (("2" (replace -2) (("2" (rewrite "abs_mult") (("2" (expand "abs" 1 1) (("2" (expand "abs" 1 1) (("2" (assert) (("2" (hide -1 -2) (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("n0z" "sqrt(snx!1)" "x" "snx!1^(3+p!1)/factorial(7 + 2 * p!1)")) (("2" (replace -1 1) (("2" (hide -1) (("2" (rewrite "div_mult_pos_lt1") (("2" (lemma "both_sides_expt_pos_lt" ("px" "snx!1" "py" "1/2" "pm" "3+p!1")) (("2" (assert) (("2" (lemma "inv_expt") (("2" (inst -1 "3+p!1" "2") (("2" (replaces -1) (("2" (rewrite "expt_inverse" 1) (("2" (case "1 / 2 ^ (3 + p!1)<1 / (2 ^ (2 + p!1)) * factorial(7 + 2 * p!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "both_sides_times_pos_lt1" ("pz" "2 ^ (3 + p!1)" "x" "1 / 2 ^ (3 + p!1)" "y" "1 / (2 ^ (2 + p!1)) * factorial(7 + 2 * p!1)")) (("2" (rewrite "div_cancel2") (("2" (replace -1 1 rl) (("2" (hide -1 -2) (("2" (lemma "expt_inverse" ("n0x" "2" "i" "2+p!1")) (("2" (replace -1 1 rl) (("2" (assert) (("2" (lemma "expt_plus" ("n0x" "2" "i" "-(2+p!1)" "j" "3+p!1")) (("2" (rewrite "associative_mult" 1 :dir rl) (("2" (replace -1 1 rl) (("2" (assert) (("2" (rewrite "expt_x1") (("2" (lemma "factorial_incr" ("k" "2" "n" "7+2*p!1")) (("2" (rewrite "factorial_2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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-all-but (-4 -5 1)) (("2" (expand "powerseries") (("2" (expand "sin_approx") (("2" (lemma "sigma_scal" ("a" "1/sqrt(snx!1)" "F" "sin_term(sqrt(snx!1))" "low" "0" "high" "2+p!1")) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (case-replace "(LAMBDA (i: nat): 1 / sqrt(snx!1) * sin_term(sqrt(snx!1))(i)) = (LAMBDA (i_1: nat): IF i_1 = 0 THEN sin_term(1)(i_1) ELSE sin_term(1)(i_1) * snx!1 ^ i_1 ENDIF)") (("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "sin_term") (("2" (name-replace "SGN" "(-1) ^ x!1") (("2" (name-replace "FACTORIAL" "factorial(1 + 2 * x!1)") (("2" (rewrite "expt_1i") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "expt_times") (("2" (rewrite "expt_x2") (("2" (rewrite "sq_rew") (("2" (case-replace "x!1=0") (("1" (rewrite "expt_x0") (("1" (assert) nil nil)) nil) ("2" (replace 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqrt_pos" ("px" "snx!1")) (("1" (propax) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((nnsreal nonempty-type-eq-decl nil sincosx nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (cauchy_sin_drx const-decl "cauchy_real" sincosx nil) (sin_series_lemma formula-decl nil sincosx nil) (sin_range application-judgement "trig_range" sincos_def "trig_fnd/") (posint_exp application-judgement "posint" exponentiation nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_approx_sin formula-decl nil trig_approx "trig_fnd/") (nonneg_real nonempty-type-eq-decl nil real_types 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/") (sqrt_pos judgement-tcc nil sqrt "reals/") (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers 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) (abs_div formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (minus_div2 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (expt_x0 formula-decl nil exponentiation nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma_scal formula-decl nil sigma "reals/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (expt_times formula-decl nil exponentiation nil) (sq_rew formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (div_cancel2 formula-decl nil real_props nil) (factorial_2 formula-decl nil factorial "ints/") (factorial_incr formula-decl nil factorial "ints/") (associative_mult formula-decl nil number_fields nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (inv_expt formula-decl nil exponentiation nil) (both_sides_expt_pos_lt formula-decl nil exponentiation nil) (expt_1i formula-decl nil exponentiation nil) (abs_expt formula-decl nil exponentiation nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/") (div_mult_pos_lt1 formula-decl nil real_props nil) (round const-decl "int" prelude_aux nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (div_div2 formula-decl nil real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_times_int_is_int application-judgement "int" integers nil) (expt_x2 formula-decl nil inv nil) (posint nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (minus_real_is_real application-judgement "real" reals nil) (expt_inverse formula-decl nil exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (div_cancel1 formula-decl nil real_props nil) (abs_mult formula-decl nil real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (rat nonempty-type-eq-decl nil rationals nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (powerseries const-decl "real" powerseries nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sin_approx const-decl "real" trig_approx "trig_fnd/") (sin const-decl "real" sincos_def "trig_fnd/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (both_sides_div_pos_le1 formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (cauchys_real? const-decl "bool" sum nil) (cauchys_real nonempty-type-eq-decl nil sum nil) (cauchy_powerseries const-decl "cauchy_real" powerseries nil) (powerseries_lemma formula-decl nil powerseries nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_nnsreal? const-decl "bool" sincosx nil) (cauchy_nnsreal nonempty-type-eq-decl nil sincosx nil) (cauchy_sin_series const-decl "cauchy_real" sincosx nil) (sin_term const-decl "real" trig_approx "trig_fnd/")) nil) (sin_drx_lemma-4 nil 3508597408 ("" (skosimp) (("" (typepred "snx!1") (("" (expand "<=" -1) (("" (split -1) (("1" (hide 1) (("1" (expand "cauchy_sin_drx") (("1" (lemma "powerseries_lemma" ("x" "snx!1" "cx" "csnx!1" "xs" "sin_term(1)" "cxs" "cauchy_sin_series")) (("1" (lemma "sin_series_lemma") (("1" (replace -1) (("1" (replace -5) (("1" (hide -1) (("1" (expand "cauchy_prop" (-1 1)) (("1" (skosimp) (("1" (inst - "2+p!1") (("1" (inst - "2+p!1") (("1" (flatten) (("1" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_sin_series, 2 + p!1)(2 + p!1)") (("1" (lemma "sin_approx_sin" ("a" "sqrt(snx!1)" "n" "2+p!1")) (("1" (lemma "both_sides_div_pos_le1" ("pz" "sqrt(snx!1)" "x" "abs(sin(sqrt(snx!1)) - sin_approx(sqrt(snx!1), 2 + p!1))" "y" "abs(sin_term(sqrt(snx!1))(2 + p!1 + 1))")) (("1" (assert) (("1" (hide -2) (("1" (lemma "abs_div" ("x" "sin(sqrt(snx!1)) - sin_approx(sqrt(snx!1), 2 + p!1)" "n0y" "sqrt(snx!1)")) (("1" (expand "abs" -1 3) (("1" (rewrite "minus_div2" -1 :dir rl) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (case-replace "sin_approx(sqrt(snx!1), 2 + p!1) / sqrt(snx!1)=powerseries(snx!1, sin_term(1), 2 + p!1)" (("1" (hide -1) (("1" (name-replace "SIN_APPROX" "powerseries(snx!1, sin_term(1), 2 + p!1)") (("1" (name-replace "SIN_" "sin(sqrt(snx!1)) / sqrt(snx!1)") (("1" (case "abs((SIN_ - SIN_APPROX)) <=2^-(2+p!1)") (("1" (hide -2) (("1" (case "abs(SIN_APPROX-CPS/2^(2+p!1))<2^-(2+p!1)") (("1" (case "abs(SIN_-CPS / 2 ^ (2 + p!1)) < 2 ^ -(1 + p!1)") (("1" (hide -2 -3 -4 -5 -8) (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (lemma "abs_mult" ("x" "SIN_ - CPS / 2 ^ (2 + p!1)" "y" "2^p!1")) (("1" (expand "abs" -1 3) (("1" (lemma "div_cancel1" ("n0z" "2^p!1" "x" "CPS/4")) (("1" (rewrite "div_div2") (("1" (rewrite "expt_plus" -2) (("1" (rewrite "expt_x2") (("1" (replace -1 -2) (("1" (case "abs(2 ^ p!1 * SIN_ - CPS / 4)<1/2") (("1" (hide -2 -3 -6 -7 -8) (("1" (name-replace "P2" "2^p!1") (("1" (grind) nil nil)) nil)) nil) ("2" (replace -2) (("2" (name-replace "LHS" "abs(SIN_ - CPS / (4 * 2 ^ p!1))") (("2" (hide-all-but (-5 1)) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "div_mult_pos_lt2") (("2" (rewrite "div_mult_pos_lt2") 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" (name-replace "DRL1" "CPS / 2 ^ (2 + p!1)") (("2" (hide-all-but (-1 -2 1)) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "expt_x2") (("2" (name-replace "P2" "2^p!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1 -4 -5)) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x2") (("2" (lemma "div_mult_pos_lt1" ("py" "4*2^p!1" "z" "CPS-1" "x" "SIN_APPROX")) (("2" (lemma "div_mult_pos_lt2" ("py" "4*2^p!1" "z" "CPS+1" "x" "SIN_APPROX")) (("2" (assert) (("2" (name-replace "P2" "2^p!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "abs(sin_term(sqrt(snx!1))(3 + p!1)) / sqrt(snx!1)<2 ^ -(2 + p!1)") (("1" (assert) nil nil) ("2" (hide-all-but (-4 -5 1)) (("2" (expand "sin_term") (("2" (rewrite "abs_div") (("2" (rewrite "abs_mult") (("2" (rewrite "abs_expt" 1 :dir rl) (("2" (expand "abs" 1 1) (("2" (rewrite "expt_1i" 1) (("2" (expand "abs" 1 2) (("2" (lemma "expt_plus" ("n0x" "sqrt(snx!1)" "i" "1" "j" "6+2*p!1")) (("2" (rewrite "expt_x1") (("2" (lemma "expt_times" ("n0x" "sqrt(snx!1)" "i" "2" "j" "3+p!1")) (("2" (rewrite "expt_x2") (("2" (rewrite "sq_rew") (("2" (replace -1) (("2" (replace -2) (("2" (rewrite "abs_mult") (("2" (expand "abs" 1 1) (("2" (expand "abs" 1 1) (("2" (assert) (("2" (hide -1 -2) (("2" (rewrite "div_div2") (("2" (lemma "div_cancel1" ("n0z" "sqrt(snx!1)" "x" "snx!1^(3+p!1)/factorial(7 + 2 * p!1)")) (("2" (replace -1 1) (("2" (hide -1) (("2" (rewrite "div_mult_pos_lt1") (("2" (lemma "both_sides_expt_pos_lt" ("px" "snx!1" "py" "1/2" "pm" "3+p!1")) (("2" (assert) (("2" (rewrite "inv_expt" -1) (("2" (rewrite "expt_inverse" 1) (("2" (case "1 / 2 ^ (3 + p!1)<1 / (2 ^ (2 + p!1)) * factorial(7 + 2 * p!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "both_sides_times_pos_lt1" ("pz" "2 ^ (3 + p!1)" "x" "1 / 2 ^ (3 + p!1)" "y" "1 / (2 ^ (2 + p!1)) * factorial(7 + 2 * p!1)")) (("2" (rewrite "div_cancel2") (("2" (replace -1 1 rl) (("2" (hide -1 -2) (("2" (lemma "expt_inverse" ("n0x" "2" "i" "2+p!1")) (("2" (replace -1 1 rl) (("2" (assert) (("2" (lemma "expt_plus" ("n0x" "2" "i" "-(2+p!1)" "j" "3+p!1")) (("2" (rewrite "associative_mult" 1 :dir rl) (("2" (replace -1 1 rl) (("2" (assert) (("2" (rewrite "expt_x1") (("2" (lemma "factorial_incr" ("k" "2" "n" "7+2*p!1")) (("2" (rewrite "factorial_2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-4 -5 1)) (("2" (expand "powerseries") (("2" (expand "sin_approx") (("2" (hide -1) (("2" (case-replace "(LAMBDA (i: nat): 1 / sqrt(snx!1) * sin_term(sqrt(snx!1))(i)) = (LAMBDA (i_1: nat): IF i_1 = 0 THEN sin_term(1)(i_1) ELSE sin_term(1)(i_1) * snx!1 ^ i_1 ENDIF)") (("1" (expand "sin_term") (("1" (name-replace "SGN" "(-1) ^ snx!1") (("1" (name-replace "FACTORIAL" "factorial(1 + 2 * snx!1)") (("1" (case-replace "snx!1=0") (("1" (assert) nil nil) ("2" (assert) (("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sqrt_pos" ("px" "snx!1")) (("1" (propax) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) nil nil) (sin_drx_lemma-3 nil 3508597344 (";;; Proof sin_drx_lemma-2 for formula sincosx.sin_drx_lemma" (skosimp) ((";;; Proof sin_drx_lemma-2 for formula sincosx.sin_drx_lemma" (typepred "snx!1") ((";;; Proof sin_drx_lemma-2 for formula sincosx.sin_drx_lemma" (expand "<=" -1) ((";;; Proof sin_drx_lemma-2 for formula sincosx.sin_drx_lemma" (split -1) (("1" (hide 1) (("1" (expand "cauchy_sin_drx") (("1" (lemma "powerseries_lemma" ("x" "snx!1" "cx" "csnx!1" "xs" "sin_term(1)" "cxs" "cauchy_sin_series")) (("1" (lemma "sin_series_lemma") (("1" (replace -1) (("1" (replace -5) (("1" (hide -1) (("1" (expand "cauchy_prop" (-1 1)) (("1" (skosimp) (("1" (inst - "2+p!1") (("1" (inst - "2+p!1") (("1" (flatten) (("1" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_sin_series, 2 + p!1)(2 + p!1)") (("1" (lemma "sin_approx_sin" ("a" "sqrt(snx!1)" "n" "2+p!1")) (("1" (lemma "both_sides_div_pos_le1" ("pz" "sqrt(snx!1)" "x" "abs(sin(sqrt(snx!1)) - sin_approx(sqrt(snx!1), 2 + p!1))" "y" "abs(sin_term(sqrt(snx!1))(2 + p!1 + 1))")) (("1" (assert) (("1" (hide -2) (("1" (lemma "abs_div" ("x" "sin(sqrt(snx!1)) - sin_approx(sqrt(snx!1), 2 + p!1)" "n0y" "sqrt(snx!1)")) (("1" (expand "abs" -1 3) (("1" (rewrite "minus_div2" -1 :dir rl) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (case-replace "sin_approx(sqrt(snx!1), 2 + p!1) / sqrt(snx!1)=powerseries(snx!1, sin_term(1), 2 + p!1)" (("1" (hide -1) (("1" (name-replace "SIN_APPROX" "powerseries(snx!1, sin_term(1), 2 + p!1)") (("1" (name-replace "SIN_" "sin(sqrt(snx!1)) / sqrt(snx!1)") (("1" (case "abs((SIN_ - SIN_APPROX)) <=2^-(2+p!1)") (("1" (hide -2) (("1" (case "abs(SIN_APPROX-CPS/2^(2+p!1))<2^-(2+p!1)") (("1" (case "abs(SIN_-CPS / 2 ^ (2 + p!1)) < 2 ^ -(1 + p!1)") (("1" (hide -2 -3 -4 -5 -8) (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (lemma --> -------------------- --> maximum size reached --> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.702Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26