|
(real_expt
(caret_TCC1 0
(caret_TCC1-1 nil 3428161063 ("" (grind) 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)
(nnreal type-eq-decl nil real_types nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(/= const-decl "boolean" notequal nil))
nil))
(caret_TCC2 0
(caret_TCC2-1 nil 3428161063
("" (skosimp)
(("" (typepred "a!1")
(("" (split)
(("1" (propax) nil nil)
("2"
(lemma "posreal_div_posreal_is_posreal"
("px" "1" "py" "x!1"))
(("1" (assert) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil))
nil)
((nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(caret_TCC3 0
(caret_TCC3-1 nil 3428161063
("" (skosimp) (("" (assert) nil nil)) nil)
((minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(real_expt_nnreal_rew_TCC1 0
(real_expt_nnreal_rew_TCC1-1 nil 3428162371
("" (subtype-tcc) nil nil) nil nil))
(real_expt_nnreal_rew 0
(real_expt_nnreal_rew-1 nil 3428162007
("" (skosimp)
(("" (expand "^")
(("" (case-replace "x!1=0")
(("1" (rewrite "nnreal_expt_0a") (("1" (postpone) nil nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)) shostak))
(real_expt_int_rew_TCC1 0
(real_expt_int_rew_TCC1-1 nil 3428162371 ("" (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)
(nnreal type-eq-decl nil real_types nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal 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)
(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))
(real_expt_int_rew 0
(real_expt_int_rew-1 nil 3428162508
("" (skosimp)
(("" (typepred "i!1")
(("" (expand "^" 1 1)
(("" (split)
(("1" (expand "^")
(("1" (case-replace "i!1>=0")
(("1" (rewrite "nnreal_expt_nat_rew")
(("1" (expand "^") (("1" (assert) nil nil)) nil)) nil)
("2" (assert)
(("2" (rewrite "inv_nnreal_expt")
(("2" (rewrite "cross_mult" 2)
(("2" (assert)
(("2" (rewrite "nnreal_expt_nat_rew")
(("2" (expand "^") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "^")
(("2" (rewrite "nnreal_expt_nat_rew")
(("2" (expand "^") (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
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 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)
(/= const-decl "boolean" notequal nil)
(number nonempty-type-decl nil numbers nil)
(OR const-decl "[bool, bool -> bool]" booleans 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 application-judgement "nnreal" exponentiation nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(nnreal_expt_nat_rew formula-decl nil nnreal_expt nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(inv_nnreal_expt formula-decl nil nnreal_expt nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(cross_mult formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(nnreal_expt const-decl "nnreal" nnreal_expt nil)
(expt def-decl "real" exponentiation nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_int_is_int application-judgement "int" integers nil)
(^ const-decl "real" exponentiation nil)
(^ const-decl "nnreal" real_expt nil))
shostak))
(real_expt_root_rew_TCC1 0
(real_expt_root_rew_TCC1-1 nil 3428222991 ("" (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)
(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)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nnreal type-eq-decl nil real_types nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals 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))
(real_expt_root_rew_TCC2 0
(real_expt_root_rew_TCC2-1 nil 3428222991 ("" (subtype-tcc) nil nil)
((even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(odd? const-decl "bool" integers nil))
nil))
(real_expt_root_rew 0
(real_expt_root_rew-1 nil 3428222992
("" (skosimp)
(("" (rewrite "real_expt_nnreal_rew")
(("" (rewrite "nnreal_expt_root_rew")
(("" (expand "root")
(("" (expand "abs")
(("" (expand "sign")
(("" (case-replace "x!1=0")
(("1" (rewrite "nn_root_0n") (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_expt_nnreal_rew 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)
(nnreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(root const-decl "real" root nil)
(sign const-decl "Sign" sign "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nnreal_expt_root_rew formula-decl nil nnreal_expt nil))
shostak))
(real_expt_x0_TCC1 0
(real_expt_x0_TCC1-1 nil 3428163143 ("" (subtype-tcc) nil nil) nil
nil))
(real_expt_x0 0
(real_expt_x0-1 nil 3428163036
("" (skosimp)
(("" (expand "^")
(("" (rewrite "nnreal_expt_nat_rew")
(("" (rewrite "expt_x0") nil nil)) nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(expt_x0 formula-decl nil exponentiation nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(nnreal type-eq-decl nil real_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_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)
(nnreal_expt_nat_rew formula-decl nil nnreal_expt nil))
shostak))
(real_expt_1a 0
(real_expt_1a-1 nil 3428163181
("" (skosimp)
(("" (expand "^")
(("" (case-replace "a!1>=0")
(("1" (rewrite "nnreal_expt_1a") nil nil)
("2" (assert) (("2" (rewrite "nnreal_expt_1a") nil nil)) nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_expt_1a formula-decl nil nnreal_expt nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(real_expt_0x 0
(real_expt_0x-1 nil 3428163222
("" (skosimp)
(("" (expand "^") (("" (rewrite "nnreal_expt_0a") nil nil)) nil))
nil)
((^ const-decl "nnreal" real_expt 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_0a formula-decl nil nnreal_expt nil))
shostak))
(real_expt_x1_TCC1 0
(real_expt_x1_TCC1-1 nil 3428163292 ("" (subtype-tcc) nil nil) nil
nil))
(real_expt_x1 0
(real_expt_x1-1 nil 3428163293
("" (skosimp)
(("" (expand "^") (("" (rewrite "nnreal_expt_x1") nil nil)) nil))
nil)
((^ const-decl "nnreal" real_expt 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_x1 formula-decl nil nnreal_expt nil))
shostak))
(real_expt_pos_TCC1 0
(real_expt_pos_TCC1-1 nil 3428188411 ("" (subtype-tcc) nil nil) nil
nil))
(real_expt_pos 0
(real_expt_pos-1 nil 3428188447
("" (skosimp)
(("" (expand "^")
(("" (case-replace "a!1>=0")
(("1" (rewrite "nnreal_expt_pos") nil nil)
("2" (assert) (("2" (rewrite "nnreal_expt_pos") nil nil))
nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_expt_pos formula-decl nil nnreal_expt 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)
(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))
(real_expt_is_0 0
(real_expt_is_0-1 nil 3428188493
("" (skosimp)
(("" (expand "^")
(("" (case-replace "a!1>=0")
(("1" (rewrite "nnreal_expt_is_0")
(("1" (assert)
(("1" (case-replace "x!1=0")
(("1" (assert) (("1" (grind) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil)
("2" (assert)
(("2" (rewrite "nnreal_expt_is_0")
(("2" (typepred "a!1")
(("2" (assert)
(("2"
(lemma "posreal_div_posreal_is_posreal"
("px" "1" "py" "x!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_expt_is_0 formula-decl nil nnreal_expt nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans 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))
(real_expt_gt1 0
(real_expt_gt1-1 nil 3428188623
("" (skosimp)
(("" (expand "^")
(("" (case-replace "a!1>=0")
(("1" (assert)
(("1" (expand ">=" -1)
(("1" (expand "<=" -1)
(("1" (split -1)
(("1" (assert)
(("1" (rewrite "nnreal_expt_gt1") nil nil)) nil)
("2" (replace -1 * rl)
(("2" (assert)
(("2" (rewrite "nnreal_expt_nat_rew")
(("2" (rewrite "expt_x0")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (typepred "a!1")
(("2" (assert)
(("2"
(lemma "posreal_div_posreal_is_posreal"
("px" "1" "py" "x!1"))
(("2" (rewrite "nnreal_expt_gt1")
(("2" (assert)
(("2" (grind)
(("1" (rewrite "div_mult_pos_gt1")
(("1" (rewrite "div_mult_pos_gt1") nil nil))
nil)
("2" (rewrite "div_mult_pos_gt1" 2) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(<= const-decl "bool" reals 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_exp application-judgement "nnreal" exponentiation nil)
(expt_x0 formula-decl nil exponentiation nil)
(nnreal_expt_gt1 formula-decl nil nnreal_expt nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans 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))
(real_expt_lt1 0
(real_expt_lt1-1 nil 3428188849
("" (skosimp)
(("" (expand "^")
(("" (case-replace "a!1>=0")
(("1" (expand ">=" -1)
(("1" (expand "<=" -1)
(("1" (split -1)
(("1" (assert)
(("1" (rewrite "nnreal_expt_lt1") nil nil)) nil)
("2" (replace -1 * rl)
(("2" (assert)
(("2" (rewrite "nnreal_expt_nat_rew")
(("2" (rewrite "expt_x0") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (rewrite "nnreal_expt_lt1")
(("1" (rewrite "div_mult_pos_lt1" 2)
(("1" (grind) nil nil)
("2" (grind)
(("2" (typepred "a!1") (("2" (assert) nil nil)) nil))
nil))
nil)
("2"
(lemma "posreal_div_posreal_is_posreal"
("px" "1" "py" "x!1"))
(("1" (assert) nil nil)
("2" (typepred "a!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal_expt_lt1 formula-decl nil nnreal_expt 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)
(expt_x0 formula-decl nil exponentiation nil)
(nnreal_exp application-judgement "nnreal" 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)
(<= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans 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_real_expt_TCC1 0
(inv_real_expt_TCC1-1 nil 3428163827
("" (skosimp)
((""
(lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "px!1"))
(("" (propax) 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)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil))
nil))
(inv_real_expt_TCC2 0
(inv_real_expt_TCC2-1 nil 3428163827
("" (skosimp) (("" (rewrite "real_expt_is_0") nil nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_expt_is_0 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)
(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)
(OR const-decl "[bool, bool -> bool]" booleans nil))
nil))
(inv_real_expt 0
(inv_real_expt-1 nil 3428164437
("" (skosimp)
(("" (expand "^")
(("" (case-replace "a!1>=0")
(("1" (rewrite "inv_nnreal_expt") nil nil)
("2" (assert)
(("2" (rewrite "div_div1")
(("2" (rewrite "inv_nnreal_expt")
(("2" (rewrite "div_div1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
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)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal_expt const-decl "nnreal" nnreal_expt nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(div_div1 formula-decl nil real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(inv_nnreal_expt formula-decl nil nnreal_expt 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)
(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))
(mult_real_expt_TCC1 0
(mult_real_expt_TCC1-1 nil 3428163827
("" (skosimp)
(("" (typepred "a!1")
(("" (split)
(("1" (propax) nil nil)
("2" (flatten)
(("2" (rewrite "posreal_times_posreal_is_posreal") nil nil))
nil))
nil))
nil))
nil)
((nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(mult_real_expt_TCC2 0
(mult_real_expt_TCC2-1 nil 3428165853 ("" (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)
(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))
nil))
(mult_real_expt_TCC3 0
(mult_real_expt_TCC3-1 nil 3428165853 ("" (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)
(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))
nil))
(mult_real_expt 0
(mult_real_expt-1 nil 3428164516
("" (skosimp)
(("" (expand "^")
(("" (case-replace "a!1>=0")
(("1" (rewrite "mult_nnreal_expt") nil nil)
("2" (assert)
(("2" (typepred "a!1")
(("2" (split)
(("1" (propax) nil nil)
("2" (flatten)
(("2" (rewrite "inv_nnreal_expt")
(("1" (rewrite "inv_nnreal_expt")
(("1" (rewrite "inv_nnreal_expt")
(("1" (rewrite "mult_nnreal_expt")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (rewrite "posreal_times_posreal_is_posreal")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(inv_nnreal_expt formula-decl nil nnreal_expt nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(mult_nnreal_expt formula-decl nil nnreal_expt nil)
(nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans 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))
(div_real_expt_TCC1 0
(div_real_expt_TCC1-1 nil 3428163827 ("" (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)
(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)
(OR const-decl "[bool, bool -> bool]" 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_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil))
(div_real_expt 0
(div_real_expt-1 nil 3428164599
("" (skosimp)
(("" (lemma "inv_real_expt" ("px" "py!1" "a" "a!1"))
(("" (lemma "mult_real_expt" ("x" "x!1" "y" "1/py!1" "a" "a!1"))
(("1" (assert) nil nil)
("2" (hide -1 2)
(("2" (typepred "a!1")
(("2" (flatten)
(("2" (split)
(("1" (propax) nil nil)
("2" (assert)
(("2" (rewrite "posreal_div_posreal_is_posreal") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(inv_real_expt formula-decl nil real_expt nil)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types 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)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(mult_real_expt formula-decl nil real_expt nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
shostak))
(real_expt_neg_TCC1 0
(real_expt_neg_TCC1-1 nil 3428165433 ("" (subtype-tcc) nil nil) nil
nil))
(real_expt_neg 0
(real_expt_neg-1 nil 3428165434
("" (skosimp)
(("" (expand "^")
(("" (case-replace "a!1=0")
(("1" (assert)
(("1" (rewrite "nnreal_expt_nat_rew")
(("1" (rewrite "nnreal_expt_nat_rew")
(("1" (rewrite "expt_x0")
(("1" (rewrite "expt_x0") nil nil)) nil))
nil))
nil))
nil)
("2" (case "a!1>0")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(expt_x0 formula-decl nil exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(posreal_exp application-judgement "posreal" exponentiation nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(nnreal_expt_nat_rew formula-decl nil nnreal_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(real_expt_plus_TCC1 0
(real_expt_plus_TCC1-1 nil 3428164963 ("" (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)
(nnreal type-eq-decl nil real_types nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(real_expt_plus 0
(real_expt_plus-1 nil 3428164964
(""
(case "FORALL (x: posreal, a, b: real):
x ^ (a + b) = x ^ a * x ^ b")
(("1" (skosimp)
(("1" (case-replace "x!1=0")
(("1" (hide -2)
(("1" (typepred "a!1")
(("1" (assert)
(("1" (typepred "b!1")
(("1" (assert)
(("1" (expand "^")
(("1" (rewrite "nnreal_expt_0a")
(("1" (rewrite "nnreal_expt_0a")
(("1" (rewrite "nnreal_expt_0a")
(("1" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst - "x!1" "a!1" "b!1") (("2" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2"
(case "FORALL (x,a: posreal, b: real): x ^ (a + b) = x ^ a * x ^ b")
(("1" (skosimp)
(("1" (lemma "trich_lt" ("x" "a!1" "y" "0"))
(("1" (split -1)
(("1" (lemma "trich_lt" ("x" "b!1" "y" "0"))
(("1" (split -1)
(("1" (hide -3)
(("1" (expand "^")
(("1" (assert)
(("1"
(lemma "nnreal_expt_plus"
("x" "1/x!1" "a" "-a!1" "b" "-b!1"))
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (rewrite "real_expt_x0")
(("2" (assert) nil nil)) nil))
nil)
("3" (inst - "x!1" "b!1" "a!1")
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (rewrite "real_expt_x0") (("2" (assert) nil nil))
nil))
nil)
("3" (inst - "x!1" "a!1" "b!1") (("3" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(case "FORALL (x, a,b: posreal): x ^ (a + b) = x ^ a * x ^ b")
(("1" (skosimp)
(("1" (lemma "trich_lt" ("x" "b!1" "y" "0"))
(("1" (split -1)
(("1" (lemma "trich_lt" ("x" "a!1+b!1" "y" "0"))
(("1" (split -1)
(("1" (typepred "a!1")
(("1" (hide -1)
(("1" (inst - "x!1" "a!1" "-b!1-a!1")
(("1"
(case-replace "a!1 + (-b!1 - a!1)=-b!1")
(("1"
(hide -1)
(("1"
(rewrite "real_expt_neg" -4)
(("1"
(lemma
"real_expt_neg"
("px" "x!1" "a" "a!1+b!1"))
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(rewrite "inv_real_expt")
(("1"
(rewrite "inv_real_expt")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (rewrite "real_expt_x0")
(("2" (case-replace "b!1=-a!1")
(("1" (rewrite "real_expt_neg" +)
(("1"
(rewrite "inv_real_expt" +)
(("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("3" (inst - "x!1" "a!1+b!1" "-b!1")
(("1" (case-replace "a!1 + b!1 + -b!1=a!1")
(("1" (hide -1)
(("1" (rewrite "real_expt_neg")
(("1"
(rewrite "inv_real_expt")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (rewrite "real_expt_x0")
(("2" (assert) nil nil)) nil))
nil)
("3" (inst - "x!1" "a!1" "b!1")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (expand "^")
(("2" (rewrite "nnreal_expt_plus") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_expt_neg formula-decl nil real_expt nil)
(inv_real_expt formula-decl nil real_expt nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(a!1 skolem-const-decl "posreal" real_expt nil)
(b!1 skolem-const-decl "real" real_expt nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_expt_plus formula-decl nil nnreal_expt nil)
(- const-decl "[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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_expt_x0 formula-decl nil real_expt nil)
(b!1 skolem-const-decl "real" real_expt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(a!1 skolem-const-decl "real" real_expt nil)
(trich_lt formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(x!1 skolem-const-decl "nnreal" real_expt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_expt_0a formula-decl nil nnreal_expt nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "nnreal" real_expt nil)
(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))
shostak))
(real_expt_minus_TCC1 0
(real_expt_minus_TCC1-1 nil 3429272540 ("" (subtype-tcc) nil nil) nil
nil))
(real_expt_minus 0
(real_expt_minus-1 nil 3429272541
("" (skosimp)
(("" (lemma "real_expt_neg" ("px" "px!1" "a" "b!1"))
(("" (lemma "real_expt_plus" ("x" "px!1" "a" "a!1" "b" "-b!1"))
(("" (assert)
(("" (replace -2 -1)
(("" (replace -1 1)
(("" (rewrite "inv_real_expt") (("" (assert) 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)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_expt_neg formula-decl nil real_expt nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(inv_real_expt formula-decl nil real_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_expt_plus formula-decl nil real_expt nil)
(nnreal type-eq-decl nil real_types nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil))
shostak))
(real_expt_times_TCC1 0
(real_expt_times_TCC1-1 nil 3428164963
("" (skosimp)
(("" (typepred "a!1")
(("" (assert)
(("" (typepred "b!1")
(("" (lemma "real_expt_is_0" ("x" "x!1" "a" "a!1"))
(("" (assert)
((""
(lemma "le_times_le_pos"
("nnx" "0" "y" "a!1" "nnz" "0" "w" "b!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(^ const-decl "nnreal" real_expt nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(le_times_le_pos formula-decl nil real_props nil)
(real_expt_is_0 formula-decl nil real_expt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(real_expt_times 0
(real_expt_times-1 nil 3428189786
("" (skosimp)
(("" (case "a!1>=0")
(("1" (case "b!1>=0")
(("1" (expand "^")
(("1"
(lemma "le_times_le_pos"
("nnx" "0" "y" "a!1" "nnz" "0" "w" "b!1"))
(("1" (assert)
(("1" (rewrite "nnreal_expt_times") nil nil)) nil))
nil))
nil)
("2" (typepred "b!1")
(("2" (split -1)
(("1" (propax) nil nil)
("2" (case-replace "x!1=0")
(("1" (rewrite "real_expt_0x" -2)
(("1" (lift-if -2)
(("1" (assert)
(("1" (prop)
(("1" (replace -1)
(("1" (rewrite "real_expt_1a")
(("1" (rewrite "real_expt_0x") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "x!1>0")
(("1" (expand ">=" -3)
(("1" (expand "<=" -3)
(("1" (split -3)
(("1"
(lemma "both_sides_times_neg_lt1"
("nz" "b!1" "y" "0" "x" "a!1"))
(("1" (assert)
(("1" (expand "^")
(("1" (rewrite "inv_nnreal_expt")
(("1"
(rewrite "inv_nnreal_expt")
(("1"
(rewrite
"nnreal_expt_times"
3
:dir
rl)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (replace -1 * rl)
(("2" (rewrite "real_expt_x0")
(("2" (rewrite "real_expt_1a") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "a!1")
(("2" (assert)
(("2" (case "b!1>=0")
(("1" (expand ">=" -1)
(("1" (expand "<=" -1)
(("1" (split -1)
(("1"
(lemma "both_sides_times_pos_lt1"
("pz" "b!1" "x" "a!1" "y" "0"))
(("1" (assert)
(("1" (expand "^")
(("1" (rewrite "inv_nnreal_expt")
(("1" (rewrite "inv_nnreal_expt")
(("1" (rewrite "inv_nnreal_expt")
(("1"
(rewrite "nnreal_expt_times" 2 :dir rl)
(("1" (assert) nil nil))
nil)
("2"
(rewrite "nnreal_expt_pos" 1)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (replace -1 * rl)
(("2" (rewrite "real_expt_x0")
(("2" (rewrite "real_expt_x0") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (typepred "b!1")
(("2" (assert)
(("2" (expand "^")
(("2"
(lemma "negreal_times_negreal_is_posreal"
("nx" "a!1" "ny" "b!1"))
(("2" (assert)
(("2" (rewrite "inv_nnreal_expt")
(("2" (rewrite "div_div1")
(("2"
(lemma "nnreal_expt_times"
("x" "x!1" "a" "-a!1" "b" "-b!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnreal type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_expt_1a formula-decl nil real_expt nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_expt_0x formula-decl nil real_expt nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(inv_nnreal_expt formula-decl nil nnreal_expt nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nnreal_expt const-decl "nnreal" nnreal_expt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(both_sides_times_neg_lt1 formula-decl nil real_props nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(real_expt_x0 formula-decl nil real_expt nil)
(<= const-decl "bool" reals nil)
(real_times_real_is_real application-judgement "real" reals 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)
(nnreal_expt_times formula-decl nil nnreal_expt nil)
(le_times_le_pos formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(^ const-decl "nnreal" real_expt nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(div_div1 formula-decl nil real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(negreal_times_negreal_is_posreal judgement-tcc nil real_types nil)
(nnreal_expt_pos formula-decl nil nnreal_expt nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil))
shostak))
(real_expt_decreasing_TCC1 0
(real_expt_decreasing_TCC1-1 nil 3428221695
("" (subtype-tcc) nil nil) nil nil))
(real_expt_decreasing_TCC2 0
(real_expt_decreasing_TCC2-1 nil 3428221695
("" (subtype-tcc) nil nil) nil nil))
(real_expt_decreasing 0
(real_expt_decreasing-1 nil 3428221696
("" (skosimp)
(("" (lemma "trich_lt" ("x" "a!1" "y" "0"))
(("" (split -1)
(("1" (typepred "lt1x!1")
(("1" (case "1<1/lt1x!1")
(("1" (hide -2)
(("1" (lemma "trich_lt" ("x" "b!1" "y" "0"))
(("1" (split -1)
(("1" (expand "^")
(("1" (assert)
(("1"
(lemma "nnreal_expt_increasing"
("a" "-b!1" "b" "-a!1" "x" "1/lt1x!1"))
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (replace -1)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.38 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.
|
