(min_posnat
 (min_TCC1 0
  (min_TCC1-1 nil 3507028515
   (""
    (inst +
     "lambda S : choose({a : posnat | S(a) AND (FORALL (x : posnat) : S(x) IMPLIES a <= x)})")
    (("" (skosimp*)
      (("" (typepred "S!1")
        (("" (expand "nonempty?")
          (("" (expand "empty?")
            (("" (expand "member")
              (("" (skosimp*)
                (("" (lemma "wf_nat")
                  (("" (expand "well_founded?")
                    (("" (inst - "S!1")
                      (("" (split -1)
                        (("1" (assert)
                          (("1" (skosimp*)
                            (("1" (typepred "y!1")
                              (("1"
                                (expand "extend")
                                (("1"
                                  (inst -4 "y!1")
                                  (("1"
                                    (ground)
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (inst - "x!2")
                                        (("1" (assert) nil)
                                         ("2"
                                          (expand "extend")
                                          (("2" (propax) nil)))))))))
                                   ("2" (ground) nil)))))))))))
                         ("2" (inst?)
                          (("2" (assert)
                            (("2" (grind) nil))))))))))))))))))))))))))
    nil)
   ((member const-decl "bool" sets nil)
    (wf_nat formula-decl nil naturalnumbers nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (S!1 skolem-const-decl "(nonempty?[posnat])" min_posnat nil)
    (y!1 skolem-const-decl "(extend[nat, posnat, bool, FALSE](S!1))"
     min_posnat nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (x!2 skolem-const-decl "posnat" min_posnat nil)
    (nonempty_extend application-judgement "(nonempty?[T])"
     extend_set_props nil)
    (well_founded? const-decl "bool" orders nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (choose const-decl "(p)" sets nil) (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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))
   nil))
 (min_def 0
  (min_def-1 nil 3507028515
   ("" (skolem-typepred)
    (("" (typepred "min(S!1)")
      (("" (prop)
        (("1" (expand "minimum?")
          (("1" (assert)
            (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil)))))))))
         ("2" (expand "minimum?")
          (("2" (flatten)
            (("2" (inst -5 "a!1")
              (("2" (assert)
                (("2" (inst -2 "min(S!1)")
                  (("2" (assert) nil))))))))))))))))
    nil)
   ((min const-decl
         "{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
         min_posnat nil)
    (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (minimum? const-decl "bool" min_posnat nil)
    (real_le_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)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (min_lem 0
  (min_lem-1 nil 3507028515
   ("" (skosimp*)
    (("" (lemma "min_def") (("" (inst?) (("" (assert) nil)))))) nil)
   ((min_def formula-decl nil min_posnat nil)
    (min const-decl
         "{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
         min_posnat nil)
    (<= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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))
   nil)))