(PVSinduction
 (Ex1 0
  (Ex1-1 nil 3310208904 3310208974
   ("" (induct "n" 1)
    (("1" (grind) nil nil)
     ("2" (skolem!) (("2" (flatten) (("2" (grind) nil nil)) nil)) nil))
    nil)
   unchecked
   ((expt def-decl "real" exponentiation nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans 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)
    (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))
   50708 4680 t shostak))
 (Ex2 0
  (Ex2-1 nil 3310225284 3310239437
   ("" (induct "i" 1)
    (("1" (grind) nil nil)
     ("2" (skolem-typepred)
      (("2" (flatten)
        (("2" (expand "^" *)
          (("2" (expand "expt" 1)
            (("2" (expand "fac" 1)
              (("2" (assert)
                (("2" (name-replace "x" "expt(2, jf!1)")
                  (("2" (name-replace "y" "fac(jf!1)")
                    (("2" (assert) (("2" (postpone) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unfinished nil 3385636 43750 t shostak)))