| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/power/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 162 kB |
|
Quelle ln_exp_def.prfSprache: Lisp |
|||||||||||||||
|
(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) (both_sides_times_pos_le1 formula-decl nil real_props nil) (EPS skolem-const-decl "real" ln_exp_def nil) (r!1 skolem-const-decl "rat" ln_exp_def nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs 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) (lower_bound? const-decl "bool" bounded_real_defs nil) (exp_continuous formula-decl nil ln_exp "lnexp_fnd/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (ln_1 formula-decl nil ln_exp "lnexp_fnd/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (increasing? const-decl "bool" real_fun_preds "reals/") (nn_rational_expt_def formula-decl nil ln_exp_def nil) (exp_increasing formula-decl nil ln_exp "lnexp_fnd/") (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_le1 formula-decl nil real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (ln_strict_increasing formula-decl nil ln_exp "lnexp_fnd/") (EPS skolem-const-decl "real" ln_exp_def nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (continuous? const-decl "bool" continuous_functions "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (continuous? const-decl "bool" continuous_functions "analysis/") (EPS skolem-const-decl "real" ln_exp_def nil) (density_positive formula-decl nil rational_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (rat nonempty-type-eq-decl nil rationals nil) (nzreal nonempty-type-eq-decl nil reals nil) (minus_real_is_real application-judgement "real" reals nil) (y!1 skolem-const-decl "posreal" ln_exp_def nil) (r!1 skolem-const-decl "rat" ln_exp_def nil) (z!1 skolem-const-decl "nnreal" ln_exp_def nil) (exp_strict_increasing formula-decl nil ln_exp "lnexp_fnd/") (both_sides_times_neg_lt1 formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (abs_mult formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/") (ln const-decl "real" ln_exp "lnexp_fnd/") (NOT const-decl "[bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (greatest_lower_bound? const-decl "bool" bounded_real_defs nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (glb const-decl "{x | greatest_lower_bound?(x, SB)}" bounded_real_defs nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (nnrat nonempty-type-eq-decl nil rationals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nn_rational_expt const-decl "nnreal" nn_rational_expt nil) (real_times_real_is_real application-judgement "real" reals nil)) nil) (nnreal_expt_def-1 nil 3432419188 ("" (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" (rewrite "continuity_def") (("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 1) (("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" (rewrite "continuity_def") (("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" (rewrite "ln_1") (("2" (rewrite "exp_0") nil 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" (rewrite "continuity_def") (("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) (exp_0 formula-decl nil ln_exp "lnexp_fnd/") (exp_continuous formula-decl nil ln_exp "lnexp_fnd/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (ln_1 formula-decl nil ln_exp "lnexp_fnd/") (increasing? const-decl "bool" real_fun_preds "reals/") (exp_increasing formula-decl nil ln_exp "lnexp_fnd/") (ln_strict_increasing formula-decl nil ln_exp "lnexp_fnd/") (continuity_def formula-decl nil continuous_functions "analysis/") (exp_strict_increasing formula-decl nil ln_exp "lnexp_fnd/") (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/") (ln const-decl "real" ln_exp "lnexp_fnd/") (nn_rational_expt const-decl "nnreal" nn_rational_expt nil)) shostak)) (real_expt_def_TCC1 0 (real_expt_def_TCC1-1 nil 3432422172 ("" (subtype-tcc) nil nil) nil nil)) (real_expt_def 0 (real_expt_def-1 nil 3432422300 ("" (skosimp) (("" (expand "^") (("" (case-replace "x!1>=0") (("1" (rewrite "nnreal_expt_def") nil nil) ("2" (assert) (("2" (rewrite "nnreal_expt_def") (("2" (rewrite "ln_div") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((^ const-decl "nnreal" real_expt nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (ln_div formula-decl nil ln_exp "lnexp_fnd/") (real_minus_real_is_real application-judgement "real" reals nil) (ln_1 formula-decl nil ln_exp "lnexp_fnd/") (- const-decl "[numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_expt_def formula-decl nil ln_exp_def 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) (nnreal type-eq-decl nil real_types 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)) shostak)) (nn_log_def_TCC1 0 (nn_log_def_TCC1-1 nil 3432421334 ("" (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) (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_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) (/= const-decl "boolean" notequal nil)) nil)) (nn_log_def_TCC2 0 (nn_log_def_TCC2-1 nil 3432421334 ("" (skosimp) (("" (split) (("1" (flatten) (("1" (lemma "ln_strict_increasing") (("1" (expand "strict_increasing?") (("1" (inst - "1" "r!1") (("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "ln_strict_increasing") (("2" (expand "strict_increasing?") (("2" (inst - "r!1" "1") (("2" (rewrite "ln_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ln_strict_increasing formula-decl nil ln_exp "lnexp_fnd/") (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) (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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ln_1 formula-decl nil ln_exp "lnexp_fnd/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (nn_log_def 0 (nn_log_def-1 nil 3432421335 ("" (skosimp) (("" (lemma "nn_expt_log" ("y" "y!1" "ne1x" "r!1")) (("" (rewrite "nnreal_expt_def") (("" (lemma "ln_exp" ("x" "nn_log(r!1)(y!1) * ln(r!1)")) (("" (replace -2) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal 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) (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) (nn_expt_log formula-decl nil nn_log nil) (ln const-decl "real" ln_exp "lnexp_fnd/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (ln_exp formula-decl nil ln_exp "lnexp_fnd/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (nn_log const-decl "nnreal" nn_log nil) (nnreal type-eq-decl nil real_types nil) (nnreal_expt_def formula-decl nil ln_exp_def nil)) shostak)) (log_def_TCC1 0 (log_def_TCC1-1 nil 3432421672 ("" (skosimp) (("" (typepred "ne1x!1") (("" (lemma "trich_lt" ("x" "ne1x!1" "y" "1")) (("" (split) (("1" (lemma "ln_strict_increasing") (("1" (expand "strict_increasing?") (("1" (inst - "ne1x!1" "1") (("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (lemma "ln_strict_increasing") (("3" (expand "strict_increasing?") (("3" (inst - "1" "ne1x!1") (("3" (rewrite "ln_1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal 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) (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) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (ln_1 formula-decl nil ln_exp "lnexp_fnd/") (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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ln_strict_increasing formula-decl nil ln_exp "lnexp_fnd/") (trich_lt formula-decl nil real_props nil)) nil)) (log_def 0 (log_def-1 nil 3432421673 ("" (skosimp) (("" (typepred "ne1x!1") (("" (lemma "trich_lt" ("x" "ne1x!1" "y" "1")) (("" (split -1) (("1" (expand "log") (("1" (expand "log") (("1" (assert) (("1" (case-replace "y!1<=1") (("1" (rewrite "nn_log_def") nil nil) ("2" (assert) (("2" (rewrite "nn_log_def") (("1" (rewrite "ln_div") (("1" (assert) nil nil)) nil) ("2" (rewrite "div_mult_pos_le1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "ln_1") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "log") (("3" (expand "log") (("3" (assert) (("3" (case-replace "y!1>=1") (("1" (rewrite "nn_log_def") nil nil) ("2" (assert) (("2" (rewrite "nn_log_def") (("1" (rewrite "ln_div") (("1" (assert) nil nil)) nil) ("2" (rewrite "div_mult_pos_ge1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal 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) (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) (log const-decl "real" log nil) (<= const-decl "bool" reals nil) (nn_log_def formula-decl nil ln_exp_def nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (ln_1 formula-decl nil ln_exp "lnexp_fnd/") (real_minus_real_is_real application-judgement "real" reals nil) (ln_div formula-decl nil ln_exp "lnexp_fnd/") (div_mult_pos_le1 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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_gt_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) (real_div_nzreal_is_real application-judgement "real" reals nil) (log const-decl "real" log nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (trich_lt formula-decl nil real_props nil)) shostak)) (log_continuous 0 (log_continuous-1 nil 3432579214 ("" (skosimp) (("" (expand "continuous") (("" (skosimp) (("" (case-replace "log(ne1x!1)=lambda (y:posreal): ln(y)/ln(ne1x!1)") (("1" (hide -1) (("1" (lemma "ln_continuous") (("1" (lemma "scal_cont_fun[posreal]" ("f" "ln" "u" "1/ln(ne1x!1)")) (("1" (assert) (("1" (hide -2) (("1" (expand "continuous" -1) (("1" (inst - "x0!1") (("1" (expand "*") (("1" (case-replace "(LAMBDA (x: posreal): 1 / ln(ne1x!1) * ln(x))=(LAMBDA (y: posreal): ln(y) / ln(ne1x!1))") (("1" (hide -1 2) (("1" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "/=") (("2" (lemma "ln_strict_increasing") (("2" (expand "strict_increasing?") (("2" (case "ne1x!1<1") (("1" (inst - "ne1x!1" "1") (("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "1" "ne1x!1") (("2" (rewrite "ln_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("1" (lemma "log_def" ("ne1x" "ne1x!1" "y" "x!1")) (("1" (expand "log" -1) (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "ln_strict_increasing") (("2" (expand "strict_increasing?") (("2" (case "ne1x!1<1") (("1" (inst - "ne1x!1" "1") (("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "1" "ne1x!1") (("2" (rewrite "ln_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "/=") (("3" (lemma "ln_strict_increasing") (("3" (expand "strict_increasing?") (("3" (case "ne1x!1<1") (("1" (inst - "ne1x!1" "1") (("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "1" "ne1x!1") (("2" (rewrite "ln_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_div_nzreal_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (/= const-decl "boolean" notequal nil) (log const-decl "real" log nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (ln const-decl "real" ln_exp "lnexp_fnd/") (ln_continuous formula-decl nil ln_exp "lnexp_fnd/") (ln_strict_increasing formula-decl nil ln_exp "lnexp_fnd/") (< const-decl "bool" reals nil) (ln_1 formula-decl nil ln_exp "lnexp_fnd/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (ne1x!1 skolem-const-decl "{r | r /= 1}" ln_exp_def nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (scal_cont_fun formula-decl nil continuous_functions "analysis/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (log const-decl "real" log nil) (log_def formula-decl nil ln_exp_def nil)) shostak)) (log_derivable_TCC1 0 (log_derivable_TCC1-1 nil 3432580342 ("" (expand "deriv_domain?") (("" (skosimp*) (("" (inst + e!1/2) (("" (grind) nil nil)) nil)) nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (log_derivable_TCC2 0 (log_derivable_TCC2-1 nil 3432580342 ("" (expand "not_one_element?") (("" (skosimp) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (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) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (log_derivable_TCC3 0 (log_derivable_TCC3-1 nil 3432580342 ("" (skosimp) (("" (hide -1) (("" (skosimp) (("" (typepred "y!1") (("" (rewrite "zero_times3") (("" (hide -1 -2) (("" (lemma "ln_strict_increasing") (("" (expand "strict_increasing?") (("" (case "ne1x!1<1") (("1" (inst - "ne1x!1" "1") (("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "1" "ne1x!1") (("2" (rewrite "ln_1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (>= 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) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ln_1 formula-decl nil ln_exp "lnexp_fnd/") (< const-decl "bool" reals nil) (ln_strict_increasing formula-decl nil ln_exp "lnexp_fnd/") (/= const-decl "boolean" notequal nil) (ln const-decl "real" ln_exp "lnexp_fnd/") (zero_times3 formula-decl nil real_props nil)) nil)) (log_derivable 0 (log_derivable-1 nil 3432580630 ("" (skosimp) (("" (lemma "ln_derivable") (("" (flatten) (("" (case "ln(ne1x!1)=0") (("1" (lemma "ln_eq_0" ("px" "ne1x!1")) (("1" (assert) nil nil)) nil) ("2" (lemma "scal_derivable_fun[posreal]" ("f" "ln" "b" "1/ln(ne1x!1)")) (("1" (assert) (("1" (lemma "deriv_scal_fun[posreal]" ("b" "1 / ln(ne1x!1)" "ff" "ln")) (("1" (replace -4) (("1" (expand "*" -1 2) (("1" (case-replace "(1 / ln(ne1x!1) * ln)=log(ne1x!1)") (("1" (assert) nil nil) ("2" (apply-extensionality :hide? t) (("2" (hide-all-but (1 2)) (("2" (lemma "log_def" ("ne1x" "ne1x!1" "y" "x!1")) (("2" (expand "log" -1) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((ln_derivable formula-decl nil ln_exp "lnexp_fnd/") (/= const-decl "boolean" notequal nil) (ln const-decl "real" ln_exp "lnexp_fnd/") (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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (ln_eq_0 formula-decl nil ln_exp "lnexp_fnd/") (real_times_real_is_real application-judgement "real" reals nil) (log const-decl "real" log nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (log const-decl "real" log nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (log_def formula-decl nil ln_exp_def nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (scal_derivable_fun formula-decl nil derivatives "analysis/") (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) shostak)) (real_expt_continuous 0 (real_expt_continuous-1 nil 3432581634 ("" (skolem + ("a!1")) (("" (case-replace "(LAMBDA y: y ^ a!1)=lambda y: exp(a!1*ln(y))") (("1" (hide -1) (("1" (lemma "ln_continuous") (("1" (lemma "exp_continuous") (("1" (lemma "scal_fun_continuous[posreal]" ("u" "a!1" "h" "ln")) (("1" (lemma "composition_cont_fun[posreal,real]" ("f" "*[posreal](a!1, ln)" "g" "exp")) (("1" (assert) (("1" (expand "o") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (rewrite "real_expt_def") nil nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals 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) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "nnreal" real_expt 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) (ln_continuous formula-decl nil ln_exp "lnexp_fnd/") (scal_fun_continuous judgement-tcc nil continuous_functions "analysis/") (continuous? const-decl "bool" continuous_functions "analysis/") (continuous_fun nonempty-type-eq-decl nil continuous_functions "analysis/") (O const-decl "T3" function_props nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (composition_cont_fun formula-decl nil composition_continuous "analysis/") (exp_continuous formula-decl nil ln_exp "lnexp_fnd/") (real_expt_def formula-decl nil ln_exp_def nil)) shostak)) (real_expt_derivable_TCC1 0 (real_expt_derivable_TCC1-1 nil 3432605120 ("" (assuming-tcc) nil nil) ((fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (real_expt_derivable 0 (real_expt_derivable-1 nil 3432605121 ("" (skosimp) (("" (case "FORALL x: (LAMBDA y: y ^ x) = (LAMBDA y: exp(x * ln(y)))") (("1" (inst-cp - "x!1") (("1" (inst - "x!1-1") (("1" (replace -2) (("1" (hide -2) (("1" (lemma "ln_derivable") (("1" (lemma "exp_deriv") (("1" (flatten) (("1" (lemma "derivable_scal[posreal]" ("b" "x!1" "ff" "ln")) (("1" (lemma "deriv_scal_fun[posreal]" ("b" "x!1" "ff" "ln")) (("1" (replace -6) (("1" (expand "*" -1 2) (("1" (lemma "composition_derivable_fun[posreal,real]" ("f" "x!1*ln" "g" "exp")) (("1" (assert) (("1" (lemma "deriv_comp_fun[posreal,real]" ("ff" "x!1*ln" "gg" "exp")) (("1" (replace -3) (("1" (replace -6) (("1" (expand "o") (("1" (expand "*") (("1" (replace -1) (("1" (replace -2) (("1" (apply-extensionality :hide? t) (("1" (hide-all-but (-9 1)) (("1" (hide -1) (("1" (lemma "real_expt_def" ("y" "x!2" "x" "x!1-1")) (("1" (replace -1) (("1" (assert) (("1" (rewrite "exp_diff") (("1" (rewrite "exp_ln") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "x!2+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (assert) (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (inst + e!1/2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (assert) (("4" (expand "not_one_element?") (("4" (skosimp*) (("4" (inst + "x!2+1") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but 1) (("5" (expand "deriv_domain?") (("5" (skosimp*) (("5" (inst + e!1/2) (("5" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (apply-extensionality :hide? t) (("2" (rewrite "real_expt_def") nil nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/") (ln const-decl "real" ln_exp "lnexp_fnd/") (^ const-decl "nnreal" real_expt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nnreal type-eq-decl nil real_types 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) (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) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (exp_deriv formula-decl nil ln_exp "lnexp_fnd/") (derivable_scal judgement-tcc nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (real_expt_def formula-decl nil ln_exp_def nil) (exp_ln formula-decl nil ln_exp "lnexp_fnd/") (exp_diff formula-decl nil ln_exp "lnexp_fnd/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (O const-decl "T3" function_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (ln_derivable formula-decl nil ln_exp "lnexp_fnd/")) shostak)))
¤ Dauer der Verarbeitung: 0.134 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26