exponentiation_aux.prf

(exponentiation_aux
 (expt_lower_bound 0
  (expt_lower_bound-1 nil 3429504771
   ("" (induct "n")
    (("1" (expand "expt") (("1" (propax) nil nil)) nil)
     ("2" (skosimp*)
      (("2" (expand "expt" 1)
        (("2" (inst - "px!1")
          (("2"
            (lemma "both_sides_times_pos_le1"
             ("pz" "px!1" "x" "1" "y" "expt(1+px!1,j!1)"))
            (("2" (rewrite "expt_gt1_bound1" -1) (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (expt_gt1_bound1 formula-decl nil exponentiation nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types
     nil)
    (real_le_is_total_order name-judgement "(total_order?[real])" real_props
     nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (posreal_expt application-judgement "posreal" exponentiation nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (expt def-decl "real" exponentiation nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals 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)
    (pred type-eq-decl nil defined_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)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types
     nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types
     nil))
   shostak)))