| products/Sources/formale Sprachen/PVS/lnexp/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: direct.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(ln_exp
(ln_1 0 (ln_1-1 nil 3253532189 ("" (expand "ln") (("" (expand "Integral") (("" (propax) nil nil)) nil)) nil) nil nil)) (ln_mult 0 (ln_mult-1 nil 3253532189 ("" (skosimp*) (("" (case "derivable[posreal](LAMBDA (x: posreal): ln(py!1 * x))") (("1" (lemma "ln_derivable") (("1" (flatten) (("1" (case "deriv(LAMBDA (x: posreal): ln(py!1*x)) = deriv(LAMBDA (x: posreal): ln(x) (("1" (lemma "derivs_eq[posreal]") (("1" (inst?) (("1" (assert) (("1" (case-replace "(LAMBDA (x: posreal): ln(x)) = ln") (("1" (assert) (("1" (hide -1) (("1" (replace -3) (("1" (assert) (("1" (skosimp*) (("1" (expand "+ ") (("1" (expand "const_fun") (("1" (case "(LAMBDA (x: posreal): ln(py!1 * x))(1) = (LAMBDA (x_824: posreal): ln(x_8 (("1" (assert) (("1" (hide -2) (("1" (rewrite "ln_1") (("1" (assert) (("1" (reveal -1) (("1" (replace -2 * rl) (("1" (case-replace "(LAMBDA (x: posreal): ln(py!1 * x))(px!1) = (LAMBDA (x_824: posreal): ln( (("1" (hide -2) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1/2") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "deriv_composition[posreal,posreal]") (("1" (case-replace "(LAMBDA (x: posreal): ln(x)) = ln") (("1" (hide -1) (("1" (replace -3) (("1" (apply-extensionality 1 :hide? t) (("1" (inst - "(LAMBDA (t: posreal): py!1*t)" "ln" "x!1") (("1" (assert) (("1" (case "derivable((LAMBDA (t: posreal): py!1 * t), x!1) ") (("1" (assert) (("1" (expand "derivable" -3) (("1" (inst -3 "py!1*x!1") (("1" (assert) (("1" (expand "o ") (("1" (expand "deriv" 1) (("1" (case "deriv(ln)(py!1*x!1) = (LAMBDA (t: posreal): 1 / t)(py!1*x!1)") (("1" (expand "deriv" -1) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "deriv[posreal]((LAMBDA (t: posreal): py!1 * t), x!1) = py!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "deriv_scal[posreal]") (("2" (inst -1 "py!1" "I[posreal]" "x!1") (("2" (split -1) (("1" (expand "I") (("1" (expand "*") (("1" (replace -1) (("1" (lemma "deriv_identity[posreal]") (("1" (expand "I") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "identity_derivable[posreal]") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "scal_derivable[posreal]") (("2" (inst -1 "py!1" "I" "x!1") (("2" (lemma "identity_derivable[posreal]") (("2" (inst?) (("2" (split -2) (("1" (expand "I") (("1" (expand "*") (("1" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) nil nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (case-replace "(LAMBDA (x: posreal): ln(x)) = ln") (("3" (apply-extensionality 1 :hide? t) nil nil)) nil) ("4" (propax) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "ln_derivable") (("2" (flatten) (("2" (assert) (("2" (lemma "scal_derivable[posreal]") (("2" (expand "derivable" 1) (("2" (skosimp*) (("2" (inst -1 "py!1" "I" "x!1") (("2" (lemma "identity_derivable[posreal]") (("2" (inst?) (("2" (lemma "composition_derivable[posreal,posreal]") (("1" (inst -1 "(LAMBDA (t:posreal): py!1*t)" "ln" "x!1") (("1" (expand "o ") (("1" (split -1) (("1" (propax) nil nil) ("2" (expand "derivable" -3) (("2" (inst -3 "py!1*x!1") (("2" (hide 2) (("2" (expand "I") (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "derivable" -3) (("3" (inst -3 "py!1*x!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!2+1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (hide-all-but (-1 1)) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((const_fun const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (ln_div 0 (ln_div-1 nil 3253532189 ("" (skosimp*) (("" (lemma "ln_mult") (("" (inst -1 "1/py!1" "py!1") (("" (assert) (("" (rewrite "ln_1") (("" (lemma "ln_mult") (("" (inst -1 "px!1" "1/py!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ln_mult formula-decl nil ln_exp nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (ln_1 formula-decl nil ln_exp 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) (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_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (ln_expt_TCC1 0 (ln_expt_TCC1-1 nil 3253532189 ("" (subtype-tcc) nil nil) nil nil)) (ln_expt 0 (ln_expt-1 nil 3253532189 ("" (skosimp*) (("" (case "(FORALL (n:nat): ln(px!1 ^ n) = n * ln(px!1))") (("1" (case-replace "i!1 >= 0") (("1" (inst?) nil nil) ("2" (expand "^") (("2" (assert) (("2" (rewrite "ln_div") (("2" (rewrite "ln_1") (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (expand "^") (("1" (expand "expt") (("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case-replace "px!1 ^ (j!1 + 1) = px!1*px!1^j!1") (("1" (rewrite "ln_mult" +) (("1" (replace -2) (("1" (hide -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "expt_plus") (("2" (expand "^" 1 2) (("2" (expand "expt") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (ln const-decl "real" ln_exp 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 "[T, T -> boolean]" equalities 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) (posreal_exp application-judgement "posreal" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation nil) (ln_div formula-decl nil ln_exp nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (ln_1 formula-decl nil ln_exp nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (i!1 skolem-const-decl "integer" ln_exp nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (ln_mult formula-decl nil ln_exp nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_plus formula-decl nil exponentiation nil)) nil)) (ln_strict_increasing 0 (ln_strict_increasing-1 nil 3253532189 ("" (lemma "positive_derivative[posreal]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "ln_derivable") (("1" (flatten) (("1" (case "deriv[posreal](ln, x!1) = deriv(ln)(x!1)") (("1" (replace -1) (("1" (replace -3) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "deriv" 1 2) (("2" (propax) nil nil)) nil)) nil) ("3" (propax) nil nil) ("4" (expand "derivable" -1) (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "ln_derivable") (("2" (flatten) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) nil nil)) (ln_increasing 0 (ln_increasing-1 nil 3253532189 ("" (lemma "ln_strict_increasing") (("" (expand "increasing?") (("" (skosimp*) (("" (expand "strict_increasing?") (("" (inst?) (("" (inst -1 "y!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing? const-decl "bool" real_fun_preds "reals/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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) (ln_strict_increasing formula-decl nil ln_exp nil)) nil)) (ln_image_all 0 (ln_image_all-1 nil 3253532189 ("" (skosimp*) (("" (lemma "ln_strict_increasing") (("" (expand "strict_increasing?") (("" (inst -1 "1" "2") (("" (assert) (("" (rewrite "ln_1") (("" (lemma "ln_expt") (("" (inst -1 "_" "2") (("" (case "(FORALL (gg: real): (EXISTS (i1,i2:int): i1 < gg/ln(2) AND gg/ln(2) < i2))") (("1" (assert) (("1" (inst -1 "y!1") (("1" (skosimp*) (("1" (case "i1!1 < i2!1") (("1" (mult-by -2 "ln(2)") (("1" (rewrite "ln_expt" -2 :dir rl) (("1" (mult-by -3 "ln(2)") (("1" (rewrite "ln_expt" -3 :dir rl) (("1" (lemma "intermediate1[posreal]") (("1" (inst -1 "2^i1!1" "2^i2!1" "ln" "y!1") (("1" (assert) (("1" (split -1) (("1" (skosimp*) (("1" (inst + "c!1") nil nil)) nil) ("2" (hide 2) (("2" (lemma "both_sides_expt_gt1_le") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "ln_derivable") (("2" (flatten) (("2" (rewrite "ln_continuous") nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lemma "axiom_of_archimedes") (("2" (inst -1 "gg!1/ln(2)") (("1" (skosimp*) (("1" (lemma "axiom_of_archimedes") (("1" (inst -1 "-gg!1/ln(2)") (("1" (skosimp*) (("1" (inst + "-i!2" "i!1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((strict_increasing? const-decl "bool" real_fun_preds "reals/")) nil)) (ln_bij 0 (ln_bij-1 nil 3253532189 ("" (lemma "ln_strict_increasing") (("" (expand "bijective?") (("" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (expand "strict_increasing?") (("1" (inst-cp - "x1!1" "x2!1") (("1" (inst - "x2!1" "x1!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (hide -1) (("2" (rewrite "ln_image_all") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (ln_image_all formula-decl nil ln_exp nil) (injective? const-decl "bool" functions 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) (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) (ln_strict_increasing formula-decl nil ln_exp nil)) nil)) (large_ln 0 (large_ln-1 nil 3253532189 ("" (skosimp*) (("" (lemma "ln_strict_increasing") (("" (expand "strict_increasing?") (("" (lemma "ln_bij") (("" (expand "bijective?") (("" (flatten) (("" (hide -1) (("" (expand "surjective?") (("" (inst -1 "a!1") (("" (skosimp*) (("" (replace -1 * rl) (("" (hide -1) (("" (inst -1 "x!1" "x!1+1") (("" (assert) (("" (inst + "1+x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ln_strict_increasing formula-decl nil ln_exp nil) (ln_bij formula-decl nil ln_exp nil) (surjective? const-decl "bool" functions nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types 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) (bijective? const-decl "bool" functions nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/")) nil)) (ln_eq_0 0 (ln_eq_0-1 nil 3297441392 ("" (skosimp*) (("" (lemma "ln_bij") (("" (expand "bijective?") (("" (flatten) (("" (expand "injective?") (("" (inst - "px!1" "1") (("" (lemma "ln_1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ln_bij formula-decl nil ln_exp 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) (ln_1 formula-decl nil ln_exp nil) (injective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil)) shostak)) (ln_ge_0 0 (ln_ge_0-1 nil 3297691676 ("" (skosimp*) (("" (lemma "ln_increasing") (("" (expand "increasing?") (("" (inst - "1" "px!1") (("" (rewrite "ln_1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((ln_increasing formula-decl nil ln_exp 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ln_1 formula-decl nil ln_exp nil) (increasing? const-decl "bool" real_fun_preds "reals/")) shostak)) (ln_gt_0 0 (ln_gt_0-1 nil 3297691602 ("" (skosimp*) (("" (lemma "ln_strict_increasing") (("" (expand "strict_increasing?") (("" (inst - "1" "px!1") (("" (rewrite "ln_1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((ln_strict_increasing formula-decl nil ln_exp 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) (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) (ln_1 formula-decl nil ln_exp nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/")) shostak)) (exp_TCC1 0 (exp_TCC1-1 nil 3253532189 ("" (inst + "(LAMBDA x: inverse(ln)(x))") (("" (lemma "bijective_inverse[posreal,real]") (("" (skosimp*) (("" (inst?) (("1" (assert) nil nil) ("2" (hide 2) (("2" (rewrite "ln_bij") nil nil)) nil)) nil)) nil)) nil)) nil) ((bijective_inverse formula-decl nil function_inverse nil) (bijective? const-decl "bool" functions nil) (ln_bij formula-decl nil ln_exp nil) (inverse const-decl "D" function_inverse nil) (ln const-decl "real" ln_exp 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)) nil)) (exp_def 0 (exp_def-1 nil 3253532189 ("" (apply-extensionality 1 :hide? t) (("1" (typepred "exp(x!1)") (("1" (lemma "bijective_inverse[posreal,real]") (("1" (inst?) (("1" (ground) nil nil) ("2" (rewrite "ln_bij") nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "bijective_inverse[posreal,real]") (("2" (inst?) (("1" (ground) nil nil) ("2" (hide 2) (("2" (rewrite "ln_bij") nil nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (bijective? const-decl "bool" functions nil) (ln_bij formula-decl nil ln_exp nil) (bijective_inverse formula-decl nil function_inverse nil) (inverse const-decl "D" function_inverse nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil) (ln const-decl "real" ln_exp 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)) nil)) (exp_bij 0 (exp_bij-1 nil 3253532189 ("" (rewrite "exp_def") (("" (assert) (("" (lemma "bijective_inverse_is_bijective[posreal,real]") (("" (inst?) (("" (hide 2) (("" (rewrite "ln_bij") nil nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (ln const-decl "real" ln_exp nil) (ln_bij formula-decl nil ln_exp nil) (bijective_inverse_is_bijective judgement-tcc nil function_inverse 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) (exp_def formula-decl nil ln_exp nil)) nil)) (ln_exp 0 (ln_exp-1 nil 3253532189 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)) (exp_ln 0 (exp_ln-1 nil 3253532189 ("" (skosimp*) (("" (assert) (("" (typepred "exp(ln(py!1))") (("" (lemma "ln_bij") (("" (expand "bijective?") (("" (flatten) (("" (expand "injective?") (("" (inst -1 "py!1" "exp(ln(py!1))") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ln_bij formula-decl nil ln_exp 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) (injective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions 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) (= const-decl "[T, T -> boolean]" equalities nil) (ln const-decl "real" ln_exp nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil)) nil)) (ln_e 0 (ln_e-1 nil 3253532189 ("" (assert) (("" (expand "e") (("" (assert) nil nil)) nil)) nil) ((e const-decl "posreal" ln_exp nil)) nil)) (ln_2_bnds 0 (ln_2_bnds-1 nil 3253532189 ("" (lemma "Integral_bound[posreal]") (("1" (inst -1 "1" "1" "2" "(LAMBDA (t: posreal): 1/t)" "1/2") (("1" (assert) (("1" (case-replace "Integral(1, 2, (LAMBDA (t: posreal): 1 / t)) = ln(2)") (("1" (rewrite "ln_prep") (("1" (assert) (("1" (split -2) (("1" (propax) nil nil) ("2" (skosimp*) (("2" (hide-all-but 1) (("2" (prop) (("1" (mult-by 1 "x!1") (("1" (assert) nil nil)) nil) ("2" (mult-by 1 "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ln") (("2" (propax) nil nil)) nil) ("3" (rewrite "ln_prep") nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!1") (("2" (inst + "x!1/2") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) nil nil)) (exp_int_TCC1 0 (exp_int_TCC1-1 nil 3253532189 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)) (exp_int 0 (exp_int-1 nil 3253532189 ("" (skosimp*) (("" (typepred "exp(i!1)") (("" (lemma "ln_expt") (("" (inst?) (("" (rewrite "ln_e") (("" (assert) (("" (lemma "ln_bij") (("" (expand "bijective?") (("" (flatten) (("" (expand "injective?") (("" (inst -1 "exp(i!1)" "e^i!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (exp const-decl "{py | x = ln(py)}" ln_exp nil) (ln const-decl "real" ln_exp 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) (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) (e const-decl "posreal" ln_exp 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) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posreal_exp application-judgement "posreal" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (bijective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (int nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (ln_bij formula-decl nil ln_exp nil) (ln_e formula-decl nil ln_exp nil) (ln_expt formula-decl nil ln_exp nil)) nil)) (exp_sum 0 (exp_sum-1 nil 3253532189 ("" (skosimp*) (("" (transform-both 1 "ln(%1)") (("1" (assert) (("1" (hide 2) (("1" (rewrite "ln_mult") (("1" (rewrite "ln_exp") (("1" (rewrite "ln_exp") (("1" (rewrite "ln_exp") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ln_mult") (("2" (assert) (("2" (rewrite "ln_mult" :dir rl) (("2" (lemma "ln_bij") (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst -1 "exp(x!1 + y!1) " "exp(x!1) * exp(y!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types 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) (= 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) (>= 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) (ln const-decl "real" ln_exp nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (ln_exp formula-decl nil ln_exp nil) (ln_mult formula-decl nil ln_exp nil) (ln_bij formula-decl nil ln_exp nil) (injective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil)) nil)) (exp_diff 0 (exp_diff-1 nil 3253532189 ("" (skosimp*) (("" (transform-both 1 "ln(%1)") (("1" (hide 2) (("1" (rewrite "ln_div") (("1" (rewrite "ln_exp") (("1" (rewrite "ln_exp") (("1" (rewrite "ln_exp") nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "ln_div") (("2" (assert) (("2" (rewrite "ln_div" :dir rl) (("2" (lemma "ln_bij") (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst -1 "exp(x!1 - y!1) " "exp(x!1) / exp(y!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (= 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) (>= 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) (ln const-decl "real" ln_exp nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" 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) (ln_div formula-decl nil ln_exp nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (ln_exp formula-decl nil ln_exp nil) (ln_bij formula-decl nil ln_exp nil) (injective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil)) nil)) (exp_scal_TCC1 0 (exp_scal_TCC1-1 nil 3253532189 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)) (exp_scal 0 (exp_scal-1 nil 3253532189 ("" (skosimp*) (("" (transform-both 1 "ln(%1)") (("1" (hide 2) (("1" (rewrite "ln_expt") (("1" (rewrite "ln_exp") (("1" (rewrite "ln_exp") nil nil)) nil)) nil)) nil) ("2" (rewrite "ln_expt") (("2" (rewrite "ln_expt" :dir rl) (("2" (lemma "ln_bij") (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst -1 "exp(i!1*x!1) " "exp(x!1)^i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (posreal_exp application-judgement "posreal" exponentiation 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) (= 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) (>= 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) (ln const-decl "real" ln_exp nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (integer nonempty-type-from-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (ln_expt formula-decl nil ln_exp nil) (ln_exp formula-decl nil ln_exp nil) (bijective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (ln_bij formula-decl nil ln_exp nil)) nil)) (exp_0 0 (exp_0-1 nil 3253532189 ("" (lemma "exp_diff") (("" (inst -1 "7" "7") (("" (assert) nil nil)) nil)) 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) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (exp_diff formula-decl nil ln_exp nil)) nil)) (exp_1 0 (exp_1-1 nil 3253532189 ("" (typepred "exp(1)") (("" (expand "e") (("" (propax) nil nil)) nil)) nil) ((e const-decl "posreal" ln_exp 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) (= const-decl "[T, T -> boolean]" equalities nil) (ln const-decl "real" ln_exp nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil)) nil)) (exp_neg 0 (exp_neg-1 nil 3302427747 ("" (skosimp*) (("" (lemma "exp_diff") (("" (inst - "0" "x!1") (("" (assert) (("" (rewrite "exp_0") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((exp_diff formula-decl nil ln_exp nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (exp_0 formula-decl nil ln_exp 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)) (expt_alt_def_TCC1 0 (expt_alt_def_TCC1-1 nil 3253532189 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (expt_alt_def_TCC2 0 (expt_alt_def_TCC2-1 nil 3253532189 ("" (skosimp*) (("" (assert) nil nil)) 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)) nil)) (expt_alt_def 0 (expt_alt_def-1 nil 3253532189 ("" (skosimp*) (("" (rewrite "exp_scal") (("" (rewrite "exp_ln") nil nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (exp_scal formula-decl nil ln_exp nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (integer nonempty-type-from-decl nil integers 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) (ln const-decl "real" ln_exp nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_exp application-judgement "posreal" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (exp_ln formula-decl nil ln_exp nil)) nil)) (exp_strict_increasing 0 (exp_strict_increasing-1 nil 3253532189 ("" (expand "strict_increasing?") (("" (skosimp*) (("" (typepred "exp(x!1)") (("" (typepred "exp(y!1)") (("" (hide -1 -2 -4 -5) (("" (lemma "ln_strict_increasing") (("" (expand "strict_increasing?") (("" (inst -1 "exp(y!1)" "exp(x!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ln_strict_increasing formula-decl nil ln_exp nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (= const-decl "[T, T -> boolean]" equalities nil) (ln const-decl "real" ln_exp nil) (exp const-decl "{py | x = ln(py)}" ln_exp nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/")) nil)) (exp_increasing 0 (exp_increasing-1 nil 3253532189 ("" (lemma "exp_strict_increasing") (("" (expand "increasing?") (("" (skosimp*) (("" (expand "strict_increasing?") (("" (inst?) (("" (inst -1 "y!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((increasing? const-decl "bool" real_fun_preds "reals/") (strict_increasing? const-decl "bool" real_fun_preds "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real 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) (exp_strict_increasing formula-decl nil ln_exp nil)) nil)) (e_bnds 0 (e_bnds-1 nil 3253532189 ("" (expand "e") (("" (lemma "ln_2_bnds") (("" (flatten) (("" (mult-by -1 "2") (("" (lemma "ln_expt") (("" (inst -1 "2" "2") (("" (replace -1 * rl) (("" (hide -1) (("" (expand "^") (("" (expand "expt") (("" (expand "expt") (("" (expand "expt") (("" (typepred "exp(1)") (("" (hide -1 -2) (("" (replace -1 (-2 -3)) (("" (hide -1) (("" (lemma "exp_increasing") (("" (expand "increasing?") (("" (inst -1 "ln(exp(1))" "ln(4)") (("" (assert) (("" (rewrite "exp_ln") (("" (rewrite "exp_ln") (("" (assert) (("" (lemma "exp_increasing") (("" (expand "increasing?") (("" (inst -1 "ln(2)" "ln(exp(1))") (("" (assert) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.119 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.Bot Zugriff |
