|
(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_824) + c!1)(1)")
(("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(x_824) + ln(py!1))(px!1)")
(("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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.91Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
