(max_bounded_posnat
 (bnd_TCC1 0
  (bnd_TCC1-1 nil 3507028515
   (""
    (inst +
     "(LAMBDA (S: {A: (nonempty?[posnat]) | EXISTS x: FORALL (y: (A)): y <= x}): choose({ a |  FORALL (x: (S)): x <= a}))")
    (("" (skosimp*)
      (("" (expand "nonempty?")
        (("" (expand "empty?")
          (("" (expand "member")
            (("" (typepred "S!1")
              (("" (skosimp*) (("" (inst -3 "x!1") nil))))))))))))))
    nil)
   ((empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil) (<= const-decl "bool" reals 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))
 (max_rec_TCC1 0
  (max_rec_TCC1-1 nil 3507028515
   ("" (skosimp*) (("" (typepred "i!1") (("" (assert) nil)))) nil)
   ((<= const-decl "bool" reals nil) (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (posnat nonempty-type-eq-decl nil integers 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)
    (> 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans 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)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (max_rec_TCC2 0
  (max_rec_TCC2-1 nil 3507028515
   ("" (skosimp*) (("" (typepred "i!1") (("" (assert) nil)))) nil)
   ((<= const-decl "bool" reals nil) (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (posnat nonempty-type-eq-decl nil integers 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)
    (> 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans 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)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (max_rec_TCC3 0
  (max_rec_TCC3-1 nil 3507028515
   ("" (skosimp*) (("" (assert) nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (max_rec_in 0
  (max_rec_in-1 nil 3507028515
   ("" (induct "m")
    (("1" (skosimp*)
      (("1" (case-replace "n!1 = choose(S!1)")
        (("1" (expand "max_rec") (("1" (propax) nil)))
         ("2" (assert) nil)))))
     ("2" (skosimp*)
      (("2" (expand "max_rec" 1)
        (("2" (inst?) (("1" (assert) nil) ("2" (assert) nil)))))))
     ("3" (hide 2) (("3" (skosimp*) nil))))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (n!1 skolem-const-decl "posnat" max_bounded_posnat nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (max_rec def-decl "posnat" max_bounded_posnat nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (choose const-decl "(p)" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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)
    (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))
   nil))
 (max_rec_bnd 0
  (max_rec_bnd-1 nil 3507028515
   ("" (induct "m")
    (("1" (skosimp*)
      (("1" (expand "max_rec")
        (("1" (lift-if) (("1" (ground) nil)))))))
     ("2" (skosimp*)
      (("2" (expand "max_rec" 1)
        (("2" (lift-if)
          (("2" (ground) (("2" (inst?) (("2" (assert) nil)))))))))))
     ("3" (hide 2) (("3" (skosimp*) nil))))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (max_rec def-decl "posnat" max_bounded_posnat nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (choose const-decl "(p)" sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (max_TCC1 0
  (max_TCC1-1 nil 3507028515
   (""
    (inst +
     "(LAMBDA (S: {A: (nonempty?[posnat]) | EXISTS x: FORALL (y: (A)): y <= x}): max_rec(S,bnd(S)))")
    (("1" (skosimp*)
      (("1" (typepred "bnd(S!1)")
        (("1" (inst - "choose[posnat](S!1)")
          (("1" (lemma "max_rec_in")
            (("1" (inst?)
              (("1" (inst -1 "bnd(S!1) - choose(S!1)")
                (("1" (assert)
                  (("1" (skosimp*)
                    (("1" (lemma "max_rec_bnd")
                      (("1" (inst?)
                        (("1" (inst - "bnd(S!1) - x!1")
                          (("1" (assert)
                            (("1" (typepred "bnd(S!1)")
                              (("1"
                                (inst - "x!1")
                                (("1" (assert) nil)))))))
                           ("2" (typepred "bnd(S!1)")
                            (("2" (inst - "x!1")
                              (("2" (assert) nil)))))))))))))))
                 ("2" (assert) nil)))))))))))))
     ("2" (skosimp*)
      (("2" (typepred "bnd(S!1)")
        (("2" (inst - "choose(S!1)") (("2" (assert) nil))))))))
    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)
    (max_rec_bnd formula-decl nil max_bounded_posnat nil)
    (x!1 skolem-const-decl "posnat" max_bounded_posnat nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (S!1 skolem-const-decl
     "{A: (nonempty?[posnat]) | EXISTS x: FORALL (y: (A)): y <= x}"
     max_bounded_posnat nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (max_rec_in formula-decl nil max_bounded_posnat nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bnd const-decl "{a | FORALL (x: (S)): x <= a}" max_bounded_posnat
     nil)
    (max_rec def-decl "posnat" max_bounded_posnat nil)
    (choose const-decl "(p)" sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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))
 (max_def 0
  (max_def-1 nil 3507028515
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "maximum?")
        (("1" (assert)
          (("1" (skosimp*)
            (("1" (assert)
              (("1" (replace -1 * rl)
                (("1" (hide -1)
                  (("1" (typepred "max(S!1)")
                    (("1" (inst?) (("1" (assert) nil)))))))))))))))))
       ("2" (expand "maximum?")
        (("2" (flatten)
          (("2" (typepred "max(S!1)")
            (("2" (inst -3 "a!1")
              (("2" (inst -5 "max(S!1)")
                (("2" (assert) nil))))))))))))))
    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)
    (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)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (max const-decl
         "{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}"
         max_bounded_posnat nil)
    (maximum? const-decl "bool" max_bounded_posnat nil))
   nil))
 (max_lem 0
  (max_lem-1 nil 3507028515
   ("" (skosimp*)
    (("" (lemma "max_def") (("" (inst?) (("" (assert) nil)))))) nil)
   ((max_def formula-decl nil max_bounded_posnat nil)
    (max const-decl
         "{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}"
         max_bounded_posnat nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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))
 (max_in 0
  (max_in-1 nil 3507028515 ("" (skosimp*) (("" (assert) nil)) nil) nil
   nil)))