|
(nn_log
(log_gt1_TCC1 0
(log_gt1_TCC1-1 nil 3428233606
("" (skosimp)
(("" (typepred "gt1x!1")
(("" (typepred "x!1")
(("" (expand ">=" -1)
(("" (expand "<=" -1)
(("" (rewrite "nnreal_expt_pos")
(("" (split)
(("1"
(lemma "nnreal_expt_gt1" ("x" "gt1x!1" "pa" "x!1"))
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (replace -1 * rl)
(("2" (rewrite "nnreal_expt_nat_rew")
(("2" (rewrite "expt_x0") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_expt_pos formula-decl nil nnreal_expt nil)
(expt_x0 formula-decl nil exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(posreal_exp application-judgement "posreal" exponentiation 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)
(nnreal_expt_gt1 formula-decl nil nnreal_expt nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil))
nil))
(log_lt1_TCC1 0
(log_lt1_TCC1-1 nil 3428233606
("" (skosimp)
(("" (rewrite "nnreal_expt_pos")
(("" (typepred "x!1")
(("" (expand ">=")
(("" (expand "<=" -1)
(("" (split)
(("1" (lemma "nnreal_expt_lt1" ("x" "lt1x!1" "pa" "x!1"))
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (replace -1 * rl)
(("2" (rewrite "nnreal_expt_nat_rew")
(("2" (rewrite "expt_x0") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal_expt_pos formula-decl nil nnreal_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)
(nnreal type-eq-decl nil real_types 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 "bool" reals 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_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_expt_lt1 formula-decl nil nnreal_expt nil)
(nnreal_expt_nat_rew formula-decl nil nnreal_expt 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)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(posreal_exp application-judgement "posreal" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(expt_x0 formula-decl nil exponentiation nil)
(<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(nn_log_TCC1 0
(nn_log_TCC1-1 nil 3428008332 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal 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))
nil))
(nn_log_TCC2 0
(nn_log_TCC2-1 nil 3428008332 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal 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))
nil))
(nn_log_TCC3 0
(nn_log_TCC3-1 nil 3428089088 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal 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))
nil))
(nn_log_expt_TCC1 0
(nn_log_expt_TCC1-1 nil 3428087923
("" (skosimp)
(("" (lemma "nnreal_expt_pos" ("px" "ne1x!1" "a" "y!1"))
(("" (assert)
(("" (flatten)
(("" (lemma "trich_lt" ("x" "ne1x!1" "y" "1"))
(("" (split -1)
(("1" (assert)
(("1" (hide 1)
(("1" (case-replace "y!1=0")
(("1" (rewrite "nnreal_expt_rat_rew")
(("1" (rewrite "nn_rational_expt_nat_rew")
(("1" (rewrite "expt_x0")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (case "y!1>0")
(("1" (hide 1)
(("1"
(lemma "nnreal_expt_lt1"
("x" "ne1x!1" "pa" "y!1"))
(("1" (assert) nil nil)
("2" (propax) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3" (assert)
(("3" (hide 2)
(("3" (case-replace "y!1=0")
(("1" (rewrite "nnreal_expt_rat_rew")
(("1" (rewrite "nn_rational_expt_nat_rew")
(("1" (rewrite "expt_x0")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2"
(lemma "nnreal_expt_gt1"
("x" "ne1x!1" "pa" "y!1"))
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nnreal_expt_pos formula-decl nil nnreal_expt nil)
(nnreal_expt_lt1 formula-decl nil nnreal_expt nil)
(nnrat nonempty-type-eq-decl nil rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nnreal_expt_rat_rew formula-decl nil nnreal_expt nil)
(expt_x0 formula-decl nil exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(posreal_exp application-judgement "posreal" exponentiation nil)
(nn_rational_expt_nat_rew formula-decl nil nn_rational_expt nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_expt_gt1 formula-decl nil nnreal_expt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(trich_lt formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(nn_log_expt 0
(nn_log_expt-1 nil 3428088350
("" (skosimp)
(("" (expand "nn_log")
(("" (case-replace "ne1x!1>1")
(("1" (expand "log_gt1")
(("1"
(lemma "inverse_injective[nnreal, {r | r >= 1}]"
("f" "LAMBDA x: nnreal_expt(ne1x!1, x)" "x" "y!1"))
(("1" (assert) nil nil)
("2" (lemma "nnreal_bijective1" ("gt1x" "ne1x!1"))
(("1" (expand "bijective?") (("1" (flatten) nil nil))
nil)
("2" (propax) nil nil))
nil)
("3" (skosimp)
(("3" (hide 2)
(("3" (case-replace "x!1=0")
(("1" (rewrite "nnreal_expt_rat_rew")
(("1" (rewrite "nn_rational_expt_nat_rew")
(("1" (rewrite "expt_x0")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2"
(lemma "nnreal_expt_gt1" ("x" "ne1x!1" "pa" "x!1"))
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "ne1x!1<1")
(("1" (hide 1)
(("1" (expand "log_lt1")
(("1"
(lemma "inverse_injective[nnreal, {r | r <= 1}]"
("f" "LAMBDA x: nnreal_expt(ne1x!1, x)" "x" "y!1"))
(("1" (assert) nil nil)
("2" (lemma "nnreal_bijective2" ("lt1x" "ne1x!1"))
(("2" (expand "bijective?")
(("2" (flatten) nil nil)) nil))
nil)
("3" (hide 2)
(("3" (skosimp)
(("3" (case-replace "x!1=0")
(("1" (rewrite "nnreal_expt_rat_rew")
(("1" (rewrite "nn_rational_expt_nat_rew")
(("1" (rewrite "expt_x0")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2"
(lemma "nnreal_expt_lt1"
("x" "ne1x!1" "pa" "x!1"))
(("1" (assert)
(("1"
(lemma "nnreal_expt_pos"
("px" "ne1x!1" "a" "x!1"))
(("1" (propax) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((nn_log const-decl "nnreal" nn_log nil)
(<= const-decl "bool" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_bijective2 formula-decl nil nnreal_expt nil)
(nnreal_expt_lt1 formula-decl nil nnreal_expt nil)
(nnreal_expt_pos formula-decl nil nnreal_expt nil)
(log_lt1 const-decl "[{r | r <= 1} -> nnreal]" nn_log nil)
(< const-decl "bool" reals nil)
(log_gt1 const-decl "[{r | r >= 1} -> nnreal]" nn_log nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(nn_rational_expt_nat_rew formula-decl nil nn_rational_expt nil)
(posreal_exp application-judgement "posreal" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(expt_x0 formula-decl nil exponentiation nil)
(nnreal_expt_rat_rew formula-decl nil nnreal_expt nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(nnrat nonempty-type-eq-decl nil rationals nil)
(nnreal_expt_gt1 formula-decl nil nnreal_expt nil)
(nnreal_bijective1 formula-decl nil nnreal_expt nil)
(bijective? const-decl "bool" functions nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(inverse_injective formula-decl nil function_inverse nil)
(injective? const-decl "bool" functions nil)
(nnreal_expt const-decl "nnreal" nnreal_expt nil)
(nnreal type-eq-decl nil real_types 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))
(nn_expt_log 0
(nn_expt_log-1 nil 3428090185
("" (skosimp)
(("" (typepred "y!1")
(("" (expand "nn_log")
(("" (split)
(("1" (flatten)
(("1" (assert)
(("1" (expand "log_gt1")
(("1" (lemma "nnreal_bijective1" ("gt1x" "ne1x!1"))
(("1" (expand "bijective?")
(("1" (flatten)
(("1"
(lemma
"inverse_surjective[nnreal, {r | r >= 1}]"
("f" "LAMBDA x: nnreal_expt(ne1x!1, x)" "y"
"y!1"))
(("1" (assert) nil nil) ("2" (propax) nil nil)
("3" (skosimp)
(("3" (hide 2 -1 -2)
(("3" (rewrite "nnreal_expt_pos")
(("3"
(case-replace "x!1=0")
(("1"
(rewrite "nnreal_expt_rat_rew")
(("1"
(rewrite
"nn_rational_expt_nat_rew")
(("1"
(rewrite "expt_x0")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma
"nnreal_expt_gt1"
("x" "ne1x!1" "pa" "x!1"))
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (assert)
(("2" (expand "log_lt1")
(("2" (lemma "nnreal_bijective2" ("lt1x" "ne1x!1"))
(("2" (expand "bijective?")
(("2" (flatten)
(("2"
(lemma
"inverse_surjective[nnreal, {r | r <= 1}]"
("f" "LAMBDA x: nnreal_expt(ne1x!1, x)" "y"
"y!1"))
(("1" (assert) nil nil) ("2" (propax) nil nil)
("3" (skosimp)
(("3" (hide -1 -2 2)
(("3" (case-replace "x!1=0")
(("1"
(rewrite "nnreal_expt_rat_rew")
(("1"
(rewrite "nn_rational_expt_nat_rew")
(("1"
(rewrite "expt_x0")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma
"nnreal_expt_pos"
("px" "ne1x!1" "a" "x!1"))
(("2"
(lemma
"nnreal_expt_lt1"
("x" "ne1x!1" "pa" "x!1"))
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(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)
(nnreal_bijective1 formula-decl nil nnreal_expt nil)
(nnreal_expt_pos formula-decl nil nnreal_expt nil)
(nnreal_expt_gt1 formula-decl nil nnreal_expt nil)
(nnrat nonempty-type-eq-decl nil rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nnreal_expt_rat_rew formula-decl nil nnreal_expt nil)
(expt_x0 formula-decl nil exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(posreal_exp application-judgement "posreal" exponentiation nil)
(nn_rational_expt_nat_rew formula-decl nil nn_rational_expt nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nnreal_expt const-decl "nnreal" nnreal_expt nil)
(surjective? const-decl "bool" functions nil)
(inverse_surjective formula-decl nil function_inverse nil)
(bijective? const-decl "bool" functions nil)
(log_gt1 const-decl "[{r | r >= 1} -> nnreal]" nn_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)
(nnreal_bijective2 formula-decl nil nnreal_expt nil)
(nnreal_expt_lt1 formula-decl nil nnreal_expt nil)
(log_lt1 const-decl "[{r | r <= 1} -> nnreal]" nn_log nil)
(nn_log const-decl "nnreal" nn_log nil))
shostak))
(nn_log_plus_TCC1 0
(nn_log_plus_TCC1-1 nil 3428099141
("" (subtype-tcc)
(("1"
(lemma "le_times_le_pos"
("nnx" "1" "y" "x!1" "nnz" "1" "w" "y!1"))
(("1" (assert) nil nil)) nil)
("2"
(lemma "le_times_le_pos"
("nnx" "x!1" "y" "1" "nnz" "y!1" "w" "1"))
(("2" (assert) nil nil)) nil))
nil)
((le_times_le_pos formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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_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)
(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 "boolean" notequal 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))
nil))
(nn_log_plus 0
(nn_log_plus-1 nil 3428099141
("" (skosimp)
((""
(lemma "trich_lt"
("x" "nn_log(ne1x!1)(x!1 * y!1)" "y"
"nn_log(ne1x!1)(x!1) + nn_log(ne1x!1)(y!1)"))
(("" (split)
(("1" (case "ne1x!1>1")
(("1"
(lemma "nnreal_expt_increasing"
("x" "ne1x!1" "b"
"nn_log(ne1x!1)(x!1) + nn_log(ne1x!1)(y!1)" "a"
"nn_log(ne1x!1)(x!1 * y!1)"))
(("1" (assert)
(("1" (rewrite "nnreal_expt_plus")
(("1" (rewrite "nn_expt_log")
(("1" (rewrite "nn_expt_log")
(("1" (rewrite "nn_expt_log")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "nnreal_expt_decreasing"
("x" "ne1x!1" "b"
"nn_log(ne1x!1)(x!1) + nn_log(ne1x!1)(y!1)" "a"
"nn_log(ne1x!1)(x!1 * y!1)"))
(("2" (assert)
(("2" (rewrite "nnreal_expt_plus")
(("2" (rewrite "nn_expt_log")
(("2" (rewrite "nn_expt_log")
(("2" (rewrite "nn_expt_log")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (typepred "ne1x!1")
(("3" (case "ne1x!1>1")
(("1"
(lemma "nnreal_expt_increasing"
("x" "ne1x!1" "a"
"nn_log(ne1x!1)(x!1) + nn_log(ne1x!1)(y!1)" "b"
"nn_log(ne1x!1)(x!1 * y!1)"))
(("1" (assert)
(("1" (rewrite "nn_expt_log")
(("1" (rewrite "nnreal_expt_plus")
(("1" (rewrite "nn_expt_log")
(("1" (rewrite "nn_expt_log")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "ne1x!1<1")
(("1" (hide 1)
(("1"
(lemma "nnreal_expt_decreasing"
("x" "ne1x!1" "a"
"nn_log(ne1x!1)(x!1) + nn_log(ne1x!1)(y!1)" "b"
"nn_log(ne1x!1)(x!1 * y!1)"))
(("1" (assert)
(("1" (rewrite "nn_expt_log")
(("1" (rewrite "nnreal_expt_plus")
(("1" (rewrite "nn_expt_log")
(("1" (rewrite "nn_expt_log")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nn_log const-decl "nnreal" nn_log nil)
(nnreal type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(trich_lt formula-decl nil real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(nn_expt_log formula-decl nil nn_log nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_expt_plus formula-decl nil nnreal_expt nil)
(nnreal_expt_increasing formula-decl nil nnreal_expt nil)
(nnreal_expt_decreasing formula-decl nil nnreal_expt nil))
shostak))
(nn_log_1_TCC1 0
(nn_log_1_TCC1-1 nil 3428235471 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(nn_log_1 0
(nn_log_1-1 nil 3428235472
("" (skosimp)
(("" (lemma "nn_log_expt" ("ne1x" "ne1x!1" "y" "0"))
(("" (rewrite "nnreal_expt_nat_rew")
(("" (rewrite "expt_x0") nil nil)) nil))
nil))
nil)
((nnreal type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nn_log_expt formula-decl nil nn_log nil)
(expt_x0 formula-decl nil exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(posreal_exp application-judgement "posreal" exponentiation 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))
shostak))
(nn_log_ne1x_TCC1 0
(nn_log_ne1x_TCC1-1 nil 3428235731 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(nn_log_ne1x 0
(nn_log_ne1x-1 nil 3428235732
("" (skosimp)
(("" (lemma "nn_log_expt" ("ne1x" "ne1x!1" "y" "1"))
(("" (rewrite "nnreal_expt_x1") nil nil)) nil))
nil)
((nnreal type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nn_log_expt formula-decl nil nn_log nil)
(nnreal_expt_x1 formula-decl nil nnreal_expt nil))
shostak))
(nn_log_gt1_TCC1 0
(nn_log_gt1_TCC1-1 nil 3428097916 ("" (subtype-tcc) nil nil) nil
nil))
(nn_log_gt1_TCC2 0
(nn_log_gt1_TCC2-1 nil 3428097916 ("" (subtype-tcc) nil nil) nil
nil))
(nn_log_gt1 0
(nn_log_gt1-1 nil 3428097917
("" (skosimp)
(("" (lemma "nn_log_ne1x" ("ne1x" "gt1x!1"))
(("" (replace -1 * rl)
(("" (hide -1)
(("" (split)
(("1" (flatten)
(("1"
(lemma "nnreal_expt_increasing"
("a" "nn_log(gt1x!1)(gt1x!1)" "b"
"nn_log(gt1x!1)(gt1y!1)" "x" "gt1x!1"))
(("1" (assert)
(("1" (rewrite "nn_expt_log")
(("1" (rewrite "nn_expt_log")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2"
(case-replace
"nn_log(gt1x!1)(gt1y!1)=nn_log(gt1x!1)(gt1x!1)")
(("1" (rewrite "nn_log_ne1x")
(("1" (hide 1)
(("1" (expand "nn_log")
(("1" (expand "log_gt1")
(("1"
(lemma "nnreal_bijective1" ("gt1x" "gt1x!1"))
(("1"
(lemma
"bijective_inverse[nnreal, {r | r >= 1}]"
("f"
"LAMBDA (y:nnreal): nnreal_expt(gt1x!1, y)"
"y" "gt1y!1" "x" "1"))
(("1" (replace -1)
(("1"
(assert)
(("1"
(rewrite "nnreal_expt_x1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (skosimp)
(("3"
(case-replace "y!1=0")
(("1"
(rewrite "nnreal_expt_nat_rew" 1)
(("1"
(rewrite "expt_x0")
(("1" (assert) nil nil))
nil))
nil)
("2"
(lemma
"nnreal_expt_gt1"
("x" "gt1x!1" "pa" "y!1"))
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "nnreal_expt_increasing"
("a" "nn_log(gt1x!1)(gt1y!1)" "b"
"nn_log(gt1x!1)(gt1x!1)" "x" "gt1x!1"))
(("2" (rewrite "nn_expt_log")
(("2" (rewrite "nn_expt_log")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(nn_log_ne1x formula-decl nil nn_log nil)
(nnreal_bijective1 formula-decl nil nnreal_expt nil)
(nnreal_expt_gt1 formula-decl nil nnreal_expt 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)
(expt_x0 formula-decl nil exponentiation nil)
(nnreal_expt_x1 formula-decl nil nnreal_expt nil)
(nnreal_expt const-decl "nnreal" nnreal_expt nil)
(bijective? const-decl "bool" functions nil)
(bijective_inverse formula-decl nil function_inverse nil)
(log_gt1 const-decl "[{r | r >= 1} -> nnreal]" nn_log nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(nn_expt_log formula-decl nil nn_log nil)
(nnreal_expt_increasing formula-decl nil nnreal_expt nil)
(nnreal type-eq-decl nil real_types 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)
(nn_log const-decl "nnreal" nn_log nil))
shostak))
(nn_inv_base_log_TCC1 0
(nn_inv_base_log_TCC1-1 nil 3428829410
("" (skosimp)
(("" (typepred "y!1")
(("" (split)
(("1" (flatten)
(("1" (assert) (("1" (rewrite "div_mult_pos_lt1" 2) nil nil))
nil))
nil)
("2" (flatten)
(("2" (assert) (("2" (rewrite "div_mult_pos_gt1" 1) nil nil))
nil))
nil))
nil))
nil))
nil)
((< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(nn_inv_base_log_TCC2 0
(nn_inv_base_log_TCC2-1 nil 3428829410 ("" (subtype-tcc) nil nil) nil
nil))
(nn_inv_base_log_TCC3 0
(nn_inv_base_log_TCC3-1 nil 3428829410
("" (skosimp)
(("" (typepred "y!1")
(("" (split)
(("1" (flatten)
(("1" (assert) (("1" (rewrite "div_mult_pos_ge1" 1) nil nil))
nil))
nil)
("2" (flatten)
(("2" (assert) (("2" (rewrite "div_mult_pos_le1" 2) nil nil))
nil))
nil))
nil))
nil))
nil)
((< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(div_mult_pos_le1 formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_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))
nil))
(nn_inv_base_log 0
(nn_inv_base_log-1 nil 3428829411
("" (skosimp)
((""
(lemma "trich_lt"
("x" "nn_log(1 / ne1x!1)(y!1)" "y" "nn_log(ne1x!1)(1 / y!1)"))
(("" (split -1)
(("1" (hide 1)
(("1" (typepred "y!1")
(("1" (split)
(("1" (flatten)
(("1"
(lemma "nnreal_expt_increasing"
("x" "ne1x!1" "a" "nn_log(1 / ne1x!1)(y!1)" "b"
"nn_log(ne1x!1)(1 / y!1)"))
(("1" (assert)
(("1" (rewrite "nn_expt_log" -1)
(("1"
(lemma "inv_nnreal_expt"
("px" "ne1x!1" "a" "nn_log(1 / ne1x!1)(y!1)"))
(("1" (rewrite "nn_expt_log" -1)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2"
(lemma "nnreal_expt_decreasing"
("a" "nn_log(1 / ne1x!1)(y!1)" "b"
"nn_log(ne1x!1)(1 / y!1)" "x" "ne1x!1"))
(("2" (assert)
(("2" (rewrite "nn_expt_log")
(("2"
(lemma "inv_nnreal_expt"
("px" "1/ne1x!1" "a"
"nn_log(1 / ne1x!1)(y!1)"))
(("2" (rewrite "nn_expt_log")
(("2"
(case-replace "1 / (1 / ne1x!1)=ne1x!1")
(("1" (assert)
(("1"
(replace -2 -3)
(("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (case "ne1x!1>1")
(("1"
(lemma "nnreal_expt_increasing"
("a" "nn_log(ne1x!1)(1 / y!1)" "b"
"nn_log(1 / ne1x!1)(y!1)" "x" "ne1x!1"))
(("1" (rewrite "nn_expt_log")
(("1" (assert)
(("1"
(lemma "inv_nnreal_expt"
("px" "ne1x!1" "a" "nn_log(1 / ne1x!1)(y!1)"))
(("1" (rewrite "nn_expt_log" -1)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (case "ne1x!1<1")
(("1" (hide 1)
(("1"
(lemma "nnreal_expt_decreasing"
("a" "nn_log(ne1x!1)(1 / y!1)" "b"
"nn_log(1 / ne1x!1)(y!1)" "x" "ne1x!1"))
(("1" (rewrite "nn_expt_log" -1)
(("1" (assert)
(("1"
(lemma "inv_nnreal_expt"
("px" "ne1x!1" "a" "nn_log(1 / ne1x!1)(y!1)"))
(("1" (rewrite "nn_expt_log")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nn_log const-decl "nnreal" nn_log nil)
(nnreal type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(trich_lt formula-decl nil real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_expt_increasing formula-decl nil nnreal_expt nil)
(nn_expt_log formula-decl nil nn_log nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(inv_nnreal_expt formula-decl nil nnreal_expt nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_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)
(nnreal_expt_decreasing formula-decl nil nnreal_expt nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(nn_log_increasing_TCC1 0
(nn_log_increasing_TCC1-1 nil 3428236182 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnreal 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(nn_log_increasing_TCC2 0
(nn_log_increasing_TCC2-1 nil 3428236182 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nnreal 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(nn_log_increasing 0
(nn_log_increasing-1 nil 3428814899
("" (skosimp)
(("" (case-replace "nn_log(gt1x!1)(y!1)=nn_log(gt1x!1)(x!1)")
(("1" (hide 1)
(("1" (lemma "nn_expt_log" ("ne1x" "gt1x!1" "y" "y!1"))
(("1" (lemma "nn_expt_log" ("ne1x" "gt1x!1" "y" "x!1"))
(("1" (replace -1 -5 rl)
(("1" (replace -2 -5 rl)
(("1" (hide -1 -2)
(("1" (replace -1) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "nnreal_expt_increasing"
("a" "nn_log(gt1x!1)(y!1)" "b" "nn_log(gt1x!1)(x!1)" "x"
"gt1x!1"))
(("2" (assert)
(("2" (rewrite "nn_expt_log")
(("2" (rewrite "nn_expt_log") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(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)
(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)
(nnreal type-eq-decl nil real_types nil)
(nn_log const-decl "nnreal" nn_log nil)
(nn_expt_log formula-decl nil nn_log nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_expt_increasing formula-decl nil nnreal_expt nil))
shostak)))
¤ Dauer der Verarbeitung: 0.51 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.
|
