products/sources/formale Sprachen/PVS/power image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Lisp

Original von: PVS©

(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" (assertnil 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) (("" (assertnil 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 nilnil 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" (assertnil 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" (assertnil 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" (assertnil nil))
                  nil)
                 ("2" (assertnil 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 nilnil
   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 nilnil
   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 nilnil
   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" (assertnil 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" (assertnil 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" (assertnil 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" (assertnil nil)) nil))
                nil))
              nil)
             ("2"
              (lemma "posreal_div_posreal_is_posreal"
               ("px" "1" "py" "x!1"))
              (("1" (assertnil nil)
               ("2" (typepred "a!1") (("2" (assertnil 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" (assertnil 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" (assertnil 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 nilnil
   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" (assertnil nil) ("2" (assertnil 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" (assertnil 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" (assertnil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (replace -1)
                    (("2" (rewrite "real_expt_x0")
                      (("2" (assertnil nil)) nil))
                    nil)
                   ("3" (inst - "x!1" "b!1" "a!1")
                    (("1" (assertnil nil) ("2" (assertnil nil))
                    nil))
                  nil))
                nil)
               ("2" (replace -1)
                (("2" (rewrite "real_expt_x0") (("2" (assertnil nil))
                  nil))
                nil)
               ("3" (inst - "x!1" "a!1" "b!1") (("3" (assertnil 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" (assertnil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (assertnil nil))
                              nil)
                             ("2" (assertnil 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" (assertnil nil))
                                nil))
                              nil)
                             ("2" (assertnil 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" (assertnil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assertnil nil))
                          nil)
                         ("2" (assertnil nil) ("3" (assertnil nil))
                        nil))
                      nil))
                    nil)
                   ("2" (replace -1)
                    (("2" (rewrite "real_expt_x0")
                      (("2" (assertnil nil)) nil))
                    nil)
                   ("3" (inst - "x!1" "a!1" "b!1")
                    (("3" (assertnil 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 nilnil
   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") (("" (assertnil 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"))
                (("" (assertnil 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" (assertnil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assertnil nil))
                        nil)
                       ("2" (replace -1 * rl)
                        (("2" (rewrite "real_expt_x0")
                          (("2" (rewrite "real_expt_1a"nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assertnil 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" (assertnil nil))
                                nil)
                               ("2"
                                (rewrite "nnreal_expt_pos" 1)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assertnil 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" (assertnil 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 nilnil nil))
 (real_expt_decreasing_TCC2 0
  (real_expt_decreasing_TCC2-1 nil 3428221695
   ("" (subtype-tcc) nil nilnil 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" (assertnil nil)) nil))
                      nil))
                    nil)
                   ("2" (replace -1)
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.83 Sekunden  (vorverarbeitet)  ¤





Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff