|
(ln_series
(ln_estimate_TCC1 0
(ln_estimate_TCC1-1 nil 3302450959
("" (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 3320163563 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(ln_estimate_TCC3 0
(ln_estimate_TCC3-1 nil 3322477326 ("" (assuming-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_taylors_TCC1 0
(ln_taylors_TCC1-1 nil 3302450959
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(ln_taylors_TCC2 0
(ln_taylors_TCC2-1 nil 3302450959
("" (skosimp*) (("" (typepred "c!1") (("" (grind) nil nil)) nil))
nil)
((between type-eq-decl nil taylor_help nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Gt_m1 type-eq-decl nil ln_series nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(> const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(ln_taylors_TCC3 0
(ln_taylors_TCC3-1 nil 3302450959
("" (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-2 nil 3302450340
("" (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"
(lift-if)
(("2"
(ground)
(("2"
(lemma "ln_nderiv")
(("2"
(inst?)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(assert)
(("2"
(simplify 2)
(("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"
(case-replace
"xgm1!1=0")
(("1"
(expand
"^"
2
3)
(("1"
(expand
"^"
2
1)
(("1"
(expand
"expt")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide
-1)
(("2"
(field
3)
(("2"
(flatten)
(("2"
(expand
"^")
(("2"
(lemma
"expt_of_mult")
(("2"
(inst
-
"n!2"
"-xgm1!1"
"-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)
("2" (hide-all-but 1)
(("2" (skosimp*) nil nil)) nil)
("3" (skosimp*)
(("3"
(lemma "nderiv_ln")
(("3" (inst?) nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (flatten)
(("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))
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))
nil)
(ln_taylors-1 nil 3302449853
("" (skosimp*)
((""
(lemma "Taylors[posreal]"
("f" "ln" "n" "n!1" "bb" "xgm1!1+1" "aa" "1"))
(("1" (lemma "ln_derivable_n_times" ("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_series_n" 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)))))))
("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)))))))))))))))))))))))))))))))
("2"
(hide-all-but 1)
(("2"
(skosimp*)
(("2"
(typepred "n!2")
(("2"
(assert)
(("2"
(rewrite "ln_1")
(("2"
(case "n!2=0")
(("1" (assert) 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"
(case-replace
"xgm1!1=0")
(("1"
(expand
"^"
2
3)
(("1"
(expand
"^"
2
1)
(("1"
(expand
"expt")
(("1"
(assert)
nil)))))))
("2"
(lemma
"div_expt"
("n0x"
"xgm1!1"
"n0y"
"-1"
"i"
"n!2"))
(("1"
(assert)
nil)
("2"
(assert)
nil)))))))))))))))))))))))))))))))))))))
("2" (hide-all-but 1)
(("2"
(skosimp*)
(("2"
(assert)
(("2"
(lemma
"ln_derivable_n_times"
("n" "nn!1"))
(("2" (propax) 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_series_n")
(("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"))
(("2"
(split -1)
(("1" (assert) nil)
("2"
(hide -1 2)
(("2"
(skosimp*)
(("2"
(case "n!2=0")
(("1"
(assert)
nil)
("2"
(assert)
(("2"
(expand
"^")
(("2"
(expand
"expt")
(("2"
(assert)
nil)))))))))))))))))))))))))))))))))))))))))))))))))
("2" (hide -1 -2)
(("2" (typepred "xgm1!1")
(("2" (typepred "c!1")
(("2" (replace -3)
(("2" (replace -4)
(("2" (propax) nil)))))))))))))))))))
("2" (hide 2)
(("2" (skosimp*)
(("2" (inst + "x!1+1") (("2" (assert) nil)))))))
("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil))))))))
nil)
nil nil))
(lnp1_TCC1 0
(lnp1_TCC1-1 nil 3321095836 ("" (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) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(abslt1 type-eq-decl nil ln_series 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)
(real_plus_real_is_real application-judgement "real" reals nil))
nil)))
¤ Dauer der Verarbeitung: 0.37 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.
|
