| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/power/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 94 kB |
|
SSL real_expt.prf
Interaktion und |
|||||||||
|
(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 --> -------------------- ¤ 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.0.28Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28