|
(log (log_TCC1 0
(log_TCC1-1 nil 3428807844
("" (skosimp)
(("" (case-replace "ne1x!1>1")
(("1" (case "y!1<1")
(("1" (hide 1 2 4)
(("1" (rewrite "div_mult_pos_ge1" 1)
(("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) (("2" (rewrite "div_mult_pos_le1" 5) nil 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)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(< const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil))
nil))
(log_expt_TCC1 0
(log_expt_TCC1-1 nil 3428807844 ("" (subtype-tcc) nil nil) nil
nil))
(log_expt_TCC2 0
(log_expt_TCC2-1 nil 3428807844
("" (skosimp) (("" (rewrite "real_expt_pos") nil nil)) nil)
((real_expt_pos formula-decl nil real_expt 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 "boolean" notequal nil))
nil))
(log_expt 0
(log_expt-1 nil 3428808876
("" (skosimp)
(("" (lemma "trich_lt" ("x" "z!1" "y" "0"))
(("" (split -1)
(("1" (expand "log")
(("1" (case-replace "ne1x!1>1")
(("1" (assert)
(("1"
(lemma "real_expt_lt1" ("x" "ne1x!1" "a" "z!1"))
(("1" (assert)
(("1" (rewrite "inv_real_expt" + :dir rl)
(("1" (rewrite "real_expt_neg" + :dir rl)
(("1" (expand "^")
(("1" (rewrite "nn_log_expt")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(lemma "real_expt_gt1" ("x" "ne1x!1" "a" "z!1"))
(("2" (assert)
(("2" (rewrite "inv_real_expt" + :dir rl)
(("2" (rewrite "real_expt_neg" + :dir rl)
(("2" (expand "^")
(("2" (rewrite "nn_log_expt")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (rewrite "real_expt_x0")
(("2" (expand "log")
(("2" (rewrite "nn_log_1")
(("2" (lift-if) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (expand "log")
(("3" (case-replace "ne1x!1 > 1")
(("1" (assert)
(("1"
(lemma "real_expt_gt1" ("x" "ne1x!1" "a" "z!1"))
(("1" (assert)
(("1" (expand "^")
(("1" (rewrite "nn_log_expt") nil nil)) nil))
nil))
nil))
nil)
("2" (lemma "real_expt_lt1" ("x" "ne1x!1" "a" "z!1"))
(("2" (assert)
(("2" (expand "^")
(("2" (rewrite "nn_log_expt") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(trich_lt formula-decl nil real_props nil)
(nn_log_1 formula-decl nil nn_log nil)
(real_expt_x0 formula-decl nil real_expt nil)
(log const-decl "real" log nil)
(real_expt_gt1 formula-decl nil real_expt 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)
(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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_expt_neg formula-decl nil real_expt nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nn_log_expt formula-decl nil nn_log nil)
(^ const-decl "nnreal" real_expt nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(inv_real_expt formula-decl nil real_expt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(real_expt_lt1 formula-decl nil real_expt nil)
(/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil))
shostak))
(expt_log_TCC1 0
(expt_log_TCC1-1 nil 3428807844 ("" (subtype-tcc) nil nil) nil
nil))
(expt_log 0
(expt_log-1 nil 3428809593
("" (skosimp)
(("" (case "ne1x!1>1")
(("1" (case "y!1>=1")
(("1" (expand "log")
(("1" (assert)
(("1" (expand "^")
(("1" (rewrite "nn_expt_log") nil nil)) nil))
nil))
nil)
("2" (case "y!1<1")
(("1" (hide 1)
(("1"
(lemma "real_expt_neg"
("px" "ne1x!1" "a" "-log(ne1x!1)(y!1)"))
(("1" (replace -1)
(("1" (hide -1)
(("1" (rewrite "inv_real_expt")
(("1"
(case "ne1x!1 ^ -log(ne1x!1)(y!1) = 1/y!1")
(("1" (replace -1)
(("1" (rewrite "div_div1") nil nil)) nil)
("2" (hide 2)
(("2" (expand "log")
(("2"
(assert)
(("2"
(expand "^")
(("2"
(lemma
"nn_expt_log"
("ne1x" "ne1x!1" "y" "1/y!1"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (case "ne1x!1<1")
(("1" (case "y!1<=1")
(("1" (hide 1)
(("1" (expand "log")
(("1" (assert)
(("1" (expand "^")
(("1" (rewrite "nn_expt_log") nil nil)) nil))
nil))
nil))
nil)
("2" (case "y!1>1")
(("1" (hide 1 2)
(("1"
(lemma "real_expt_neg"
("px" "ne1x!1" "a" "nn_log(ne1x!1)(1 / y!1)"))
(("1" (rewrite "inv_real_expt")
(("1" (expand "^")
(("1" (expand "log")
(("1" (assert)
(("1" (typepred "nn_log(ne1x!1)(1 / y!1)")
(("1"
(expand ">=" -1)
(("1"
(expand "<=" -1)
(("1"
(split -1)
(("1"
(assert)
(("1"
(replace -2)
(("1"
(hide -2)
(("1"
(rewrite "nn_expt_log")
(("1"
(rewrite "div_div1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1 * rl)
(("2"
(assert)
(("2"
(rewrite
"nnreal_expt_nat_rew")
(("2"
(rewrite "expt_x0")
(("2"
(hide -2)
(("2"
(expand "nn_log")
(("2"
(expand "log_lt1")
(("2"
(lemma
"nnreal_bijective2"
("lt1x" "ne1x!1"))
(("2"
(lemma
"bijective_inverse[nnreal, {r | r <= 1}]"
("f"
"LAMBDA (y:nnreal): nnreal_expt(ne1x!1, y)"
"y"
"1/y!1"
"x"
"0"))
(("1"
(assert)
(("1"
(rewrite
"nnreal_expt_nat_rew"
-1)
(("1"
(rewrite
"expt_x0")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil)
("3"
(skosimp)
(("3"
(case-replace
"y!2=0")
(("1"
(rewrite
"nnreal_expt_nat_rew"
1)
(("1"
(rewrite
"expt_x0")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(lemma
"nnreal_expt_lt1"
("x"
"ne1x!1"
"pa"
"y!2"))
(("1"
(assert)
(("1"
(rewrite
"nnreal_expt_pos"
2)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (assert)
(("2" (rewrite "div_mult_pos_le1") nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_expt_neg formula-decl nil real_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_div1 formula-decl nil real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(inv_real_expt formula-decl nil real_expt nil)
(log const-decl "real" log nil)
(^ const-decl "nnreal" real_expt nil)
(nn_expt_log formula-decl nil nn_log nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(<= const-decl "bool" reals 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(nnreal_expt_nat_rew formula-decl nil nnreal_expt nil)
(posreal_exp application-judgement "posreal" exponentiation
nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(log_lt1 const-decl "[{r | r <= 1} -> nnreal]" nn_log nil)
(bijective_inverse formula-decl nil function_inverse nil)
(bijective? const-decl "bool" functions nil)
(nnreal_expt const-decl "nnreal" nnreal_expt nil)
(nnreal_expt_pos formula-decl nil nnreal_expt nil)
(nnreal_expt_lt1 formula-decl nil nnreal_expt nil)
(nnreal_bijective2 formula-decl nil nnreal_expt nil)
(expt_x0 formula-decl nil exponentiation nil)
(minus_even_is_even application-judgement "even_int" integers
nil)
(nn_log const-decl "nnreal" nn_log nil))
shostak))
(log_1 0
(log_1-1 nil 3428809311
("" (skosimp)
(("" (expand "log")
(("" (assert)
(("" (rewrite "nn_log_1")
(("" (lift-if) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((log const-decl "real" log nil)
(nn_log_1 formula-decl nil nn_log 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 "boolean" notequal nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(log_ne1x 0
(log_ne1x-1 nil 3428824130
("" (skosimp)
(("" (expand "log")
(("" (case-replace "ne1x!1 >1")
(("1" (assert) (("1" (rewrite "nn_log_ne1x") nil nil)) nil)
("2" (assert) (("2" (rewrite "nn_log_ne1x") nil nil))
nil))
nil))
nil))
nil)
((log const-decl "real" log nil)
(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_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)
(nn_log_ne1x formula-decl nil nn_log nil)
(/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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))
(inv_base_log_TCC1 0
(inv_base_log_TCC1-1 nil 3428828063 ("" (subtype-tcc) nil nil)
nil nil))
(inv_base_log 0
(inv_base_log-1 nil 3428828064
(""
(case "FORALL (x: {r | r > 1}, y: posreal):
log(1/x)(y) = log(x)(1 / y)")
(("1" (skosimp)
(("1" (case "ne1x!1>1")
(("1" (inst - "ne1x!1" "y!1") nil nil)
("2" (inst - "1/ne1x!1" "1/y!1")
(("1" (rewrite "div_div1")
(("1" (rewrite "div_div1")
(("1" (rewrite "div_div1")
(("1" (rewrite "div_div1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (rewrite "div_mult_pos_gt1" 1) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (expand "log")
(("2" (typepred "x!1")
(("2" (rewrite "div_mult_pos_lt1" 1)
(("2" (rewrite "div_mult_pos_ge1" 1)
(("2" (case-replace "y!1=1")
(("1" (assert)
(("1" (rewrite "nn_log_1")
(("1" (rewrite "nn_log_1") nil nil)) nil))
nil)
("2" (case "y!1<1")
(("1" (assert)
(("1" (hide 1)
(("1"
(lemma "nn_inv_base_log"
("ne1x" "x!1" "y" "y!1"))
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (assert)
(("2" (case "y!1>1")
(("1" (hide 1 2)
(("1"
(lemma
"nn_inv_base_log"
("ne1x" "x!1" "y" "1/y!1"))
(("1"
(replace -1)
(("1"
(lift-if 1)
(("1"
(rewrite "div_mult_pos_gt1" 1)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite "div_mult_pos_le1" 1)
nil
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((div_mult_pos_lt1 formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nn_log_1 formula-decl nil nn_log nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_real_is_real application-judgement "real" reals nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(nn_inv_base_log formula-decl nil nn_log nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(< const-decl "bool" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(div_div1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ne1x!1 skolem-const-decl "{r | r /= 1}" log nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types 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)
(/= const-decl "boolean" notequal nil)
(log const-decl "real" log nil)
(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))
(log_inv 0
(log_inv-1 nil 3428820725
("" (skosimp)
(("" (expand "log")
(("" (case-replace "ne1x!1>1")
(("1" (lemma "trich_lt" ("x" "y!1" "y" "1"))
(("1" (split -1)
(("1" (assert)
(("1" (rewrite "div_mult_pos_ge1" 1)
(("1" (assert) nil nil)) nil))
nil)
("2" (replace -1)
(("2" (assert)
(("2" (rewrite "nn_log_1") (("2" (assert) nil nil))
nil))
nil))
nil)
("3" (assert)
(("3" (rewrite "div_mult_pos_ge1" 1)
(("3" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (assert)
(("2" (lemma "trich_lt" ("x" "y!1" "y" "1"))
(("2" (split -1)
(("1" (assert)
(("1" (rewrite "div_mult_pos_le1" 2)
(("1" (rewrite "div_div1") nil nil)) nil))
nil)
("2" (replace -1)
(("2" (assert)
(("2" (rewrite "nn_log_1")
(("2" (assert) nil nil)) nil))
nil))
nil)
("3" (assert)
(("3" (rewrite "div_mult_pos_le1" 2)
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((log const-decl "real" log nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(div_div1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(trich_lt formula-decl nil real_props nil)
(nn_log_1 formula-decl nil nn_log nil)
(minus_even_is_even application-judgement "even_int" integers
nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(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)
(posreal_times_posreal_is_posreal application-judgement
"posreal" real_types nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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))
(log_mult 0
(log_mult-1 nil 3428820389
("" (skosimp)
(("" (case "ne1x!1>1")
(("1" (case "x!1>=1")
(("1" (case "y!1>=1")
(("1"
(lemma "le_times_le_pos"
("nnx" "1" "y" "x!1" "nnz" "1" "w" "y!1"))
(("1" (expand "log")
(("1" (assert)
(("1" (rewrite "nn_log_plus") nil nil)) nil))
nil))
nil)
("2" (case "y!1<1")
(("1" (hide 1)
(("1" (case "x!1*y!1>=1")
(("1" (expand "log")
(("1" (assert)
(("1"
(lemma "nn_log_plus"
("ne1x" "ne1x!1" "x" "x!1 * y!1" "y"
"1/y!1"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (case "x!1*y!1<1")
(("1" (hide 1)
(("1" (expand "log")
(("1" (assert)
(("1"
(lemma "nn_log_plus"
("ne1x"
"ne1x!1"
"x"
"x!1"
"y"
"1 / (x!1 * y!1)"))
(("1"
(case-replace
"x!1 * (1 / (x!1 * y!1))=1/y!1")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (case "x!1<1")
(("1" (hide 1)
(("1" (case "y!1>=1")
(("1" (case "x!1 * y!1>=1")
(("1" (expand "log")
(("1" (assert)
(("1"
(lemma "nn_log_plus"
("ne1x" "ne1x!1" "x" "x!1*y!1" "y" "1/x!1"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "log")
(("2" (assert)
(("2"
(lemma "nn_log_plus"
("ne1x" "ne1x!1" "x" "y!1" "y"
"1 / (x!1 * y!1)"))
(("2"
(case-replace
"y!1 * (1 / (x!1 * y!1))=1/x!1")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "lt_times_lt_pos1"
("px" "x!1" "y" "1" "nnz" "y!1" "w" "1"))
(("2" (expand "log")
(("2" (assert)
(("2"
(lemma "nn_log_plus"
("ne1x" "ne1x!1" "x" "1/x!1" "y" "1/y!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (case "ne1x!1<1")
(("1" (hide 1)
(("1" (case "x!1<=1")
(("1" (case "y!1<=1")
(("1"
(lemma "le_times_le_pos"
("nnx" "x!1" "y" "1" "nnz" "y!1" "w" "1"))
(("1" (expand "log")
(("1" (assert)
(("1" (rewrite "nn_log_plus") nil nil)) nil))
nil))
nil)
("2" (case "y!1>1")
(("1" (hide 1)
(("1" (case "x!1 * y!1<=1")
(("1" (expand "log")
(("1" (assert)
(("1"
(lemma "nn_log_plus"
("ne1x"
"ne1x!1"
"x"
"x!1 * y!1"
"y"
"1/y!1"))
(("1"
(case-replace
"x!1 * y!1 * (1 / y!1)=x!1")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "log")
(("2" (assert)
(("2"
(lemma "nn_log_plus"
("ne1x"
"ne1x!1"
"y"
"1/(x!1*y!1)"
"x"
"x!1"))
(("2"
(case-replace
"x!1 * (1 / (x!1 * y!1))=1/y!1")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (case "x!1>1")
(("1" (hide 1)
(("1" (case "y!1<=1")
(("1" (case "x!1*y!1<=1")
(("1" (expand "log")
(("1" (assert)
(("1"
(lemma "nn_log_plus"
("ne1x"
"ne1x!1"
"x"
"x!1 * y!1"
"y"
"1/x!1"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "log")
(("2" (assert)
(("2"
(lemma "nn_log_plus"
("ne1x"
"ne1x!1"
"x"
"y!1"
"y"
"1/(x!1*y!1)"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2"
(lemma "lt_times_lt_pos1"
("px" "1" "y" "x!1" "nnz" "1" "w" "y!1"))
(("2" (expand "log")
(("2" (assert)
(("2"
(lemma "nn_log_plus"
("ne1x"
"ne1x!1"
"x"
"1/x!1"
"y"
"1/y!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
((/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(lt_times_lt_pos1 formula-decl nil real_props nil)
(log const-decl "real" log 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)
(nn_log_plus formula-decl nil nn_log 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)
(posreal_times_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_plus_real_is_real application-judgement "real" reals nil)
(le_times_le_pos formula-decl nil real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil))
shostak))
(log_div 0
(log_div-1 nil 3428826839
("" (skosimp)
(("" (lemma "log_inv" ("ne1x" "ne1x!1" "y" "y!1"))
((""
(lemma "log_mult" ("ne1x" "ne1x!1" "x" "x!1" "y" "1/y!1"))
(("" (assert) 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)
(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)
(log_inv formula-decl nil log nil)
(real_minus_real_is_real application-judgement "real" reals
nil)
(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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(log_mult formula-decl nil log nil)
(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))
(log_xz_TCC1 0
(log_xz_TCC1-1 nil 3428954667 ("" (subtype-tcc) nil nil) nil
nil))
(log_xz_TCC2 0
(log_xz_TCC2-1 nil 3428954667
("" (skosimp) (("" (rewrite "real_expt_pos") nil nil)) nil)
((real_expt_pos formula-decl nil real_expt 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))
nil))
(log_xz 0
(log_xz-1 nil 3428954668
("" (skosimp)
(("" (case-replace "x!1 ^ z!1=ne1x!1^(z!1*log(ne1x!1)(x!1))")
(("1" (rewrite "log_expt") nil nil)
("2" (hide 2)
(("2"
(lemma "real_expt_times"
("x" "ne1x!1" "a" "log(ne1x!1)(x!1)" "b" "z!1"))
(("1" (rewrite "expt_log" -1) (("1" (assert) nil nil))
nil)
("2" (rewrite "expt_log" 1) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
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)
(real_times_real_is_real application-judgement "real" reals
nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(> const-decl "bool" reals nil)
(^ const-decl "nnreal" real_expt nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil)
(log const-decl "real" log nil)
(log_expt formula-decl nil log nil)
(real_expt_times formula-decl nil real_expt nil)
(expt_log formula-decl nil log nil))
shostak))
(log_increasing_TCC1 0
(log_increasing_TCC1-1 nil 3428835559 ("" (subtype-tcc) nil nil)
nil nil))
(log_increasing 0
(log_increasing-1 nil 3428835694
("" (skosimp)
(("" (case "log(gt1x!1)(x!1) = log(gt1x!1)(y!1)")
(("1" (lemma "expt_log" ("ne1x" "gt1x!1" "y" "x!1"))
(("1" (lemma "expt_log" ("ne1x" "gt1x!1" "y" "y!1"))
(("1" (assert) nil nil)) nil))
nil)
("2"
(lemma "real_expt_increasing"
("gt1x" "gt1x!1" "a" "log(gt1x!1)(y!1)" "b"
"log(gt1x!1)(x!1)"))
(("2" (rewrite "expt_log")
(("2" (rewrite "expt_log") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((log const-decl "real" log 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(expt_log formula-decl nil log nil)
(real_expt_increasing formula-decl nil real_expt nil))
shostak))
(log_decreasing_TCC1 0
(log_decreasing_TCC1-1 nil 3428835559 ("" (subtype-tcc) nil nil)
nil nil))
(log_decreasing 0
(log_decreasing-1 nil 3428835560
("" (skosimp)
(("" (case "log(lt1x!1)(x!1) = log(lt1x!1)(y!1)")
(("1" (lemma "expt_log" ("ne1x" "lt1x!1" "y" "x!1"))
(("1" (replace -1 -3 rl)
(("1" (lemma "expt_log" ("ne1x" "lt1x!1" "y" "y!1"))
(("1" (replace -1 -4 rl)
(("1" (replace -3) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2"
(lemma "real_expt_decreasing"
("lt1x" "lt1x!1" "a" "log(lt1x!1)(x!1)" "b"
"log(lt1x!1)(y!1)"))
(("2" (rewrite "expt_log")
(("2" (rewrite "expt_log") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((< const-decl "bool" reals nil) (log const-decl "real" log 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(expt_log formula-decl nil log nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_expt_decreasing formula-decl nil real_expt nil))
shostak))
(log_is_0 0
(log_is_0-1 nil 3428837403
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (lemma "trich_lt" ("x" "y!1" "y" "1"))
(("1" (split)
(("1" (case "ne1x!1>1")
(("1"
(lemma "log_increasing"
("x" "y!1" "y" "1" "gt1x" "ne1x!1"))
(("1" (rewrite "log_1") (("1" (assert) nil nil))
nil)
("2" (propax) nil nil))
nil)
("2"
(lemma "log_decreasing"
("x" "y!1" "y" "1" "lt1x" "ne1x!1"))
(("1" (rewrite "log_1") (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (propax) nil nil)
("3" (case "ne1x!1>1")
(("1"
(lemma "log_increasing"
("y" "y!1" "x" "1" "gt1x" "ne1x!1"))
(("1" (rewrite "log_1") (("1" (assert) nil nil))
nil)
("2" (propax) nil nil))
nil)
("2"
(lemma "log_decreasing"
("y" "y!1" "x" "1" "lt1x" "ne1x!1"))
(("1" (rewrite "log_1") (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1) (("2" (rewrite "log_1") 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)
(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)
(trich_lt formula-decl nil real_props nil)
(/= const-decl "boolean" notequal nil)
(log_1 formula-decl nil log 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)
(log_increasing formula-decl nil log nil)
(log_decreasing formula-decl nil log nil)
(< const-decl "bool" reals nil))
shostak))
(log_pos 0
(log_pos-1 nil 3428837654
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (case-replace "ne1x!1>1")
(("1" (hide 2)
(("1"
(lemma "log_increasing"
("gt1x" "ne1x!1" "x" "y!1" "y" "1"))
(("1" (rewrite "log_1")
(("1" (case-replace "y!1=1")
(("1" (rewrite "log_1") (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil)
("2" (assert)
(("2" (hide 2)
(("2" (case-replace "y!1=1")
(("1" (rewrite "log_1") (("1" (assert) nil nil))
nil)
("2"
(lemma "log_decreasing"
("lt1x" "ne1x!1" "x" "1" "y" "y!1"))
(("2" (rewrite "log_1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split)
(("1" (flatten)
(("1"
(lemma "log_increasing"
("gt1x" "ne1x!1" "x" "1" "y" "y!1"))
(("1" (rewrite "log_1") (("1" (assert) nil nil)) nil)
("2" (propax) nil nil))
nil))
nil)
("2" (flatten)
(("2"
(lemma "log_decreasing"
("lt1x" "ne1x!1" "y" "1" "x" "y!1"))
(("1" (rewrite "log_1") (("1" (assert) nil nil)) nil)
("2" (propax) nil nil))
nil))
nil))
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)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal nil)
(log_increasing formula-decl nil log nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(log_1 formula-decl nil log nil)
(log_decreasing formula-decl nil log nil)
(< const-decl "bool" reals nil))
shostak))
(log_neg 0
(log_neg-1 nil 3428837916
("" (skosimp)
(("" (lemma "log_pos" ("ne1x" "ne1x!1" "y" "y!1"))
(("" (lemma "log_is_0" ("ne1x" "ne1x!1" "y" "y!1"))
(("" (lemma "trich_lt" ("x" "log(ne1x!1)(y!1)" "y" "0"))
(("" (split -1)
(("1" (assert)
(("1" (flatten)
(("1" (case-replace "ne1x!1 > 1")
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3" (assert)
(("3" (split)
(("1" (split)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (flatten) (("2" (assert) nil nil)) nil))
nil)
("2" (split)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (flatten) (("2" (assert) 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)
(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)
(log_pos formula-decl nil log nil)
(log const-decl "real" log nil)
(trich_lt formula-decl nil real_props 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)
(log_is_0 formula-decl nil log nil))
shostak))
(log_increasing1 0
(log_increasing1-1 nil 3428896910
("" (skolem + ("x!1" "y!1" "z!1"))
(("" (flatten)
(("" (case "log(x!1)(z!1) = log(y!1)(z!1)")
(("1" (hide 1)
(("1" (lemma "expt_log" ("ne1x" "x!1" "y" "z!1"))
(("1" (lemma "expt_log" ("ne1x" "y!1" "y" "z!1"))
(("1" (replace -3 -1 rl)
(("1"
(lemma "trich_lt" ("x" "log(x!1)(z!1)" "y" "0"))
(("1" (split -1)
(("1"
(lemma "real_expt_strict_decreasing"
("px" "x!1" "y" "y!1" "na" "log(x!1)(z!1)"))
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil)
("2" (assert)
(("2" (rewrite "log_is_0" -1) nil nil)) nil)
("3"
(lemma "real_expt_strict_increasing"
("x" "x!1" "y" "y!1" "pa" "log(x!1)(z!1)"))
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "log(x!1)(z!1) > log(y!1)(z!1)")
(("1" (hide 1 2)
(("1" (split)
(("1" (flatten)
(("1" (split)
(("1" (lemma "log_neg" ("ne1x" "x!1" "y" "z!1"))
(("1" (assert)
(("1"
(lemma "real_expt_strict_decreasing"
("px" "x!1" "y" "y!1" "na"
"log(x!1)(z!1)"))
(("1"
(lemma "real_expt_increasing"
("a"
"log(y!1)(z!1)"
"b"
"log(x!1)(z!1)"
"gt1x"
"y!1"))
(("1"
(rewrite "expt_log")
(("1"
(rewrite "expt_log")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "log_pos" ("ne1x" "y!1" "y" "z!1"))
(("2" (assert)
(("2"
(lemma "real_expt_strict_increasing"
("x" "x!1" "y" "y!1" "pa"
"log(y!1)(z!1)"))
(("2"
(lemma "real_expt_decreasing"
("a"
"log(y!1)(z!1)"
"b"
"log(x!1)(z!1)"
"lt1x"
"x!1"))
(("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.105 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
