Quelle  ordered_finite_sequences.prf

(ordered_finite_sequences
 (extract_one_TCC1 0
  (extract_one_TCC1-1 nil 3410288297 ("" (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (^ const-decl "finseq" finite_sequences nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (extract_one_TCC2 0
  (extract_one_TCC2-1 nil 3410288297 ("" (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (extract_one 0
  (extract_one-1 nil 3410288310
   ("" (skosimp*)
    (("" (expand "^") (("" (lift-if) (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (^ const-decl "finseq" finite_sequences 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)
    (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))
   nil))
 (extract_upper_TCC1 0
  (extract_upper_TCC1-1 nil 3410109370
   ("" (expand "^")
    (("" (expand "min")
      (("" (skosimp*)
        (("" (lift-if)
          (("" (assert)
            (("" (assert) (("" (ground) (("" (postpone) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs 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)
    (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)
    (^ const-decl "finseq" finite_sequences nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (extract_upper 0
  (extract_upper-2 nil 3410111279
   ("" (skosimp*)
    (("" (expand "^")
      (("" (expand "min") (("" (lift-if) (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (^ const-decl "finseq" finite_sequences nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil)
  (extract_upper-1 nil 3410109221
   ("" (skosimp*)
    (("" (expand "^") (("" (lift-if) (("" (assert) nil nil)) nil))
      nil))
    nil)
   nil nil))
 (min_extract_TCC1 0
  (min_extract_TCC1-1 nil 3409322352
   ("" (skosimp*)
    (("" (expand "^")
      (("" (assert)
        (("" (expand "min")
          (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (^ const-decl "finseq" finite_sequences nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (sort_length formula-decl nil sort_seq "structures/")
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
 (min_extract_TCC2 0
  (min_extract_TCC2-1 nil 3409325353 ("" (subtype-tcc) nil 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (sort_length formula-decl nil sort_seq "structures/"))
   nil))
 (min_extract 0
  (min_extract-1 nil 3409322581
   ("" (skosimp*)
    (("" (typepred "min(sort(s!1) ^ (i!1, j!1))")
      (("" (skosimp*)
        (("" (replace -2 :dir RL :hide? T)
          (("" (typepred "jj!1")
            (("" (expand "^")
              (("" (lift-if)
                (("" (assert)
                  (("" (case-replace "jj!1 = 0")
                    (("1" (assert) nil nil)
                     ("2" (inst - "0")
                      (("2" (typepred "sort(s!1)")
                        (("2" (expand "increasing?")
                          (("2" (inst - "i!1" "i!1+jj!1")
                            (("2" (assert)
                              (("2"
                                (typepred "<=")
                                (("2"
                                  (expand "total_order?")
                                  (("2"
                                    (expand "partial_order?")
                                    (("2"
                                      (expand "antisymmetric?")
                                      (("2"
                                        (flatten)
                                        (("2"
                                          (inst?)
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((min const-decl "{t: T |
         (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq
         "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dom type-eq-decl nil min_seq "structures/")
    (ne_seqs type-eq-decl nil seqs "structures/")
    (> const-decl "bool" reals nil)
    (sort const-decl
          "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
      sort_seq "structures/")
    (increasing? const-decl "bool" sort_seq "structures/")
    (permutation? const-decl "bool" permutations_seq "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (seqs type-eq-decl nil sort_seq "structures/")
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (^ const-decl "finseq" finite_sequences nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs 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)
    (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)
    (sort_length formula-decl nil sort_seq "structures/")
    (antisymmetric? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   shostak))
 (max_extract_TCC1 0
  (max_extract_TCC1-1 nil 3410102768 ("" (subtype-tcc) nil 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (sort_length formula-decl nil sort_seq "structures/"))
   nil))
 (max_extract 0
  (max_extract-1 nil 3410102772
   ("" (skosimp*)
    (("" (typepred "max(sort(s!1) ^ (i!1, j!1))")
      (("" (skosimp*)
        (("" (replace -2 :dir RL :hide? T)
          (("" (typepred "jj!1")
            (("" (expand "^")
              (("" (lift-if)
                (("" (assert)
                  (("" (expand "min")
                    (("" (case-replace "jj!1 = j!1-i!1")
                      (("1" (assert) nil nil)
                       ("2" (inst - "j!1-i!1")
                        (("1" (assert)
                          (("1" (typepred "sort(s!1)")
                            (("1" (expand "increasing?")
                              (("1"
                                (inst - "i!1+jj!1" "j!1")
                                (("1"
                                  (assert)
                                  (("1"
                                    (typepred "<=")
                                    (("1"
                                      (expand "total_order?")
                                      (("1"
                                        (expand "partial_order?")
                                        (("1"
                                          (expand "antisymmetric?")
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (inst?)
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "^")
                          (("2" (assert)
                            (("2" (expand "min")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "{t: T |
         (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq
         "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dom type-eq-decl nil max_seq "structures/")
    (ne_seqs type-eq-decl nil seqs "structures/")
    (> const-decl "bool" reals nil)
    (sort const-decl
          "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
      sort_seq "structures/")
    (increasing? const-decl "bool" sort_seq "structures/")
    (permutation? const-decl "bool" permutations_seq "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (seqs type-eq-decl nil sort_seq "structures/")
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (^ const-decl "finseq" finite_sequences nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs 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)
    (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)
    (sort_length formula-decl nil sort_seq "structures/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (antisymmetric? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
    (i!1 skolem-const-decl "nat" ordered_finite_sequences nil)
    (j!1 skolem-const-decl "nat" ordered_finite_sequences nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (minmax_TCC1 0
  (minmax_TCC1-1 nil 3403444278
   ("" (skosimp*)
    (("" (expand "list2finseq")
      (("" (expand "length") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((list2finseq const-decl "finseq[T]" list2finseq nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (length def-decl "nat" list_props nil))
   nil))
 (min_le_max 0
  (min_le_max-1 nil 3403441120
   ("" (skosimp*)
    (("" (use "min_seq_in?")
      (("" (expand "in?")
        (("" (skosimp*)
          (("" (replace -1 :hide? t) (("" (use "max_seq_lem") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((min_seq_in? formula-decl nil min_seq "structures/")
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (> 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (dom type-eq-decl nil max_seq "structures/")
    (< const-decl "bool" reals 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)
    (max_seq_lem formula-decl nil max_seq "structures/")
    (in? const-decl "bool" seqs "structures/"))
   nil))
 (min_minmax 0
  (min_minmax-1 nil 3403446988
   ("" (skosimp*)
    (("" (use "min_seq_it_is")
      (("" (assert)
        (("" (hide 2)
          (("" (prop)
            (("1" (skosimp* t)
              (("1" (expand "minmax")
                (("1" (expand "list2finseq")
                  (("1" (expand "length")
                    (("1" (expand "length")
                      (("1" (expand "length")
                        (("1" (expand "nth")
                          (("1" (expand "nth")
                            (("1" (assert)
                              (("1"
                                (lift-if)
                                (("1"
                                  (prop)
                                  (("1" (use "reflexive") nil nil)
                                   ("2" (use "min_le_max") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "in?")
              (("2" (inst + 0)
                (("2" (expand "minmax")
                  (("2" (expand "list2finseq")
                    (("2" (expand "nth") (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((min_seq_it_is formula-decl nil min_seq "structures/")
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (min const-decl "{t: T |
         (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq
         "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dom type-eq-decl nil min_seq "structures/")
    (< const-decl "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (minmax const-decl "ne_seqs" ordered_finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (> 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (in? const-decl "bool" seqs "structures/")
    (below type-eq-decl nil naturalnumbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (list2finseq const-decl "finseq[T]" list2finseq nil)
    (nth def-decl "T" list_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (reflexive formula-decl nil relations_extra nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (min_le_max formula-decl nil ordered_finite_sequences nil)
    (length def-decl "nat" list_props nil))
   shostak))
 (max_minmax 0
  (max_minmax-1 nil 3403447685
   ("" (skosimp*)
    (("" (use "max_seq_it_is")
      (("" (assert)
        (("" (hide 2)
          (("" (prop)
            (("1" (skosimp* t)
              (("1" (expand "minmax")
                (("1" (expand "list2finseq")
                  (("1" (expand "length")
                    (("1" (expand "length")
                      (("1" (expand "length")
                        (("1" (expand "nth")
                          (("1" (expand "nth")
                            (("1" (assert)
                              (("1"
                                (lift-if)
                                (("1"
                                  (prop)
                                  (("1" (use "min_le_max") nil nil)
                                   ("2" (use "reflexive") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "in?")
              (("2" (inst + 1)
                (("1" (expand "minmax")
                  (("1" (expand "list2finseq")
                    (("1" (expand "nth")
                      (("1" (expand "nth") (("1" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "minmax")
                  (("2" (expand "list2finseq")
                    (("2" (expand "length")
                      (("2" (expand "length") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max_seq_it_is formula-decl nil max_seq "structures/")
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (max const-decl "{t: T |
         (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
          (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq
         "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dom type-eq-decl nil max_seq "structures/")
    (< const-decl "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (minmax const-decl "ne_seqs" ordered_finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (> 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (in? const-decl "bool" seqs "structures/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (list2finseq const-decl "finseq[T]" list2finseq nil)
    (nth def-decl "T" list_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min_le_max formula-decl nil ordered_finite_sequences nil)
    (reflexive formula-decl nil relations_extra nil)
    (reflexive? const-decl "bool" relations nil)
    (PRED type-eq-decl nil defined_types nil)
    (length def-decl "nat" list_props nil))
   shostak))
 (min_in_consensus 0
  (min_in_consensus-1 nil 3403623583
   ("" (skosimp*) (("" (use "min_seq_in?") nil nil)) nil)
   ((ne_seqs type-eq-decl nil seqs "structures/")
    (> 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (min_seq_in? formula-decl nil min_seq "structures/")
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil))
   nil))
 (max_in_consensus 0
  (max_in_consensus-1 nil 3403623583
   ("" (skosimp*) (("" (use "max_seq_in?") nil nil)) nil)
   ((ne_seqs type-eq-decl nil seqs "structures/")
    (> 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (max_seq_in? formula-decl nil max_seq "structures/")
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil))
   nil))
 (in_consensus 0
  (in_consensus-1 nil 3403441741
   ("" (skosimp* t)
    (("" (typepred "x!1(x1!1)")
      (("" (expand "in?")
        (("" (skosimp*)
          (("" (replace*)
            (("" (use "min_seq_lem")
              (("" (use "max_seq_lem") (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((in_consensus_function type-eq-decl nil finite_seqs nil)
    (in? const-decl "bool" seqs "structures/")
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (min_seq_lem formula-decl nil min_seq "structures/")
    (below type-eq-decl nil naturalnumbers nil)
    (dom type-eq-decl nil min_seq "structures/")
    (< const-decl "bool" reals 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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min_in_consensus name-judgement "in_consensus_function"
     ordered_finite_sequences nil)
    (max_in_consensus name-judgement "in_consensus_function"
     ordered_finite_sequences nil)
    (dom type-eq-decl nil max_seq "structures/")
    (max_seq_lem formula-decl nil max_seq "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/"))
   nil))
 (lower_TCC1 0
  (lower_TCC1-1 nil 3403492562 ("" (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (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)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil))
   nil))
 (lower_TCC2 0
  (lower_TCC2-1 nil 3403492562
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sort_length formula-decl nil sort_seq "structures/")
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil))
   nil))
 (lower_TCC3 0
  (lower_TCC3-1 nil 3403495511
   ("" (skosimp*)
    (("" (use "finite_below[k!1]")
      (("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil))
        nil)
       ("2" (skosimp*) (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (sort_length formula-decl nil sort_seq "structures/")
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (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)
    (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)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (i!1 skolem-const-decl "below(k!1)" ordered_finite_sequences nil)
    (k!1 skolem-const-decl "posnat" ordered_finite_sequences nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
    (sort const-decl
          "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
      sort_seq "structures/")
    (increasing? const-decl "bool" sort_seq "structures/")
    (permutation? const-decl "bool" permutations_seq "structures/")
    (seqs type-eq-decl nil sort_seq "structures/")
    (ne_seqs type-eq-decl nil seqs "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (upper_TCC1 0
  (upper_TCC1-1 nil 3403492562
   ("" (skosimp*)
    (("" (use "finite_below[k!1]")
      (("1" (skosimp*) (("1" (assert) nil nil)) nil)
       ("2" (skosimp*) (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (sort_length formula-decl nil sort_seq "structures/")
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (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)
    (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)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (k!1 skolem-const-decl "posnat" ordered_finite_sequences nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
    (i!1 skolem-const-decl "below(k!1)" ordered_finite_sequences nil)
    (sort const-decl
          "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
      sort_seq "structures/")
    (increasing? const-decl "bool" sort_seq "structures/")
    (permutation? const-decl "bool" permutations_seq "structures/")
    (seqs type-eq-decl nil sort_seq "structures/")
    (ne_seqs type-eq-decl nil seqs "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (map_set_TCC1 0
  (map_set_TCC1-1 nil 3406993589
   ("" (skosimp*)
    (("" (rewrite "finite_below")
      (("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (map_set_TCC2 0
  (map_set_TCC2-1 nil 3406994305
   ("" (skosimp*)
    (("" (rewrite "finite_below")
      (("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (map_set_TCC3 0
  (map_set_TCC3-1 nil 3407064954
   ("" (skosimp*)
    (("" (rewrite "finite_below")
      (("1" (skosimp*) (("1" (assert) nil nil)) nil)
       ("2" (skosimp*) (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (seqs type-eq-decl nil sort_seq "structures/")
    (bijective? const-decl "bool" functions nil)
    (permutation? const-decl "bool" permutations_seq "structures/")
    (increasing? const-decl "bool" sort_seq "structures/")
    (sort const-decl
          "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
      sort_seq "structures/")
    (sort_map const-decl "{map: [below(length(s)) -> below(length(s))] |
         bijective?(map) AND
          (FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}"
     sort_seq "structures/")
    (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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (map_subset_lower_TCC1 0
  (map_subset_lower_TCC1-1 nil 3407078876
   ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil)
   ((finite_below formula-decl nil finite_sets_below "finite_sets/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil))
   nil))
 (map_subset_lower 0
  (map_subset_lower-1 nil 3407078741
   ("" (skosimp*)
    (("" (expand "subset?")
      (("" (expand "member")
        (("" (expand "lower")
          (("" (expand "map_set")
            (("" (assert)
              (("" (skosimp*)
                (("" (typepred "sort_map(s!1)")
                  (("" (inst?)
                    (("" (case "sort_map(s!1)(x!1) = i!1")
                      (("1" (typepred "<=")
                        (("1" (expand "total_order?")
                          (("1" (expand "partial_order?")
                            (("1" (expand "preorder?")
                              (("1"
                                (expand "reflexive?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (inst - "s!1`seq(x!1)")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (typepred "sort(s!1)")
                        (("2" (expand "increasing?")
                          (("2" (inst - "sort_map(s!1)(x!1)" "i!1")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (lower const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sort_map const-decl "{map: [below(length(s)) -> below(length(s))] |
         bijective?(map) AND
          (FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}"
     sort_seq "structures/")
    (sort const-decl
          "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
      sort_seq "structures/")
    (increasing? const-decl "bool" sort_seq "structures/")
    (permutation? const-decl "bool" permutations_seq "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (seqs type-eq-decl nil sort_seq "structures/")
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bijective? const-decl "bool" functions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (preorder? const-decl "bool" orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (reflexive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (sort_length formula-decl nil sort_seq "structures/")
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (member const-decl "bool" sets nil))
   nil))
 (map_subset_upper_TCC1 0
  (map_subset_upper_TCC1-1 nil 3407081389
   ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil)
   ((finite_below formula-decl nil finite_sets_below "finite_sets/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil))
   nil))
 (map_subset_upper 0
  (map_subset_upper-2 nil 3407081571
   ("" (skosimp*)
    (("" (expand "subset?")
      (("" (expand "member")
        (("" (expand "upper")
          (("" (expand "map_set")
            (("" (assert)
              (("" (skosimp*)
                (("" (typepred "sort_map(s!1)")
                  (("" (inst?)
                    (("" (case "sort_map(s!1)(x!1) = i!1")
                      (("1" (typepred "<=")
                        (("1" (expand "total_order?")
                          (("1" (expand "partial_order?")
                            (("1" (expand "preorder?")
                              (("1"
                                (expand "reflexive?")
                                (("1"
                                  (flatten)
                                  (("1"
                                    (inst - "s!1`seq(x!1)")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (typepred "sort(s!1)")
                        (("2" (expand "increasing?")
                          (("2" (inst - "i!1" "sort_map(s!1)(x!1)")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subset? const-decl "bool" sets nil)
    (upper const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sort_map const-decl "{map: [below(length(s)) -> below(length(s))] |
         bijective?(map) AND
          (FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}"
     sort_seq "structures/")
    (sort const-decl
          "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
      sort_seq "structures/")
    (increasing? const-decl "bool" sort_seq "structures/")
    (permutation? const-decl "bool" permutations_seq "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (seqs type-eq-decl nil sort_seq "structures/")
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bijective? const-decl "bool" functions nil)
    (below type-eq-decl nil naturalnumbers nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (preorder? const-decl "bool" orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (reflexive? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (sort_length formula-decl nil sort_seq "structures/")
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (member const-decl "bool" sets nil))
   nil)
  (map_subset_upper-1 nil 3407081559 ("" (postpone) nil nil) nil
   shostak))
 (mapper_TCC1 0
  (mapper_TCC1-1 nil 3407078375 ("" (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (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)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (injective? const-decl "bool" functions nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (mapper_TCC2 0
  (mapper_TCC2-1 nil 3407078375 ("" (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (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)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (injective? const-decl "bool" functions nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (map_card_eq 0
  (map_card_eq-1 nil 3407078529
   ("" (skosimp*)
    (("" (use "card_eq_bij[below(k!1), below(k!1)]")
      (("" (assert)
        (("" (hide 2)
          (("" (inst + "mapper(s!1,k!1,a!1)")
            (("" (typepred "sort_map(s!1)")
              (("" (hide-all-but (-1 1))
                (("" (expand "bijective?")
                  (("" (expand "mapper")
                    (("" (ground)
                      (("1" (expand "injective?")
                        (("1" (skosimp*)
                          (("1" (inst - "x1!1" "x2!1")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (expand "surjective?")
                        (("2" (skosimp*)
                          (("2" (inst-cp - "y!1")
                            (("2" (skosimp*)
                              (("2"
                                (inst-cp + "x!1")
                                (("2"
                                  (expand "map_set")
                                  (("2"
                                    (typepred "y!1")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/")
    (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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (sort_map const-decl "{map: [below(length(s)) -> below(length(s))] |
         bijective?(map) AND
          (FORALL (i: below(length(s))): seq(s)(i) = seq(sort(s))(map(i)))}"
     sort_seq "structures/")
    (sort const-decl
          "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}"
      sort_seq "structures/")
    (increasing? const-decl "bool" sort_seq "structures/")
    (permutation? const-decl "bool" permutations_seq "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (seqs type-eq-decl nil sort_seq "structures/")
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bijective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (injective? const-decl "bool" functions nil)
    (x!1 skolem-const-decl "below(length(s!1))"
     ordered_finite_sequences nil)
    (a!1 skolem-const-decl "finite_set[below(k!1)]"
     ordered_finite_sequences nil)
    (k!1 skolem-const-decl "posnat" ordered_finite_sequences nil)
    (s!1 skolem-const-decl "ne_seqs[T]" ordered_finite_sequences nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (surjective? const-decl "bool" functions nil)
    (mapper const-decl "(a)" ordered_finite_sequences nil))
   nil))
 (card_below_set_TCC1 0
  (card_below_set_TCC1-1 nil 3406999880
   ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil)
   ((finite_below formula-decl nil finite_sets_below "finite_sets/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil))
   nil))
 (card_below_set 0
  (card_below_set-1 nil 3406999886
   ("" (induct "i")
    (("1" (skosimp*)
      (("1" (assert)
        (("1" (use "empty_card[below(k!1)]")
          (("1" (assert)
            (("1" (expand "empty?")
              (("1" (inst - "0")
                (("1" (expand "member") (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (rewrite "finite_below") nil nil))
          nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (assert)
        (("2" (inst - "k!1")
          (("2" (assert)
            (("2"
              (case "add(1+j!1,{m: below(k!1) | m <= j!1}) = {m: below(k!1) | m <= 1 + j!1}")
              (("1" (replace -1 :dir RL)
                (("1" (rewrite "card_add[below(k!1)]")
                  (("1" (assert) nil nil)
                   ("2" (rewrite "finite_below") nil nil))
                  nil))
                nil)
               ("2" (hide-all-but 1)
                (("2" (expand "add")
                  (("2" (expand "member")
                    (("2" (decompose-equality)
                      (("2" (iff) (("2" (ground) nil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skosimp*) (("3" (rewrite "finite_below") nil nil)) nil))
    nil)
   ((nonempty? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (card_add formula-decl nil finite_sets nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (empty_card formula-decl nil finite_sets nil)
    (k!1 skolem-const-decl "posnat" ordered_finite_sequences nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (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)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (pred type-eq-decl nil defined_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (<= const-decl "bool" reals nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   shostak))
 (card_above_set_TCC1 0
  (card_above_set_TCC1-1 nil 3407080645
   ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil)
   ((finite_below formula-decl nil finite_sets_below "finite_sets/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil) (<= const-decl "bool" 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil))
   nil))
 (card_above_set 0
  (card_above_set-2 nil 3407080879
   ("" (induct "i")
    (("1" (skosimp*)
      (("1" (use "card_below_fullset[k!1]")
        (("1" (expand "fullset") (("1" (assert) nil nil)) nil)) nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst - "k!1")
        (("2" (assert)
          (("2"
            (case "add(j!1,{m: below(k!1) | j!1+1<=m}) = {m: below(k!1) | j!1<=m}")
            (("1" (replace -1 :dir RL)
              (("1" (rewrite "card_add[below(k!1)]")
                (("1" (assert) nil nil)
                 ("2" (hide-all-but 1)
                  (("2" (rewrite "finite_below") nil nil)) nil))
                nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (expand "add")
                (("2" (expand "member")
                  (("2" (decompose-equality)
                    (("2" (iff) (("2" (ground) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("3" (skosimp*) (("3" (rewrite "finite_below") nil nil)) nil))
    nil)
   ((nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (member const-decl "bool" sets nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (card_add formula-decl nil finite_sets nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (add const-decl "(nonempty?)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (fullset const-decl "set" sets 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)
    (card_below_fullset formula-decl nil finite_sets_below
     "finite_sets/")
    (nat_induction formula-decl nil naturalnumbers nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (pred type-eq-decl nil defined_types 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (<= const-decl "bool" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil)
  (card_above_set-1 nil 3407080645
   ("" (induct "i")
    (("1" (skosimp*)
      (("1" (assert)
        (("1" (use "card_below_fullset[k!1]")
          (("1" (expand "fullset") (("1" (assert) nil nil)) nil)) nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst - "k!1")
        (("2" (assert) (("2" (postpone) nil nil)) nil)) nil))
      nil)
     ("3" (postpone) nil nil))
    nil)
   nil shostak))
 (card_lower 0
  (card_lower-2 nil 3407076827
   ("" (skosimp*)
    (("" (use "map_subset_lower")
      (("" (assert)
        (("" (use "card_subset[below(k!1)]")
          (("1" (assert)
            (("1" (rewrite "map_card_eq")
              (("1" (use "card_below_set") (("1" (assert) nil nil))
                nil)
               ("2" (rewrite "finite_below") nil nil))
              nil))
            nil)
           ("2" (rewrite "finite_below") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((map_subset_lower formula-decl nil ordered_finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (card_subset formula-decl nil finite_sets nil)
    (lower const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (i!1 skolem-const-decl "nat" ordered_finite_sequences nil)
    (<= const-decl "bool" reals nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (k!1 skolem-const-decl "posnat" ordered_finite_sequences nil)
    (map_card_eq formula-decl nil ordered_finite_sequences nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (card_below_set formula-decl nil ordered_finite_sequences nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   nil)
  (card_lower-1 nil 3403494320
   ("" (induct "i")
    (("1" (expand "lower")
      (("1" (skosimp*)
        (("1" (use "nonempty_card[below(k!1)]")
          (("1" (assert)
            (("1" (hide 2)
              (("1" (expand "nonempty?")
                (("1" (expand "empty?")
                  (("1" (expand "member")
                    (("1" (typepred "sort(s!1)")
                      (("1" (expand "permutation?")
                        (("1" (skosimp*)
                          (("1" (expand "bijective?")
                            (("1" (expand "surjective?")
                              (("1"
                                (flatten)
                                (("1"
                                  (inst - "0")
                                  (("1"
                                    (skosimp*)
                                    (("1"
                                      (inst?)
                                      (("1"
                                        (inst?)
                                        (("1"
                                          (replace*)
                                          (("1"
                                            (typepred "<=")
                                            (("1"
                                              (expand "total_order?")
                                              (("1"
                                                (expand
                                                 "partial_order?")
                                                (("1"
                                                  (expand "preorder?")
                                                  (("1"
                                                    (expand
                                                     "reflexive?")
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (inst?)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (rewrite "finite_below") nil nil)
           ("3" (assert) nil nil))
          nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst?)
        (("2" (assert)
          (("2" (use "lower")
            (("2" (assert)
              (("2" (rewrite "lower_increment")
                (("2" (rewrite "card_union[below(k!1)]")
                  (("1" (move-terms -1 R 2)
                    (("1" (assert)
                      (("1" (iff)
                        (("1" (assert)
                          (("1" (ground)
                            (("1" (hide -1 -3)
                              (("1"
                                (move-terms -1 R 2)
                                (("1"
                                  (assert)
                                  (("1"
                                    (use "lower_increment_alt")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (split)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (rewrite "empty_card")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (lemma
                                                     "nonempty_card[below(k!1)]")
                                                    (("1"
                                                      (hide -2)
                                                      (("1"
                                                        (inst
                                                         -
                                                         "at(s!1, 1 + j!1)")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (postpone)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2" (postpone) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (postpone) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (postpone) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (card_upper 0
  (card_upper-1 nil 3407081392
   ("" (skosimp*)
    (("" (use "map_subset_upper")
      (("" (assert)
        (("" (use "card_subset[below(k!1)]")
          (("1" (assert)
            (("1" (rewrite "map_card_eq")
              (("1" (use "card_above_set") (("1" (assert) nil nil))
                nil)
               ("2" (rewrite "finite_below") nil nil))
              nil))
            nil)
           ("2" (rewrite "finite_below") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((map_subset_upper formula-decl nil ordered_finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers 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)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (card_subset formula-decl nil finite_sets nil)
    (upper const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (map_set const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (i!1 skolem-const-decl "nat" ordered_finite_sequences nil)
    (<= const-decl "bool" reals nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (k!1 skolem-const-decl "posnat" ordered_finite_sequences nil)
    (map_card_eq formula-decl nil ordered_finite_sequences nil)
    (card_above_set formula-decl nil ordered_finite_sequences nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas 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)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (sort_overlap_TCC1 0
  (sort_overlap_TCC1-1 nil 3403483151 ("" (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil))
   nil))
 (sort_overlap_TCC2 0
  (sort_overlap_TCC2-1 nil 3403483151 ("" (subtype-tcc) nil 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= formal-const-decl "(total_order?[T])" ordered_finite_sequences
        nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (sort_length formula-decl nil sort_seq "structures/"))
   nil))
 (sort_overlap 0
  (sort_overlap-1 nil 3403483158
   ("" (skosimp*)
    (("" (lemma "pigeonhole[below(k!1)]")
      (("" (inst - "lower(s2!1, k!1, i!1)" "upper(s1!1, k!1, i!1)")
        (("" (assert)
          (("" (prop)
            (("1" (expand "lower")
              (("1" (expand "upper") (("1" (propax) nil nil)) nil))
              nil)
             ("2" (hide 2)
              (("2" (use "card_lower")
                (("2" (use "card_upper")
                  (("2" (assert)
                    (("2"
                      (invoke (then (case "%1 <= %2") (assert)) (! 1 r)
                       (! -1 l 1))
                      (("2" (hide-all-but 1)
                        (("2" (use "card_below[k!1]") nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((below type-eq-decl nil naturalnumbers 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)
    (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)
    (pigeonhole formula-decl nil pigeonhole nil)
    (finite_union application-judgement "finite_set" finite_sets nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (card_upper formula-decl nil ordered_finite_sequences nil)
    (union const-decl "set" sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (<= const-decl "bool" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (card_below formula-decl nil finite_sets_below "finite_sets/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (card_lower formula-decl nil ordered_finite_sequences nil)
    (upper const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (lower const-decl "finite_set[below(k)]" ordered_finite_sequences
     nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil))
   shostak))
 (leq_validity 0
  (leq_validity-1 nil 3408980206
   ("" (skosimp*)
    (("" (use "sort_overlap")
      (("" (assert)
        (("" (inst?) (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((sort_overlap formula-decl nil ordered_finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil ordered_finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil))
   shostak)))