|
(ln_exp_def
(expt_exp 0
(expt_exp-1 nil 3432401063
("" (skosimp)
(("" (lemma "expt_alt_def" ("x" "y!1" "i" "n!1"))
(("" (assert) (("" (expand "^") (("" (propax) nil nil)) nil))
nil))
nil))
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)
(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 nonempty-type-from-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)
(expt_alt_def formula-decl nil ln_exp "lnexp_fnd/")
(^ const-decl "real" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(posreal_expt application-judgement "posreal" exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(nn_root_def_TCC1 0
(nn_root_def_TCC1-1 nil 3432416668
("" (skosimp) (("" (assert) nil nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(nn_root_def 0
(nn_root_def-1 nil 3432416669
("" (skosimp)
(("" (case-replace "z!1=0")
(("1" (rewrite "nn_root_0n") nil nil)
("2" (assert)
(("2" (lemma "expt_nn_root" ("x" "z!1" "pn" "pn!1"))
(("2"
(lemma "expt_alt_def"
("x" "exp(ln(z!1) / pn!1)" "i" "pn!1"))
(("2" (assert)
(("2" (rewrite "ln_exp")
(("2" (lemma "div_cancel1")
(("2" (inst - "pn!1" "ln(z!1)")
(("2" (replace -1)
(("2" (rewrite "exp_ln")
(("2" (hide -1)
(("2"
(lemma "both_sides_nn_root"
("x" "z!1" "y" "exp(ln(z!1) / pn!1)^pn!1"
"pn" "pn!1"))
(("2"
(lemma "nn_root_expt"
("x" "exp(ln(z!1) / pn!1)" "pn" "pn!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(nnreal type-eq-decl nil real_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(nn_root_0n formula-decl nil nn_root nil)
(expt_nn_root formula-decl nil nn_root nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(div_cancel1 formula-decl nil real_props nil)
(nn_root_expt formula-decl nil nn_root nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(posreal_exp application-judgement "posreal" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(^ const-decl "nnreal" real_expt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(both_sides_nn_root formula-decl nil nn_root nil)
(exp_ln formula-decl nil ln_exp "lnexp_fnd/")
(nonzero_real nonempty-type-eq-decl nil reals nil)
(ln_exp formula-decl nil ln_exp "lnexp_fnd/")
(expt_alt_def formula-decl nil ln_exp "lnexp_fnd/")
(integer nonempty-type-from-decl nil integers nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(ln const-decl "real" ln_exp "lnexp_fnd/")
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/")
(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)
(real_div_nzreal_is_real application-judgement "real" reals nil))
shostak))
(nn_rational_expt_def 0
(nn_rational_expt_def-1 nil 3432418222
("" (skosimp)
(("" (expand "nn_rational_expt")
(("" (rewrite "expt_exp")
(("1" (rewrite "nn_root_def")
(("1" (rewrite "ln_exp")
(("1" (lemma "rational_def" ("r" "q!1"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "q!1")
(("2" (expand ">=" -1)
(("2" (expand "<=" -1)
(("2" (split)
(("1" (lemma "numerator_pos" ("r" "q!1"))
(("1" (assert) nil nil)) nil)
("2" (lemma "numerator_is_zero" ("r" "q!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nn_rational_expt const-decl "nnreal" nn_rational_expt 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)
(numerator_pos formula-decl nil rational_props_aux nil)
(numerator_is_zero formula-decl nil rational_props_aux nil)
(<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nn_root_def formula-decl nil ln_exp_def nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(denominator const-decl "posnat" rational_props_aux nil)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(ln const-decl "real" ln_exp "lnexp_fnd/")
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(rational_def formula-decl nil rational_props_aux nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(ln_exp formula-decl nil ln_exp "lnexp_fnd/")
(real_times_real_is_real application-judgement "real" reals nil)
(posreal_expt application-judgement "posreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation 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)
(nnrat nonempty-type-eq-decl nil rationals nil)
(numerator const-decl "int" rational_props_aux nil)
(rat nonempty-type-eq-decl nil rationals 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)
(expt_exp formula-decl nil ln_exp_def nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(nnreal_expt_def 0
(nnreal_expt_def-2 nil 3453736998
("" (skosimp)
(("" (expand "nnreal_expt")
(("" (assert)
(("" (case-replace "z!1=0")
(("1" (rewrite "exp_0") nil nil)
("2" (assert)
(("2" (case "z!1>0")
(("1" (hide 1)
(("1" (lemma "trich_lt" ("x" "y!1" "y" "1"))
(("1" (split)
(("1" (assert)
(("1"
(typepred "glb(extend[real, nnreal, bool, FALSE]
({z | EXISTS q: q <= z!1 AND z = nn_rational_expt(y!1, q)}))")
(("1"
(name-replace "GLB"
"glb(extend[real, nnreal, bool, FALSE]
({z | EXISTS q: q <= z!1 AND z = nn_rational_expt(y!1, q)}))")
(("1" (expand "extend")
(("1" (expand "greatest_lower_bound?")
(("1"
(flatten)
(("1"
(expand "lower_bound?")
(("1"
(lemma
"trich_lt"
("x"
"GLB"
"y"
"exp(z!1 * ln(y!1))"))
(("1"
(split -1)
(("1"
(hide 1)
(("1"
(lemma "exp_continuous")
(("1"
(expand "continuous?")
(("1"
(inst - "z!1 * ln(y!1)")
(("1"
(expand "continuous?")
(("1"
(name
"EPS"
"exp(z!1 * ln(y!1))-GLB")
(("1"
(inst - "EPS")
(("1"
(skosimp)
(("1"
(lemma
"ln_strict_increasing")
(("1"
(expand
"strict_increasing?")
(("1"
(inst
-
"y!1"
"1")
(("1"
(rewrite
"ln_1")
(("1"
(assert)
(("1"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"delta!1"
"py"
"abs(ln(y!1))"))
(("1"
(inst
-7
"exp(z!1 * ln(y!1))")
(("1"
(split
-7)
(("1"
(assert)
nil
nil)
("2"
(skosimp)
(("2"
(typepred
"s!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(lemma
"both_sides_times_neg_le1"
("nz"
"ln(y!1)"
"y"
"q!1"
"x"
"z!1"))
(("2"
(assert)
(("2"
(lemma
"exp_increasing")
(("2"
(expand
"increasing?")
(("2"
(inst
-
"z!1 * ln(y!1)"
"q!1 * ln(y!1)")
(("2"
(assert)
(("2"
(rewrite
"nn_rational_expt_def")
(("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))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3"
(hide -3)
(("3"
(name
"EPS"
"GLB-exp(z!1 * ln(y!1))")
(("3"
(case "EPS>0")
(("1"
(lemma "exp_continuous")
(("1"
(expand "continuous?")
(("1"
(inst
-
"z!1 * ln(y!1)")
(("1"
(expand
"continuous?")
(("1"
(inst - "EPS")
(("1"
(skosimp)
(("1"
(lemma
"ln_strict_increasing")
(("1"
(expand
"strict_increasing?")
(("1"
(inst
-
"y!1"
"1")
(("1"
(rewrite
"ln_1")
(("1"
(assert)
(("1"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"delta!1"
"py"
"abs(ln(y!1))"))
(("1"
(lemma
"density_positive"
("x"
"max(0,z!1-delta!1 / abs(ln(y!1)))"
"y"
"z!1"))
(("1"
(assert)
(("1"
(split)
(("1"
(skosimp)
(("1"
(inst
-
"r!1*ln(y!1)")
(("1"
(lemma
"abs_mult"
("x"
"r!1-z!1"
"y"
"ln(y!1)"))
(("1"
(replace
-1)
(("1"
(lemma
"div_mult_pos_lt2"
("x"
"abs(r!1 - z!1)"
"py"
"abs(ln(y!1))"
"z"
"delta!1"))
(("1"
(replace
-1
*
rl)
(("1"
(hide
-1
-2)
(("1"
(name-replace
"DELTA"
"delta!1 / abs(ln(y!1))")
(("1"
(expand
"abs"
-5)
(("1"
(assert)
(("1"
(lemma
"both_sides_times_neg_lt1"
("nz"
"ln(y!1)"
"y"
"r!1"
"x"
"z!1"))
(("1"
(assert)
(("1"
(lemma
"exp_strict_increasing")
(("1"
(expand
"strict_increasing?")
(("1"
(inst
-
"z!1 * ln(y!1)"
"r!1 * ln(y!1)")
(("1"
(assert)
(("1"
(inst
-
"exp(r!1 * ln(y!1))")
(("1"
(assert)
nil
nil)
("2"
(inst
+
"r!1")
(("2"
(assert)
(("2"
(rewrite
"nn_rational_expt_def")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name-replace
"DELTA"
"delta!1 / abs(ln(y!1))")
(("2"
(hide-all-but
(-1
-9
1))
(("2"
(grind)
nil
nil))
nil))
nil)
("3"
(name-replace
"DELTA"
"delta!1 / abs(ln(y!1))")
(("3"
(hide-all-but
(-1
-9
1))
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (replace -1) (("2" (assert) nil nil)) nil))
nil)
("3" (assert)
(("3"
(typepred "lub(extend[real, nnreal, bool, FALSE]
({z | EXISTS q: q <= z!1 AND z = nn_rational_expt(y!1, q)}))")
(("3"
(name-replace "LUB"
"lub(extend[real, nnreal, bool, FALSE]
({z | EXISTS q: q <= z!1 AND z = nn_rational_expt(y!1, q)}))")
(("3" (expand "least_upper_bound?")
(("3" (expand "extend")
(("3"
(expand "upper_bound?")
(("3"
(flatten)
(("3"
(lemma "ln_strict_increasing")
(("3"
(expand "strict_increasing?")
(("3"
(inst - "1" "y!1")
(("3"
(rewrite "ln_1")
(("3"
(assert)
(("3"
(lemma
"trich_lt"
("x"
"LUB"
"y"
"exp(z!1 * ln(y!1))"))
(("3"
(split)
(("1"
(hide -4 1)
(("1"
(name
"EPS"
"exp(z!1 * ln(y!1))-LUB")
(("1"
(lemma
"exp_continuous")
(("1"
(expand
"continuous?")
(("1"
(inst
-
"z!1*ln(y!1)")
(("1"
(expand
"continuous?")
(("1"
(inst
-
"EPS")
(("1"
(skosimp)
(("1"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"delta!1"
"py"
"ln(y!1)"))
(("1"
(lemma
"density_positive"
("x"
"max(0,z!1-delta!1 / ln(y!1))"
"y"
"z!1"))
(("1"
(assert)
(("1"
(split)
(("1"
(skosimp)
(("1"
(inst
-4
"r!1*ln(y!1)")
(("1"
(lemma
"abs_mult"
("x"
"r!1-z!1"
"y"
"ln(y!1)"))
(("1"
(replace
-1)
(("1"
(lemma
"div_mult_pos_lt2"
("x"
" abs(r!1 - z!1)"
"py"
"abs(ln(y!1))"
"z"
"delta!1"))
(("1"
(replace
-1
*
rl)
(("1"
(expand
"abs")
(("1"
(assert)
(("1"
(hide
-1
-2)
(("1"
(lemma
"both_sides_times_pos_lt1"
("pz"
"ln(y!1)"
"x"
"r!1"
"y"
"z!1"))
(("1"
(assert)
(("1"
(lemma
"exp_strict_increasing")
(("1"
(expand
"strict_increasing?")
(("1"
(inst
-
"r!1 * ln(y!1)"
"z!1 * ln(y!1)")
(("1"
(assert)
(("1"
(inst
-
"exp(r!1*ln(y!1))")
(("1"
(assert)
nil
nil)
("2"
(inst
+
"r!1")
(("2"
(assert)
(("2"
(rewrite
"nn_rational_expt_def")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"abs")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(name-replace
"DELTA"
"delta!1 / ln(y!1)")
(("2"
(hide-all-but
(-1
-8
1))
(("2"
(grind)
nil
nil))
nil))
nil)
("3"
(name-replace
"DELTA"
"delta!1 / ln(y!1)")
(("3"
(hide-all-but
(-1
-8
1))
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3"
(inst
-4
"exp(z!1 * ln(y!1))")
(("3"
(split)
(("1"
(assert)
nil
nil)
("2"
(skosimp)
(("2"
(hide 2)
(("2"
(typepred
"s!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(lemma
"both_sides_times_pos_le1"
("pz"
"ln(y!1)"
"x"
"q!1"
"y"
"z!1"))
(("2"
(assert)
(("2"
(lemma
"exp_increasing")
(("2"
(expand
"increasing?")
(("2"
(inst
-
"q!1 * ln(y!1)"
"z!1 * ln(y!1)")
(("2"
(assert)
(("2"
(rewrite
"nn_rational_expt_def")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_expt const-decl "nnreal" nnreal_expt nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(nnreal type-eq-decl nil real_types nil)
(exp_0 formula-decl nil ln_exp "lnexp_fnd/")
(> const-decl "bool" reals nil)
(trich_lt formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.342 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.
|
