|
(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"
--> --------------------
--> maximum size reached
--> --------------------
[ Verzeichnis aufwärts0.21unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
