|
(ln_approx
(ln_le2_bounds_TCC1 0
(ln_le2_bounds_TCC1-1 nil 3296313954 ("" (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)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_ge_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_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(ln_le2_bounds 0
(ln_le2_bounds-1 nil 3296309969
("" (expand "ln_le2_lb")
(("" (expand "ln_le2_ub")
(("" (skosimp*)
(("" (lift-if)
(("" (prop)
(("1" (assert) nil nil) ("2" (assert) nil nil)
("3" (lemma "ln_taylors" ("xgm1" "x!1" "n" "2*n!1"))
(("1" (skosimp*)
(("1" (typepred "c!1")
(("1" (assert)
(("1" (hide -1 -3 -4)
(("1" (replace -2)
(("1" (hide -2)
(("1" (flatten)
(("1"
(lemma "expt_plus"
("n0x" "x!1/-c!1" "i" "1" "j" "2*n!1"))
(("1"
(rewrite "expt_x1")
(("1"
(lemma
"expt_times"
("n0x"
"x!1/-c!1"
"i"
"2"
"j"
"n!1"))
(("1"
(case "(x!1 / -c!1) ^ 2 > 0")
(("1"
(lemma
"expt_pos"
("px"
"(x!1 / -c!1) ^ 2"
"i"
"n!1"))
(("1"
(case
"((x!1 / -c!1) ^ (1 + 2 * n!1)) / (1 + 2 * n!1) < 0")
(("1" (assert) nil nil)
("2"
(hide 2)
(("2"
(rewrite
"div_mult_pos_lt1"
1)
(("2"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"x!1"
"py"
"(x!1 / -c!1) ^ (2 * n!1)"))
(("1"
(lemma
"both_sides_div_neg_lt1"
("nz" "-c!1"))
(("1"
(inst
-
"x!1 * (x!1 / -c!1) ^ (2 * n!1)"
"0")
(("1"
(assert)
(("1"
(replace -6)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"both_sides_div_neg_lt1"
("nz"
"-c!1"
"y"
"0"
"x"
"x!1"))
(("1"
(lemma
"negreal_times_negreal_is_posreal"
("nx"
"x!1/-c!1"
"ny"
"x!1/-c!1"))
(("1"
(assert)
(("1"
(expand "^" 1)
(("1"
(expand "expt")
(("1"
(expand "expt")
(("1"
(expand "expt")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("4" (lemma "ln_taylors" ("xgm1" "x!1" "n" "1+2*n!1"))
(("1" (skosimp*)
(("1" (replace -1)
(("1" (typepred "c!1")
(("1" (assert)
(("1" (hide -1 -3 -4)
(("1" (flatten)
(("1" (hide -3)
(("1"
(case "0<((x!1 / -c!1) ^ (2 + 2 * n!1)) / (2 + 2 * n!1)")
(("1" (assert) nil nil)
("2"
(hide 2)
(("2"
(lemma
"expt_times"
("n0x"
"x!1/-c!1"
"i"
"2"
"j"
"1+n!1"))
(("2"
(lemma
"expt_pos"
("px"
"(x!1 / -c!1) ^ 2"
"i"
"1+n!1"))
(("1"
(assert)
(("1"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"(x!1 / -c!1) ^ (2 + 2 * n!1)"
"py"
"2 + 2*n!1"))
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide -1 2)
(("2"
(lemma
"both_sides_div_neg_lt1"
("nz"
"-c!1"
"y"
"0"
"x"
"x!1"))
(("1"
(assert)
(("1"
(lemma
"negreal_times_negreal_is_posreal"
("nx"
"x!1/-c!1"
"ny"
"x!1/-c!1"))
(("1"
(expand "^")
(("1"
(expand "expt")
(("1"
(expand "expt")
(("1"
(expand "expt")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) 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)
((ln_le2_ub const-decl "real" ln_approx nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(Gt_m1 type-eq-decl nil ln_series nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals 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_taylors formula-decl nil ln_series 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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(expt_plus formula-decl nil exponentiation nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(expt_times formula-decl nil exponentiation nil)
(negreal_times_negreal_is_posreal judgement-tcc nil real_types nil)
(expt def-decl "real" exponentiation nil)
(expt_pos formula-decl nil exponentiation nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(both_sides_div_neg_lt1 formula-decl nil real_props nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(^ const-decl "real" exponentiation nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(expt_x1 formula-decl nil exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(even_plus_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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(ln_le2_lb const-decl "real" ln_approx nil))
shostak))
(ln_gt1_lb_TCC1 0
(ln_gt1_lb_TCC1-1 nil 3321024764 ("" (subtype-tcc) nil nil) nil nil))
(ln_gt1_bounds_TCC1 0
(ln_gt1_bounds_TCC1-1 nil 3296313957 ("" (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)
(real_ge_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))
shostak))
(ln_gt1_bounds_TCC2 0
(ln_gt1_bounds_TCC2-1 nil 3296313957 ("" (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)
(real_ge_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))
shostak))
(ln_gt1_bounds 0
(ln_gt1_bounds-2 nil 3321025214
("" (skosimp*)
(("" (expand "ln_gt1_lb")
(("" (expand "ln_gt1_ub")
(("" (typepred "log_nat(x!1,2)`2")
(("1" (name-replace "m" "log_nat(x!1,2)`1")
(("1" (name-replace "y" "log_nat(x!1,2)`2")
(("1" (replaces -3)
(("1" (rewrite "ln_mult")
(("1" (rewrite "ln_expt")
(("1" (lemma "ln_le2_bounds")
(("1" (inst -1 "n!1" "1")
(("1" (assert)
(("1" (flatten)
(("1" (case "m=0")
(("1"
(replaces -1)
(("1"
(rewrite "expt_x0")
(("1"
(assert)
(("1"
(lemma "ln_le2_bounds")
(("1"
(inst -1 "n!1" "y-1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(mult-by -1 "m")
(("2"
(mult-by -2 "m")
(("2"
(case "y=1")
(("1"
(replaces -1)
(("1"
(rewrite "ln_1")
(("1"
(expand "ln_le2_lb")
(("1"
(expand "ln_le2_ub")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(lemma "ln_le2_bounds")
(("2"
(inst -1 "n!1" "y-1")
(("2"
(assert)
(("2"
(flatten)
(("2" (assert) nil 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)
((posint_exp application-judgement "posint" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(ln_gt1_lb const-decl "real" ln_approx nil)
(log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
"reals/")
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers 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)
(>= 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)
(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)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(ln_mult formula-decl nil ln_exp 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)
(ln_le2_bounds formula-decl nil ln_approx nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(expt_x0 formula-decl nil exponentiation nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(ln_le2_ub const-decl "real" ln_approx nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(ln_1 formula-decl nil ln_exp nil)
(m skolem-const-decl "nat" ln_approx nil)
(ln const-decl "real" ln_exp nil)
(ln_le2_lb const-decl "real" ln_approx nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(ln_expt formula-decl nil ln_exp nil)
(integer nonempty-type-from-decl nil integers nil)
(ln_gt1_ub const-decl "real" ln_approx nil))
nil))
(ln_lb_TCC1 0
(ln_lb_TCC1-1 nil 3296503304
("" (skosimp)
(("" (rewrite "div_mult_pos_gt1") (("" (assert) nil nil)) nil))
nil)
((div_mult_pos_gt1 formula-decl nil extra_real_props 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)
(>= const-decl "bool" reals 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)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(ln_lb_TCC2 0
(ln_lb_TCC2-1 nil 3296503304 ("" (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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_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))
shostak))
(ln_bounds 0
(ln_bounds-1 nil 3296503392
("" (expand "ln_ub")
(("" (expand "ln_lb")
(("" (skosimp*)
(("" (case-replace "px!1 < 1")
(("1" (lemma "ln_gt1_bounds" ("x" "1/px!1" "n" "n!1"))
(("1"
(lemma "div_mult_pos_lt2" ("py" "px!1" "x" "1" "z" "1"))
(("1" (assert)
(("1" (flatten)
(("1" (lemma "ln_div" ("px" "1" "py" "px!1"))
(("1" (rewrite "ln_1")
(("1"
(lemma "both_sides_times_neg_lt1" ("nz" "-1"))
(("1"
(inst-cp - "ln(px!1)"
"-ln_gt1_ub(n!1, 1 / px!1)")
(("1"
(inst - "-ln_gt1_lb(n!1, 1 / px!1)"
"ln(px!1)")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case-replace "px!1=1")
(("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (lemma "ln_gt1_bounds" ("n" "n!1" "x" "px!1"))
(("2" (assert)
(("2" (flatten) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ln_lb const-decl "real" ln_approx 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)
(< const-decl "bool" reals nil) (>= const-decl "bool" reals 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)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(ln_1 formula-decl nil ln_exp nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(ln_gt1_ub const-decl "real" ln_approx nil)
(ln const-decl "real" ln_exp nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(ln_gt1_lb const-decl "real" ln_approx nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(both_sides_times_neg_lt1 formula-decl nil real_props nil)
(ln_div formula-decl nil ln_exp nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(ln_gt1_bounds formula-decl nil ln_approx 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)
(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 "[T, T -> boolean]" equalities nil)
(ln_ub const-decl "real" ln_approx nil))
shostak)))
¤ Dauer der Verarbeitung: 0.35 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.
|
