|
(ln_exp_series_alt
(ln_estimate_TCC1 0
(ln_estimate_TCC1-1 nil 3270048045
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(ln_estimate_TCC2 0
(ln_estimate_TCC2-1 nil 3270048058
("" (skosimp*) (("" (inst + "n!1+1") (("" (assert) nil nil)) nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(ln_estimate_TCC3 0
(ln_estimate_TCC3-1 nil 3374414377 ("" (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)
(>= const-decl "bool" 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(/= const-decl "boolean" notequal nil))
nil))
(ln_estimate_scaf4_TCC1 0
(ln_estimate_scaf4_TCC1-1 nil 3309547516
("" (skosimp) (("" (assert) nil nil)) nil)
((real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(ln_estimate_scaf4_TCC2 0
(ln_estimate_scaf4_TCC2-1 nil 3309547523
("" (skosimp) (("" (assert) nil nil)) nil) nil shostak))
(ln_estimate_scaf4_TCC3 0
(ln_estimate_scaf4_TCC3-1 nil 3309547541
("" (skosimp) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(ln_estimate_scaf4 0
(ln_estimate_scaf4-1 nil 3309546853
("" (skosimp)
(("" (name "SS" "sigma(0, n!1, LAMBDA (i: nat): x!1 ^ i)")
(("" (replace -1)
((""
(lemma "add_div"
("x" "SS" "n0x" "1" "y" "x!1^(n!1+1)" "n0y" "1-x!1"))
(("" (replace -1 2)
((""
(lemma "both_sides_div1"
("x" "1" "y" "SS * (1 - x!1) + x!1 ^ (n!1 + 1)" "n0z"
"1-x!1"))
(("" (replace -1 2)
(("" (hide -1 -2)
((""
(case "forall (n:nat): 1 = sigma(0, n, LAMBDA (i: nat): x!1 ^ i) *(1-x!1) + x!1 ^ (n+1)")
(("1" (inst - "n!1") (("1" (assert) nil nil)) nil)
("2" (hide-all-but (1 2))
(("2" (induct "n")
(("1" (expand "sigma")
(("1" (assert)
(("1" (expand "^")
(("1"
(expand "expt")
(("1"
(expand "expt")
(("1"
(expand "sigma")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "sigma" 1)
(("2"
(name-replace "DRL101"
"sigma(0, j!1, LAMBDA (i: nat): x!1 ^ i)")
(("2"
(case-replace
"(x!1 ^ (1 + j!1)) * x!1 = x!1 ^ (2 + j!1)")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2"
(expand "^")
(("2"
(expand "expt" 1 2)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(add_div formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(both_sides_div1 formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(expt def-decl "real" exponentiation nil)
(sigma_0_neg formula-decl nil sigma_nat "reals/")
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(real_times_real_is_real application-judgement "real" reals 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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(ln_estimate_scaf5_TCC1 0
(ln_estimate_scaf5_TCC1-1 nil 3309550054
("" (skosimp) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(ln_estimate_scaf5_TCC2 0
(ln_estimate_scaf5_TCC2-1 nil 3309550054
("" (skosimp) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(ln_estimate_scaf5 0
(ln_estimate_scaf5-1 nil 3309548279
("" (skosimp)
(("" (lemma "ln_estimate_scaf4" ("x" "1-nzx!1" "n" "n!1"))
(("" (assert) nil nil)) nil))
nil)
((nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(ln_estimate_scaf4 formula-decl nil ln_exp_series_alt nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals 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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(ln_estimate_bnd_TCC1 0
(ln_estimate_bnd_TCC1-1 nil 3322390165 ("" (subtype-tcc) nil nil) nil
nil))
(ln_estimate_bnd_TCC2 0
(ln_estimate_bnd_TCC2-1 nil 3322390165 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(ln_estimate_bnd_TCC3 0
(ln_estimate_bnd_TCC3-1 nil 3322390165
("" (skosimp*)
(("" (typepred "n!1")
(("" (name "NP1" "n!1+1")
(("" (replace -1)
(("" (lift-if)
(("" (name "zP1" "z!1+1")
(("" (replace -1)
(("" (ground) (("" (mult-cases -2) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(>= 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(real_gtm1_le1 nonempty-type-eq-decl nil ln_exp_series_alt nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(zero_times3 formula-decl nil real_props nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posint nonempty-type-eq-decl nil integers nil))
nil))
(ln_estimate_bnd 0
(ln_estimate_bnd-1 nil 3322390178
("" (skosimp)
(("" (lemma "ln_estimate_scaf9" ("px" "1+z!1" "n" "n!1"))
(("" (replace -1)
(("" (assert)
(("" (hide -1)
(("" (typepred "z!1")
(("" (case "0 <=z!1")
(("1" (hide -2)
(("1"
(lemma "ln_estimate_scaf10"
("px" "1+z!1" "n" "n!1"))
(("1" (assert)
(("1" (expand "abs" 1 2) (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(lemma "ln_estimate_scaf11" ("px" "1+z!1" "n" "n!1"))
(("2" (assert)
(("2" (expand "abs" 2 2) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(lnT_TCC1 0
(lnT_TCC1-1 nil 3309361152 ("" (skosimp) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(lnT_TCC2 0
(lnT_TCC2-1 nil 3309361152
(""
(case "forall (n:nat,x:real): -1 <= x & x <= 1 => -1 <= x^n & x^n <= 1")
(("1" (skosimp)
(("1" (case-replace "x!1=0")
(("1" (expand "^" 1)
(("1" (expand "expt" 1) (("1" (propax) nil nil)) nil)) nil)
("2" (case-replace "n!1=0")
(("1" (rewrite "expt_x1") (("1" (assert) nil nil)) nil)
("2" (inst - "n!1+1" "-x!1")
(("2" (assert)
(("2" (flatten)
(("2" (rewrite "div_mult_pos_lt2" 3)
(("2" (rewrite "div_mult_pos_le1" 3)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skolem 1 ("_" "x"))
(("2" (induct "n")
(("1" (expand "^" 1)
(("1" (expand "expt" 1) (("1" (propax) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (assert)
(("2" (flatten)
(("2" (expand "^")
(("2" (expand "expt" 1)
(("2" (lemma "trichotomy" ("x" "x"))
(("2" (split -1)
(("1"
(lemma "both_sides_times_pos_le1" ("pz" "x"))
(("1" (inst-cp - "-1" "expt(x, j!1)")
(("1" (inst - "expt(x, j!1)" "1")
(("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil)
("2" (replace -1) (("2" (assert) nil nil))
nil)
("3"
(lemma "both_sides_times_neg_le1" ("nz" "x"))
(("1" (inst-cp - "expt(x, j!1)" "-1")
(("1" (inst - "1" "expt(x, j!1)")
(("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(trichotomy formula-decl nil real_axioms nil)
(both_sides_times_neg_le1 formula-decl nil real_props nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(nat_expt application-judgement "nat" exponentiation nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_x1 formula-decl nil exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_expt application-judgement "int" exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(expt def-decl "real" 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)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(< const-decl "bool" reals nil)
(real_gtm1_le1 nonempty-type-eq-decl nil ln_exp_series_alt nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil))
shostak))
(ln_taylors_TCC1 0
(ln_taylors_TCC1-1 nil 3270048072 ("" (grind) nil nil) nil shostak))
(ln_taylors_TCC2 0
(ln_taylors_TCC2-1 nil 3270048235 ("" (grind) 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)
(> const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(between type-eq-decl nil taylor_help nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(/= const-decl "boolean" notequal nil))
shostak))
(ln_taylors_TCC3 0
(ln_taylors_TCC3-1 nil 3270063121
("" (skosimp*) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
shostak))
(ln_taylors 0
(ln_taylors-1 nil 3270058061
("" (skosimp*)
((""
(lemma "Taylors[posreal]"
("f" "ln" "n" "n!1" "bb" "xgm1!1+1" "aa" "1"))
(("1" (lemma "nderiv_ln" ("n" "n!1+1"))
(("1" (replace -1)
(("1" (skosimp*)
(("1" (inst + "c!1")
(("1" (lemma "ln_nderiv" ("n" "n!1+1"))
(("1" (simplify -1)
(("1" (replace -1 -3)
(("1" (simplify -3)
(("1" (rewrite "div_expt" 1)
(("1" (expand "ln_estimate" 1)
(("1"
(lemma "sigma_eq[nat]"
("low" "0" "high" "n!1" "F"
"LAMBDA (nn:nat):
IF nn > n!1 THEN 0
ELSIF nn = 0 THEN ln(1)
ELSE nderiv(nn, ln)(1) * xgm1!1 ^ nn / factorial(nn)
ENDIF" "G" "LAMBDA (nn: nat):
IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF"))
(("1" (split -1)
(("1"
(replace -1 -4)
(("1"
(name-replace
"K1"
"sigma(0, n!1,
LAMBDA (nn: nat):
IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF)")
(("1"
(replace -4 1)
(("1"
(hide-all-but 1)
(("1"
(typepred "c!1")
(("1"
(hide -1 -3 -4 -5)
(("1"
(expand "factorial" 1 2)
(("1"
(name-replace
"K2"
"factorial(n!1)")
(("1"
(lemma
"div_cancel1"
("x"
"((-1/ (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (1+n!1)"
"n0z"
"K2"))
(("1"
(rewrite
"div_div2"
-1)
(("1"
(case
"K2 * (((-1 / (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (K2 + K2 * n!1)) = ((-K2 / (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (K2 + K2 * n!1)")
(("1"
(replace -1)
(("1"
(replace -2)
(("1"
(hide -1 -2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(name-replace
"K3"
"K2 + K2 * n!1")
(("2"
(name-replace
"K4"
"xgm1!1 ^ (1 + n!1)")
(("2"
(name-replace
"K5"
"(-c!1) ^ (1 + n!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skosimp*)
(("2"
(typepred "n!2")
(("2"
(assert)
(("2"
(case "n!2=0")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(lemma
"ln_nderiv"
("n" "n!2"))
(("2"
(assert)
(("2"
(replace -1 2)
(("2"
(simplify 2)
(("2"
(hide -1)
(("2"
(lemma
"cross_mult"
("x"
"-factorial(n!2 - 1) / (-1) ^ n!2 * xgm1!1 ^ n!2"
"n0x"
"factorial(n!2)"
"y"
"-(-xgm1!1) ^ n!2"
"n0y"
"n!2"))
(("2"
(replace -1 2)
(("2"
(expand
"factorial"
2
2)
(("2"
(assert)
(("2"
(case-replace
"xgm1!1=0")
(("1"
(expand
"^"
2
3)
(("1"
(expand
"^"
2
1)
(("1"
(expand
"expt")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(lemma
"div_expt"
("n0x"
"xgm1!1"
"n0y"
"-1"
"i"
"n!2"))
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) nil nil)
("3" (skosimp*)
(("3"
(assert)
(("3" (rewrite "nderiv_ln") nil nil))
nil))
nil))
nil))
nil)
("2" (expand "/=" 1)
(("2" (replace -1)
(("2" (rewrite "ln_1")
(("2"
(expand "^" 1)
(("2"
(expand "expt" 1)
(("2"
(assert)
(("2"
(rewrite "zero_times1")
(("2"
(simplify 1)
(("2"
(expand "ln_estimate")
(("2"
(hide-all-but 1)
(("2"
(lemma
"sigma_zero[nat]"
("low"
"0"
"high"
"n!1"))
(("2"
(lemma
"sigma_eq[nat]"
("low"
"0"
"high"
"n!1"
"F"
"LAMBDA (i: nat): 0"
"G"
"LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-0) ^ nn / nn ENDIF"))
(("1"
(split -1)
(("1"
(assert)
nil
nil)
("2"
(hide -1 2)
(("2"
(skosimp*)
(("2"
(case "n!2=0")
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(expand
"^")
(("2"
(expand
"expt")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -2)
(("2" (typepred "xgm1!1")
(("2" (typepred "c!1")
(("2" (replace -3)
(("2" (replace -4) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil))
nil))
nil))
nil)
((ln const-decl "real" ln_exp nil)
(sigma_zero formula-decl nil sigma "reals/")
(sigma def-decl "real" sigma "reals/")
(sigma_eq formula-decl nil sigma "reals/")
(ln_1 formula-decl nil ln_exp nil))
shostak))
(expT_TCC1 0
(expT_TCC1-1 nil 3309695446
("" (skosimp) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(exp_taylors_TCC1 0
(exp_taylors_TCC1-1 nil 3269926951 ("" (grind) nil nil)
((/= const-decl "boolean" notequal nil)) shostak))
(exp_taylors 0
(exp_taylors-1 nil 3269893214
("" (skosimp*)
(("" (lemma "Taylors" ("f" "exp" "n" "n!1" "aa" "0" "bb" "x!1"))
(("" (lemma "nderiv_exp")
(("" (inst?)
(("" (flatten)
(("" (replace -1)
(("" (skosimp*)
(("" (inst + "c!1")
(("" (replace -2)
(("" (expand "exp_estimate")
((""
(lemma "sigma_eq[nat]"
("low" "0" "high" "n!1" "F" "LAMBDA (nn:nat):
IF nn > n!1 THEN 0
ELSIF nn = 0 THEN exp(0)
ELSE nderiv(nn, exp)(0) * (x!1 - 0) ^ nn / factorial(nn)
ENDIF" "G"
"LAMBDA (nn: nat): IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF"))
(("1" (split -1)
(("1" (assert)
(("1" (expand "expT")
(("1"
(replace -1 1 rl)
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2"
(typepred "n!2")
(("2"
(assert)
(("2"
(lemma "nderiv_exp")
(("2"
(inst - "n!2")
(("2"
(flatten)
(("2"
(hide -1)
(("2"
(replace -1)
(("2"
(rewrite "exp_0")
(("2"
(case "n!2=0")
(("1" (assert) nil nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (hide 2)
(("2"
(lemma "nderiv_exp")
(("2"
(inst?)
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((exp const-decl "{py | x = ln(py)}" ln_exp nil)
(ln const-decl "real" ln_exp nil)
(exp_0 formula-decl nil ln_exp nil)
(sigma_eq formula-decl nil sigma "reals/"))
shostak))
(exp_estimate_bnd_TCC1 0
(exp_estimate_bnd_TCC1-1 nil 3322390567 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(exp_estimate_bnd 0
(exp_estimate_bnd-1 nil 3269894172
("" (skosimp*)
(("" (lemma "exp_taylors" ("x" "x!1" "n" "n!1"))
(("" (skosimp*)
(("" (typepred "c!1")
(("" (lemma "trichotomy" ("x" "x!1"))
((""
(case "exp(x!1) - exp_estimate(x!1, n!1) = exp(c!1) * x!1 ^ (n!1 + 1) / factorial(n!1 + 1)")
(("1" (replace -1)
(("1" (rewrite "abs_div" 1)
(("1" (expand "abs" 1 2)
(("1"
(lemma "both_sides_div_pos_le1"
("x" "abs(exp(c!1) * x!1 ^ (1 + n!1))" "y"
"max(exp(x!1),1) * x!1 ^ (1 + n!1)" "pz"
"factorial(1 + n!1)"))
(("1" (hide -1 -2 -7)
(("1" (rewrite "abs_mult")
(("1" (expand "abs" 1 1)
(("1" (case "exp(c!1)<=max(exp(x!1),1)")
(("1"
(split -2)
(("1"
(lemma
"expt_pos"
("px" "x!1" "i" "1+n!1"))
(("1"
(expand "abs" 1)
(("1"
(lemma "exp_strict_increasing")
(("1"
(expand "strict_increasing?")
(("1"
(inst-cp - "0" "c!1")
(("1"
(inst - "c!1" "x!1")
(("1"
(rewrite "exp_0")
(("1"
(assert)
(("1"
(flatten -6)
(("1"
(expand "max")
(("1"
(assert)
(("1"
(lemma
"both_sides_times_pos_lt1"
("x"
"exp(c!1)"
"y"
"exp(x!1)"
"pz"
"x!1^(1+n!1)"))
(("1"
(assert)
(("1"
(lemma
"both_sides_div_pos_lt1"
("x"
"exp(c!1) * x!1 ^ (1 + n!1)"
"y"
"exp(x!1) * x!1 ^ (1 + n!1)"
"pz"
"factorial(1+n!1)"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2"
(replace -1)
(("2"
(replace -5)
(("2"
(rewrite "exp_0")
(("2"
(expand "max")
(("2"
(expand "^")
(("2"
(expand "expt")
(("2"
(expand "abs")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(lemma "exp_strict_increasing")
(("3"
(expand "strict_increasing?")
(("3"
(assert)
(("3"
(hide -4 -6)
(("3"
(flatten -4)
(("3"
(inst-cp - "x!1" "c!1")
(("3"
(inst - "c!1" "0")
(("3"
(rewrite "exp_0")
(("3"
(expand "max")
(("3"
(assert)
(("3"
(typepred
"exp(c!1)")
(("3"
(hide -1 -3)
(("3"
(case
"abs(x!1 ^ (1 + n!1)) = abs(x!1) ^ (1 + n!1)")
(("1"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"abs(x!1) ^ (1 + n!1)"
"py"
"factorial(1 + n!1)"))
(("1"
(lemma
"both_sides_times_pos_le1"
("x"
"exp(c!1)"
"y"
"1"
"pz"
"abs(x!1) ^ (1 + n!1) / factorial(1 + n!1)"))
(("1"
(assert)
(("1"
(replace
-3
1)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"expt_pos"
("px"
"abs(x!1)"
"i"
"1+n!1"))
(("1"
(propax)
nil
nil)
("2"
(hide
2)
(("2"
(expand
"abs")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(case
"FORALL (n:nat): abs(x!1^n) = abs(x!1)^n")
(("1"
(inst
-
"1+n!1")
nil
nil)
("2"
(hide-all-but
(-4
1))
(("2"
(induct
"n")
(("1"
(rewrite
"expt_x0")
(("1"
(rewrite
"expt_x0")
(("1"
(expand
"abs")
(("1"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"^")
(("2"
(expand
"expt"
1)
(("2"
(rewrite
"abs_mult"
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)
("2"
(hide 2)
(("2"
(expand "max")
(("2"
(lemma "exp_strict_increasing")
(("2"
(expand "strict_increasing?")
(("2"
(split -2)
(("1"
(assert)
(("1"
(flatten -3)
(("1"
(inst-cp - "0" "c!1")
(("1"
(inst - "c!1" "x!1")
(("1"
(rewrite "exp_0")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(replace -1)
(("2"
(replace -3)
(("2"
(rewrite "exp_0")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(assert)
(("3"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.78 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
