|
(exp_approx
(exp_neg_le1_bounds 0
(exp_neg_le1_bounds-3 nil 3307800311
("" (skosimp)
(("" (case "exp(x!1) < exp_neg_le1_ub(n!1, x!1)")
(("1" (assert)
(("1" (expand "exp_neg_le1_ub")
(("1" (expand "exp_neg_le1_lb")
(("1" (lemma "exp_taylors_err")
(("1" (inst - "2*n!1" "x!1")
(("1" (expand "abs")
(("1" (assert)
(("1"
(case "(max(exp(x!1), 1) * (-x!1) ^ (1 + 2 * n!1)) <= 1")
(("1" (mult-by -1 "1/factorial(1+2*n!1)")
(("1" (assert) nil nil)) nil)
("2" (assert)
(("2"
(case "FORALL (aa,bb:nnreal): aa<=1 AND bb<=1 IMPLIES aa*bb <= 1")
(("1" (rewrite -1)
(("1" (expand "max" 1)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(lemma "exp_increasing")
(("1"
(expand "increasing?")
(("1"
(inst - "x!1" "0")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "both_sides_expt_pos_le")
(("2"
(inst - "1+2*n!1" "-x!1" "1")
(("2" (assert) nil nil))
nil))
nil)
("3" (assert)
(("3"
(lemma "nnreal_expt")
(("3"
(expand "^")
(("3" (inst?) nil nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (skeep)
(("2"
(mult-ineq -1 -2)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "exp_neg_le1_ub")
(("2"
(name "FF" "LAMBDA (nn:nat): exp_estimate(x!1, 2 * nn)")
(("2"
(comment "this part of the proof changed 1/30/2013 by Anthony")
(("2" (case "FORALL (nn:nat): FF(nn+1) < FF(nn)")
(("1"
(case "FORALL (epsil:posreal): EXISTS (M:nat): FORALL (nn:nat): nn>=M IMPLIES abs(exp(x!1)-exp_estimate(x!1,nn)) < epsil")
(("1"
(case "FORALL (nn,mm:nat): mm>nn IMPLIES FF(mm) < FF(nn)")
(("1" (hide -3)
(("1" (inst-cp - "n!1" "n!1+1")
(("1" (assert)
(("1" (case "NOT exp(x!1)>=FF(n!1)")
(("1" (expand "FF" 1)
(("1" (assert) nil nil)) nil)
("2" (inst -4 "(exp(x!1) - FF(1+n!1))/2")
(("1"
(skeep -4)
(("1"
(case
"EXISTS (KK:posnat): 2*KK > M AND KK > 1+n!1")
(("1"
(skeep -1)
(("1"
(inst -6 "2*KK")
(("1"
(assert)
(("1"
(inst - "1+n!1" "KK")
(("1"
(assert)
(("1"
(expand "FF")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(inst + "max(M+1,2+n!1)")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide -1)
(("2"
(case "FORALL (nn,mm:nat): FF(nn+1+mm) <= FF(nn+1)")
(("1" (skeep)
(("1" (case "mm = nn+1")
(("1"
(inst -4 "nn")
(("1" (assert) nil nil))
nil)
("2"
(assert)
(("2"
(inst - "nn" "mm-1-nn")
(("2"
(assert)
(("2"
(inst - "nn")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "mm")
(("1" (assert) nil nil)
("2"
(skeep)
(("2"
(skeep)
(("2"
(assert)
(("2"
(inst - "nn")
(("2"
(assert)
(("2"
(inst - "(1+j+nn)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-1 -2 2))
(("2" (lemma "exp_taylors_err")
(("2" (lemma "archimedean")
(("2" (skeep)
(("2" (inst - "epsil")
(("2" (skosimp*)
(("2"
(inst + "n!2 + 2")
(("2"
(skeep)
(("2"
(inst - "nn" "x!1")
(("2"
(case
"(max(exp(x!1), 1) * abs(x!1) ^ (1 + nn)) <= 1")
(("1"
(mult-by
-1
"1/factorial(1+nn)")
(("1"
(assert)
(("1"
(case
"1/factorial(1+nn) < 1/n!2")
(("1" (assert) nil nil)
("2"
(cross-mult 1)
(("2"
(case
"FORALL (kkr:nat): factorial(1+kkr)>=kkr")
(("1"
(assert)
(("1"
(inst - "nn")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(induct "kkr")
(("1"
(assert)
nil
nil)
("2"
(skeep)
(("2"
(assert)
(("2"
(expand
"factorial"
+)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"FORALL (aa,bb:nnreal): aa<=1 AND bb<=1 IMPLIES aa*bb <= 1")
(("1"
(rewrite -1)
(("1"
(expand "max" 1)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(lemma
"exp_increasing")
(("1"
(expand
"increasing?")
(("1"
(inst
-
"x!1"
"0")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"both_sides_expt_pos_le")
(("2"
(inst
-
"1+nn"
"abs(x!1)"
"1")
(("2"
(assert)
(("2"
(expand "abs" 1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2"
(mult-ineq -1 -2)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-1 2))
(("2" (skeep)
(("2" (expand "FF")
(("2" (expand "exp_estimate")
(("2" (expand "sigma" + 1)
(("2" (expand "sigma" + 1)
(("2"
(case "-(x!1 ^ (1 + 2 * nn)) / factorial(1 + 2 * nn)
> (x!1 ^ (2 + 2 * nn)) / factorial(2 + 2 * nn)")
(("1" (assert) nil nil)
("2"
(hide 2)
(("2"
(case
"-(x!1 ^ (1 + 2 * nn)) >=
(x!1 ^ (2 + 2 * nn))")
(("1"
(cross-mult 1)
(("1"
(mult-by -1 "factorial(1+2*nn)")
(("1"
(case "2+2*nn > 1")
(("1"
(mult-by
-1
"-(x!1 ^ (1 + 2 * nn)) * factorial(1 + 2 * nn)")
(("1"
(assert)
(("1"
(expand "factorial" + 1)
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide 2)
(("2"
(case
"FORALL (aa:real): aa > 0 IMPLIES (aa>=0 AND aa>0)")
(("1"
(rewrite -1)
(("1"
(hide 2)
(("1"
(lemma
"posreal_exp")
(("1"
(inst
-
"(1+2*nn)"
"-x!1")
(("1"
(assert)
(("1"
(lemma
"mult_expt")
(("1"
(inst
-
"1+2*nn"
"-1"
"x!1")
(("1"
(replaces
-1)
(("1"
(lemma
"not_even_m1_pow")
(("1"
(inst?)
(("1"
(split
-)
(("1"
(replaces
-1)
(("1"
(mult-by
-1
"factorial(1+2*nn)")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(lemma
"even_or_odd")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(mult-by
-1
"-(x!1 ^ (1 + 2 * nn))")
(("1"
(assert)
(("1"
(expand "^")
(("1"
(expand "expt" + 2)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma "mult_expt")
(("2"
(inst
-
"1+2*nn"
"-1"
"x!1")
(("2"
(lemma "posreal_exp")
(("2"
(inst
-
"1+2*nn"
"-x!1")
(("2"
(replaces -2)
(("2"
(lemma
"not_even_m1_pow")
(("2"
(inst?)
(("2"
(split -)
(("1"
(assert)
nil
nil)
("2"
(lemma
"even_or_odd")
(("2"
(inst?)
(("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))
";;; this part of the proof changed 1/30/2013 by Anthony"))
nil))
nil))
nil))
nil))
nil))
nil)
((exp_neg_le1_ub const-decl "real" exp_approx nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(exp const-decl "{py | x = ln(py)}" ln_exp nil)
(ln const-decl "real" ln_exp nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(exp_taylors_err formula-decl nil exp_series nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(factorial def-decl "posnat" factorial "ints/")
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal type-eq-decl nil real_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nnreal_expt judgement-tcc nil exponentiation nil)
(both_sides_expt_pos_le formula-decl nil exponentiation nil)
(expt_1i formula-decl nil exponentiation nil)
(posint_exp application-judgement "posint" exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(increasing? const-decl "bool" real_fun_preds "reals/")
(exp_0 formula-decl nil ln_exp nil)
(exp_increasing formula-decl nil ln_exp nil)
(n!1 skolem-const-decl "nat" exp_approx nil)
(x!1 skolem-const-decl "real" exp_approx nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_times_le_any1 formula-decl nil extra_real_props nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posreal_max application-judgement
"{z: posreal | z >= x AND z >= y}" real_defs nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(exp_neg_le1_lb const-decl "real" exp_approx nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sigma def-decl "real" sigma "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(both_sides_times_pos_gt1 formula-decl nil real_props nil)
(nn skolem-const-decl "nat" exp_approx nil)
(mult_expt formula-decl nil exponentiation nil)
(even_or_odd formula-decl nil naturalnumbers nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_exp application-judgement "int" exponentiation nil)
(not_even_m1_pow formula-decl nil exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(posreal_exp judgement-tcc nil exponentiation nil)
(div_mult_pos_gt2 formula-decl nil extra_real_props nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(expt def-decl "real" exponentiation nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(posrat_max application-judgement "{s: posrat | s >= q AND s >= r}"
real_defs nil)
(posint_max application-judgement "{k: posint | i <= k AND j <= k}"
real_defs nil)
(FF skolem-const-decl "[nat -> real]" exp_approx nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(times_div2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(factorial_1 formula-decl nil factorial "ints/")
(archimedean formula-decl nil real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(exp_estimate const-decl "real" exp_series nil))
nil)
(exp_neg_le1_bounds-2 nil 3307367265
("" (expand "exp_neg_le1_lb")
(("" (expand "exp_neg_le1_ub")
(("" (skosimp)
(("" (case "FORALL (n:nat): 0 < x!1^(2*n) & x!1^(2*n) <= 1")
(("1"
(case "FORALL (n:nat): -1 <= x!1^(2*n+1) & x!1^(2*n+1) < 0")
(("1" (case "max(exp(x!1), 1) = 1")
(("1"
(case "FORALL (n,m:posnat): n < m => abs(x!1)^m/factorial(m) < abs(x!1)^n/factorial(n)")
(("1"
(case-replace
"exp_estimate(x!1, 1 + 2 * n!1) < exp(x!1)")
(("1" (lemma "exp_series" ("x" "x!1" "n" "1+2*n!1"))
(("1" (expand "abs" -1 1)
(("1" (assert)
(("1" (replace -4)
(("1" (hide -2)
(("1" (expand "exp_estimate")
(("1"
(expand "sigma" -1 1)
(("1"
(name-replace
"RHS"
"sigma(0, 2 * n!1,
LAMBDA (nn: nat):
IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)")
(("1"
(case
"(x!1^(1+2*n!1))/factorial(1+2*n!1) + abs(x!1)^(2+2*n!1)/factorial(2+2*n!1) < 0")
(("1" (assert) nil)
("2"
(inst -2 "1+2*n!1" "2+2*n!1")
(("2"
(assert)
(("2"
(case-replace
"abs(x!1) ^ (1 + 2 * n!1) = -(x!1^(1+2*n!1))")
(("1" (assert) nil)
("2"
(hide 2 3 -1 -3)
(("2"
(hide -1 -2 -3)
(("2"
(rewrite "expt_plus")
(("1"
(rewrite "expt_plus")
(("1"
(rewrite "expt_x1")
(("1"
(rewrite
"expt_x1")
(("1"
(rewrite
"expt_times")
(("1"
(rewrite
"expt_times")
(("1"
(expand
"abs")
(("1"
(case-replace
"(-x!1) ^ 2=x!1 ^ 2")
(("1"
(assert)
nil)
("2"
(hide
2)
(("2"
(expand
"^")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(assert)
nil)))))))))))))))))
("2"
(expand
"abs")
(("2"
(assert)
nil)))))))))))
("2"
(expand "abs")
(("2"
(assert)
nil)))))))))))))))))))))))))))))))))
("2" (hide 2)
(("2"
(lemma "exp_series" ("x" "x!1" "n" "2+2*n!1"))
(("2" (replace -3)
(("2" (expand "abs" -1 1)
(("2" (expand "exp_estimate")
(("2" (expand "sigma" -1)
(("2"
(name-replace
"LB"
"sigma(0, 1 + 2 * n!1,
LAMBDA (nn: nat):
IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)")
(("2"
(case-replace
"exp(x!1) - LB - (x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) < 0")
(("1"
(hide -1)
(("1"
(case
"x!1^(2+2*n!1) / factorial(2+2*n!1) - abs(x!1)^(3+2*n!1)/factorial(3+2*n!1) > 0")
(("1" (assert) nil)
("2"
(hide -1 2)
(("2"
(inst - "2+2*n!1" "3+2*n!1")
(("2"
(assert)
(("2"
(case-replace
"abs(x!1) ^ (2 + 2 * n!1) = x!1 ^ (2 + 2 * n!1)")
(("1" (assert) nil)
("2"
(hide -1 2)
(("2"
(lemma
"expt_times"
("i"
"2"
"j"
"1+n!1"))
(("2"
(inst-cp
-
"abs(x!1)")
(("1"
(inst - "x!1")
(("1"
(case-replace
"abs(x!1)^2 = x!1^2")
(("1"
(assert)
nil)
("2"
(hide-all-but
(-7 1))
(("2"
(expand
"^")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(expand
"abs")
(("2"
(assert)
nil)))))))))))))))))
("2"
(expand "abs")
(("2"
(assert)
nil)))))))))))))))))))))
("2"
(hide -1)
(("2"
(case
"(x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) > 0")
(("1" (assert) nil)
("2"
(hide 2 3)
(("2"
(inst -4 "1+n!1")
(("2"
(flatten)
(("2"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"x!1 ^ (2 + 2 * n!1)"
"py"
"factorial(2 + 2 * n!1)"))
(("1" (propax) nil)
("2"
(assert)
nil)))))))))))))))))))))))))))))))
("2" (hide-all-but (-4 -5 1))
(("2" (skosimp)
(("2"
(case "forall (n,m:posnat): factorial(n) < factorial(n+m)")
(("1" (case "abs(x!1) ^ m!1 <= abs(x!1) ^ n!2")
(("1"
(lemma "lt_div_lt_pos1"
("px" "abs(x!1) ^ m!1" "w" "factorial(m!1)"
"y" "abs(x!1) ^ n!2" "pz"
"factorial(n!2)"))
(("1" (split -1)
(("1" (propax) nil) ("2" (propax) nil)
("3" (inst - "n!2" "m!1-n!2")
(("1" (assert) nil)
("2" (assert) nil)))))
("2"
(lemma "expt_pos"
("px" "abs(x!1)" "i" "m!1"))
(("1" (propax) nil)
("2" (expand "abs")
(("2" (assert) nil)))))))
("2" (hide 2 -1)
(("2" (case-replace "abs(x!1)=1")
(("1" (rewrite "expt_1i")
(("1"
(rewrite "expt_1i")
(("1" (assert) nil)))))
("2" (case "abs(x!1)<1")
(("1"
(lemma
"both_sides_expt_lt1_lt"
("lt1x"
"abs(x!1)"
"i"
"m!1"
"j"
"n!2"))
(("1" (assert) nil)
("2"
(assert)
(("2"
(expand "abs")
(("2" (assert) nil)))))))
("2"
(expand "abs")
(("2" (assert) nil)))))))))))
("2" (hide -2 -3 2)
(("2" (hide -1)
(("2" (induct "m")
(("1" (assert) nil) ("2" (assert) nil)
("3" (skosimp*)
(("3"
(case-replace "j!1=0")
(("1"
(expand "factorial" 1 2)
(("1"
(lemma
"both_sides_times_pos_lt1"
("pz"
"factorial(n!3)"
"x"
"1"
"y"
"1+n!3"))
(("1" (assert) nil)))))
("2"
(assert)
(("2"
(inst - "n!3")
(("2"
(expand "factorial" 2 2)
(("2"
(assert)
nil)))))))))))))))))))))))))
("2" (hide-all-but (-4 1))
(("2" (expand "max")
(("2" (lemma "exp_strict_increasing")
(("2" (expand "strict_increasing?")
(("2" (inst - "x!1" "0")
(("2" (rewrite "exp_0")
(("2" (assert) nil)))))))))))))))
("2" (hide 2)
(("2" (skosimp)
(("2" (inst - "n!2")
(("2" (flatten)
(("2" (rewrite "expt_plus" 1)
(("2" (rewrite "expt_x1" 1)
(("2"
(lemma "both_sides_times_neg_lt1"
("nz" "x!1" "y" "0" "x" "x!1^(2*n!2)"))
(("1"
(lemma "both_sides_times_neg_le1"
("nz" "x!1" "x" "1" "y" "x!1^(2*n!2)"))
(("1" (assert) nil)))
("2" (assert) nil)))))))))))))))))
("2" (hide 2)
(("2" (skosimp)
(("2" (rewrite "expt_times" 1)
(("2" (case "0 < x!1^2 & x!1^2<=1")
(("1" (flatten)
(("1" (lemma "expt_pos" ("i" "n!2" "px" "x!1^2"))
(("1" (expand "<=" -3)
(("1" (split -3)
(("1" (case-replace "n!2=0")
(("1" (rewrite "expt_x0")
(("1" (assert) nil)))
("2"
(lemma "both_sides_expt_pos_lt"
("px" "x!1^2" "py" "1" "pm" "n!2"))
(("1"
(rewrite "expt_1i")
(("1" (assert) nil)))
("2" (assert) nil)))))
("2" (replace -1)
(("2" (rewrite "expt_1i")
(("2" (assert) nil)))))))))
("2" (assert) nil)))))
("2" (hide 2)
(("2"
(lemma "negreal_times_negreal_is_posreal"
("nx" "x!1" "ny" "x!1"))
(("1" (lemma "le_times_le_neg")
(("1" (inst - "x!1" "x!1" "-1" "-1")
(("1" (expand "^")
(("1" (expand "expt")
(("1"
(expand "expt")
(("1"
(expand "expt")
(("1" (assert) nil)))))))))
("2" (assert) nil)))))
("2" (assert) nil))))))))))))))))))))
nil)
nil nil)
(exp_neg_le1_bounds-1 nil 3295528895
("" (expand "exp_neg_le1_lb")
(("" (expand "exp_neg_le1_ub")
(("" (skosimp)
(("" (case "FORALL (n:nat): 0 < x!1^(2*n) & x!1^(2*n) <= 1")
(("1"
(case "FORALL (n:nat): -1 <= x!1^(2*n+1) & x!1^(2*n+1) < 0")
(("1" (case "max(exp(x!1), 1) = 1")
(("1"
(case "FORALL (n,m:posnat): n < m => abs(x!1)^m/factorial(m) < abs(x!1)^n/factorial(n)")
(("1"
(case-replace
"exp_series_n(x!1, 1 + 2 * n!1) < exp(x!1)")
(("1" (lemma "exp_series" ("x" "x!1" "n" "1+2*n!1"))
(("1" (expand "abs" -1 1)
(("1" (assert)
(("1" (replace -4)
(("1" (hide -2)
(("1" (expand "exp_series_n")
(("1"
(expand "sigma" -1 1)
(("1"
(name-replace
"RHS"
"sigma(0, 2 * n!1,
LAMBDA (nn: nat):
IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)")
(("1"
(case
"(x!1^(1+2*n!1))/factorial(1+2*n!1) + abs(x!1)^(2+2*n!1)/factorial(2+2*n!1) < 0")
(("1" (assert) nil nil)
("2"
(inst -2 "1+2*n!1" "2+2*n!1")
(("2"
(assert)
(("2"
(case-replace
"abs(x!1) ^ (1 + 2 * n!1) = -(x!1^(1+2*n!1))")
(("1" (assert) nil nil)
("2"
(hide 2 3 -1 -3)
(("2"
(hide -1 -2 -3)
(("2"
(rewrite "expt_plus")
(("1"
(rewrite "expt_plus")
(("1"
(rewrite "expt_x1")
(("1"
(rewrite
"expt_x1")
(("1"
(rewrite
"expt_times")
(("1"
(rewrite
"expt_times")
(("1"
(expand
"abs")
(("1"
(case-replace
"(-x!1) ^ 2=x!1 ^ 2")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(expand
"^")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"abs")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "abs")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(lemma "exp_series" ("x" "x!1" "n" "2+2*n!1"))
(("2" (replace -3)
(("2" (expand "abs" -1 1)
(("2" (expand "exp_series_n")
(("2" (expand "sigma" -1)
(("2"
(name-replace
"LB"
"sigma(0, 1 + 2 * n!1,
LAMBDA (nn: nat):
IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)")
(("2"
(case-replace
"exp(x!1) - LB - (x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) < 0")
(("1"
(hide -1)
(("1"
(case
"x!1^(2+2*n!1) / factorial(2+2*n!1) - abs(x!1)^(3+2*n!1)/factorial(3+2*n!1) > 0")
(("1" (assert) nil nil)
("2"
(hide -1 2)
(("2"
(inst - "2+2*n!1" "3+2*n!1")
(("2"
(assert)
(("2"
(case-replace
"abs(x!1) ^ (2 + 2 * n!1) = x!1 ^ (2 + 2 * n!1)")
(("1" (assert) nil nil)
("2"
(hide -1 2)
(("2"
(lemma
"expt_times"
("i"
"2"
"j"
"1+n!1"))
(("2"
(inst-cp
-
"abs(x!1)")
(("1"
(inst - "x!1")
(("1"
(case-replace
"abs(x!1)^2 = x!1^2")
(("1"
(assert)
nil
nil)
("2"
(hide-all-but
(-7 1))
(("2"
(expand
"^")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(expand
"expt")
(("2"
(expand
"abs")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.916 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
