SSL min_seq.prf   Sprache: Lisp

(min_seq
 (Imin_TCC1 0
  (Imin_TCC1-1 nil 3284470600 ("" (skosimp*) (("" (assert) nil)) 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))
 (Imin_TCC2 0
  (Imin_TCC2-1 nil 3284470600 ("" (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 min_seq nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs 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) (dom type-eq-decl nil min_seq nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (abv type-eq-decl nil min_seq nil)
    (subrange type-eq-decl nil integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (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))
   nil))
 (Imin_TCC3 0
  (Imin_TCC3-2 nil 3284470891
   (""
    (inst 1 "(LAMBDA ((s: ne_seqs), (ii: dom(s)), (jj:abv(ii, s))):
                      Imin[length(s),T,<=](seq(s),ii,jj))")
    (("" (skosimp*)
      (("" (typepred "Imin[length(s!1), T, <=](seq(s!1), ii!1, jj!1)")
        (("" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Imin const-decl
     "{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}"
     min_array_def nil)
    (abv type-eq-decl nil min_array_def nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (abv type-eq-decl nil min_seq nil) (< const-decl "bool" reals nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (dom type-eq-decl nil min_seq nil)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil)
  (Imin_TCC3-1 nil 3284470600
   (""
    (inst 1 "(LAMBDA ((s: seqs), (ii: dom(s)), (jj:abv(ii, s))):
                    Imin[length(s),T,<=](seq(s),ii,jj))")
    (("" (skosimp*)
      (("" (typepred "Imin[length(s!1), T, <=](seq(s!1), ii!1, jj!1)")
        (("" (inst?) (("1" (assert) nil) ("2" (assert) nil))))))))
    nil)
   nil nil))
 (Imin_seq_1_TCC1 0
  (Imin_seq_1_TCC1-1 nil 3284470600 ("" (subtype-tcc) nil nil) nil
   nil))
 (Imin_seq_1 0
  (Imin_seq_1-1 nil 3284470600
   ("" (skosimp*)
    (("" (typepred "Imin(s!1, ii!1, ii!1)")
      (("1" (inst?) (("1" (assert) nil) ("2" (assert) nil)))
       ("2" (skosimp*) (("2" (assert) nil))))))
    nil)
   ((Imin const-decl "{i: subrange(ii, jj) |
         (FORALL j: ii <= j AND j <= jj IMPLIES seq(s)(i) <= seq(s)(j))}"
     min_seq nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (abv type-eq-decl nil min_seq nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (dom type-eq-decl nil min_seq nil)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq 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)
    (<= const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (imin_TCC1 0
  (imin_TCC1-1 nil 3284470600
   ("" (inst 1 "(LAMBDA s: Imin(s,0,length(s)-1))")
    (("" (skosimp*)
      (("" (typepred "Imin(s!1, 0, length(s!1) - 1)")
        (("1" (assert)
          (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil)))))))
         ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil))))))))))
    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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (Imin const-decl "{i: subrange(ii, jj) |
         (FORALL j: ii <= j AND j <= jj IMPLIES seq(s)(i) <= seq(s)(j))}"
     min_seq nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (abv type-eq-decl nil min_seq nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil min_seq nil) (< 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)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (min_TCC1 0
  (min_TCC1-1 nil 3284470600
   ("" (inst 1 "(LAMBDA s: seq(s)(imin(s)))")
    (("" (skosimp*)
      (("" (prop)
        (("1" (skosimp*)
          (("1" (typepred "imin(s!1)") (("1" (inst?) nil)))))
         ("2" (inst?) nil))))))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (imin const-decl
     "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}"
     min_seq nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil min_seq nil) (< 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)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
 (min_seq_lem 0
  (min_seq_lem-1 nil 3284470600
   ("" (skosimp*) (("" (typepred "min(s!1)") (("" (inst?) 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 nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil min_seq nil)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq 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))
   nil))
 (min_seq_in? 0
  (min_seq_in?-1 nil 3284470600
   ("" (skosimp*)
    (("" (expand "in?")
      (("" (typepred "min(s!1)")
        (("" (skosimp*)
          (("" (hide -1) (("" (inst?) (("" (assert) nil))))))))))))
    nil)
   ((in? const-decl "bool" seqs nil)
    (below type-eq-decl nil naturalnumbers 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)
    (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)
    (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 min_seq nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (> const-decl "bool" reals nil) (ne_seqs type-eq-decl nil seqs nil)
    (dom type-eq-decl nil min_seq nil)
    (pred type-eq-decl nil defined_types nil)
    (total_order? const-decl "bool" orders nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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 nil))
   nil))
 (min_seq_def 0
  (min_seq_def-1 nil 3284470600
   ("" (skosimp*)
    (("" (prop)
      (("1" (rewrite "min_seq_lem") nil)
       ("2" (rewrite "min_seq_in?") nil))))
    nil)
   ((dom type-eq-decl nil min_seq nil) (< 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)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (min_seq_lem formula-decl nil min_seq nil)
    (min_seq_in? formula-decl nil min_seq nil))
   nil))
 (min_seq_it_is 0
  (min_seq_it_is-1 nil 3284470600
   ("" (skosimp*)
    (("" (typepred "min(s!1)")
      (("" (expand "in?")
        (("" (skosimp*)
          (("" (replace -2 * rl)
            (("" (hide -2)
              (("" (replace -3)
                (("" (hide -3)
                  (("" (inst?)
                    (("" (inst -2 "jj!1")
                      (("" (typepred "<=")
                        (("" (expand "total_order?")
                          (("" (expand "partial_order?")
                            (("" (flatten)
                              ((""
                                (expand "antisymmetric?")
                                ((""
                                  (inst?)
                                  ((""
                                    (assert)
                                    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 nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil min_seq nil)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq 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)
    (antisymmetric? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (below type-eq-decl nil naturalnumbers nil)
    (in? const-decl "bool" seqs nil))
   nil))
 (imin_seq_lem 0
  (imin_seq_lem-1 nil 3284470600
   ("" (skosimp*)
    (("" (typepred "imin(s!1)")
      (("" (typepred "min(s!1)")
        (("" (skosimp*)
          (("" (replace -2 * rl)
            (("" (hide -2)
              (("" (inst?)
                (("" (inst -3 "jj!1")
                  (("" (typepred "min_seq.<=")
                    (("" (expand "total_order?")
                      (("" (expand "partial_order?")
                        (("" (flatten)
                          (("" (expand "antisymmetric?")
                            (("" (inst?)
                              ((""
                                (assert)
                                nil))))))))))))))))))))))))))))
    nil)
   ((imin const-decl
     "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}"
     min_seq nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil min_seq 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)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (antisymmetric? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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 nil))
   nil))
 (imin_seq_1 0
  (imin_seq_1-1 nil 3284470600
   ("" (skosimp*) (("" (typepred "imin(s!1)") (("" (assert) nil))))
    nil)
   ((imin const-decl
     "{i: dom(s) | (FORALL (ii: dom(s)): seq(s)(i) <= seq(s)(ii))}"
     min_seq nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil min_seq 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)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (min_seq_2_TCC1 0
  (min_seq_2_TCC1-1 nil 3284470600 ("" (subtype-tcc) nil nil) nil nil))
 (min_seq_2_TCC2 0
  (min_seq_2_TCC2-1 nil 3284470600 ("" (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 min_seq nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (ne_seqs type-eq-decl nil seqs 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))
 (min_seq_2 0
  (min_seq_2-1 nil 3284470600
   ("" (skosimp*)
    (("" (typepred "min(s!1)")
      (("" (skosimp*)
        (("" (replace -2 * rl)
          (("" (hide -2)
            (("" (inst-cp -1 "0")
              (("" (inst -1 "1")
                (("1" (lift-if)
                  (("1" (ground)
                    (("1" (typepred "jj!1")
                      (("1" (case-replace "jj!1 = 0 OR jj!1 = 1")
                        (("1" (prop)
                          (("1" (assert) nil)
                           ("2" (replace -1)
                            (("2" (hide -1)
                              (("2"
                                (typepred "min_seq.<=")
                                (("2"
                                  (expand "total_order?")
                                  (("2"
                                    (expand "partial_order?")
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (expand "antisymmetric?")
                                        (("2"
                                          (inst?)
                                          (("2"
                                            (assert)
                                            nil)))))))))))))))))))
                         ("2" (assert) nil)))))))))
                 ("2" (assert) 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 nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= formal-const-decl "(total_order?[T])" min_seq nil)
    (total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (dom type-eq-decl nil min_seq nil)
    (ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil min_seq 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (antisymmetric? const-decl "bool" relations nil)
    (partial_order? const-decl "bool" orders nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (s!1 skolem-const-decl "ne_seqs[T]" min_seq nil))
   nil)))