SSL monotone_subsequence.prf  Interaktion und
Portierbarkeitunbekannt

(monotone_subsequence
 (minimum_prefix 0
  (minimum_prefix-1 nil 3507029426
   ("" (skolem + (_ "u!1"))
    (("" (induct "n")
      (("1" (reduce) nil nil)
       ("2" (skosimp*)
        (("2"
          (inst +
           "IF u!1(i!1) <= u!1(j!1+1) THEN i!1 ELSE j!1+1 ENDIF")
          (("2" (skosimp)
            (("2" (inst - "j!2") (("2" (smash) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    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)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (sequence type-eq-decl nil sequences nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (minimum_suffix 0
  (minimum_suffix-1 nil 3507029426
   ("" (grind :if-match nil)
    (("" (use "minimum_prefix" ("n" "n!1"))
      (("" (skolem!)
        (("" (inst + "IF u!1(i!2) <= u!1(i!1) THEN i!2 ELSE i!1 ENDIF")
          (("" (skolem!)
            (("" (inst - "j!1")
              (("" (inst - "j!1") (("" (smash) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((minimum_prefix formula-decl nil monotone_subsequence nil)
    (sequence type-eq-decl nil sequences nil)
    (<= const-decl "bool" reals nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (has_minimum const-decl "bool" monotone_subsequence nil))
   nil))
 (min_prop 0
  (min_prop-1 nil 3507029426
   ("" (skolem!)
    (("" (name-replace "m" "mini(v!1, n!1)" :hide? nil)
      (("" (expand "mini")
        (("" (use "epsilon_ax[nat]")
          (("" (replace -2)
            (("" (delete -2)
              (("" (split)
                (("1" (propax) nil nil)
                 ("2" (typepred "v!1")
                  (("2" (inst?)
                    (("2" (expand "has_minimum")
                      (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (sequence type-eq-decl nil sequences nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (mini const-decl "nat" monotone_subsequence nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil))
 (min_prop1 0
  (min_prop1-1 nil 3507029426
   ("" (skolem!) (("" (use "min_prop") (("" (flatten) nil nil)) nil))
    nil)
   ((min_prop formula-decl nil monotone_subsequence nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (sequence type-eq-decl nil sequences nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
 (min_prop2 0
  (min_prop2-1 nil 3507029426
   ("" (skosimp) (("" (use "min_prop") (("" (reduce) nil nil)) nil))
    nil)
   ((min_prop formula-decl nil monotone_subsequence nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (sequence type-eq-decl nil sequences 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (h_TCC1 0
  (h_TCC1-1 nil 3507029426 ("" (skosimp) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (h_TCC2 0
  (h_TCC2-1 nil 3507029426 ("" (skosimp) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (h_increasing 0
  (h_increasing-1 nil 3507029426
   ("" (skolem!)
    (("" (rewrite "strict_incr_condition")
      (("" (skolem!)
        (("" (expand "h" 1 2)
          (("" (use "min_prop1") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((strict_incr_condition formula-decl nil sequence_props 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)
    (sequence type-eq-decl nil sequences nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (h def-decl "nat" monotone_subsequence 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (min_prop1 formula-decl nil monotone_subsequence nil))
   nil))
 (hseq_extraction 0
  (hseq_extraction-1 nil 3507029426
   ("" (skolem!)
    (("" (expand* "hseq" "subseq")
      (("" (inst + "h(v!1)")
        (("1" (assert) nil nil) ("2" (rewrite "h_increasing") nil nil))
        nil))
      nil))
    nil)
   ((subseq const-decl "bool" sequence_props nil)
    (hseq const-decl "sequence[real]" monotone_subsequence nil)
    (h_increasing formula-decl nil monotone_subsequence nil)
    (extraction type-eq-decl nil sequence_props 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)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (sequence type-eq-decl nil sequences nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (h def-decl "nat" monotone_subsequence nil)
    (v!1 skolem-const-decl "{u | FORALL n: has_minimum(u, n)}"
     monotone_subsequence nil))
   nil))
 (hseq_increasing 0
  (hseq_increasing-1 nil 3507029426
   ("" (skolem!)
    (("" (rewrite "incr_condition")
      (("" (skolem!)
        (("" (expand "hseq")
          (("" (name-replace "k" "h(v!1)(i!1)" :hide? nil)
            (("" (expand "h" -1)
              (("" (smash)
                (("1" (use "min_prop2" ("i" "h(v!1)(1 + i!1)"))
                  (("1" (assert) nil nil)) nil)
                 ("2" (use "min_prop2" ("i" "h(v!1)(1 + i!1)"))
                  (("2" (assert)
                    (("2" (use "h_increasing")
                      (("2" (expand "strict_increasing?")
                        (("2" (inst - "i!1 - 1" "1 + i!1")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((incr_condition formula-decl nil sequence_props 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)
    (sequence type-eq-decl nil sequences nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (hseq const-decl "sequence[real]" monotone_subsequence nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (h_increasing formula-decl nil monotone_subsequence nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (min_prop2 formula-decl nil monotone_subsequence nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (h def-decl "nat" monotone_subsequence nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil))
 (no_minimum 0
  (no_minimum-1 nil 3507029426
   ("" (skolem-typepred)
    (("" (forward-chain "minimum_suffix") nil nil)) nil)
   ((minimum_suffix formula-decl nil monotone_subsequence nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (sequence type-eq-decl nil sequences nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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))
   nil))
 (pick_prop 0
  (pick_prop-1 nil 3507029426
   ("" (skolem!)
    (("" (name-replace "k" "pick(w!1, n!1)" :hide? nil)
      (("" (expand "pick")
        ((""
          (lemma "epsilon_ax"
           ("p" "LAMBDA (i : nat) : n!1 <= i AND w!1(i) < w!1(n!1)"))
          (("" (replace -2)
            (("" (assert)
              (("" (split)
                (("1" (propax) nil nil)
                 ("2" (delete -1 2)
                  (("2" (use "no_minimum" ("n" "n!1"))
                    (("2" (expand "has_minimum")
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (skosimp)
                            (("2" (inst?) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (sequence type-eq-decl nil sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (pick const-decl "nat" monotone_subsequence nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pred type-eq-decl nil defined_types nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (no_minimum formula-decl nil monotone_subsequence nil))
   nil))
 (pick_prop1 0
  (pick_prop1-1 nil 3507029426
   ("" (skolem!) (("" (use "pick_prop") (("" (ground) nil nil)) nil))
    nil)
   ((pick_prop formula-decl nil monotone_subsequence nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences 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)
    (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))
   nil))
 (pick_prop2 0
  (pick_prop2-1 nil 3507029426
   ("" (skolem!) (("" (use "pick_prop") (("" (flatten) nil nil)) nil))
    nil)
   ((pick_prop formula-decl nil monotone_subsequence nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sequence type-eq-decl nil sequences nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
 (g_TCC1 0
  (g_TCC1-1 nil 3507029426 ("" (skosimp) (("" (assert) nil nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (g_TCC2 0 (g_TCC2-1 nil 3507029426 ("" (assert) nil nil) nil nil))
 (g_increasing 0
  (g_increasing-1 nil 3507029426
   ("" (skolem!)
    (("" (rewrite "strict_incr_condition")
      (("" (skolem!)
        (("" (expand "g" 1 2) (("" (rewrite "pick_prop1") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_incr_condition formula-decl nil sequence_props 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)
    (sequence type-eq-decl nil sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (g def-decl "nat" monotone_subsequence nil)
    (pick_prop1 formula-decl nil monotone_subsequence nil))
   nil))
 (gseq_extraction 0
  (gseq_extraction-1 nil 3507029426
   ("" (skolem!)
    (("" (expand* "subseq" "gseq")
      (("" (inst + "g(w!1)")
        (("1" (assert) nil nil) ("2" (rewrite "g_increasing") nil nil))
        nil))
      nil))
    nil)
   ((gseq const-decl "sequence[real]" monotone_subsequence nil)
    (subseq const-decl "bool" sequence_props nil)
    (g_increasing formula-decl nil monotone_subsequence nil)
    (extraction type-eq-decl nil sequence_props 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)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (sequence type-eq-decl nil sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (g def-decl "nat" monotone_subsequence nil)
    (w!1 skolem-const-decl "{u | NOT has_minimum(u, 0)}"
     monotone_subsequence nil))
   nil))
 (gseq_decreasing 0
  (gseq_decreasing-1 nil 3507029426
   ("" (skolem!)
    (("" (rewrite "strict_decr_condition")
      (("" (skolem!)
        (("" (expand "gseq")
          (("" (expand "g" 1 1) (("" (rewrite "pick_prop2") nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_decr_condition formula-decl nil sequence_props 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)
    (sequence type-eq-decl nil sequences nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (gseq const-decl "sequence[real]" monotone_subsequence nil)
    (pick_prop2 formula-decl nil monotone_subsequence nil)
    (g def-decl "nat" monotone_subsequence nil))
   nil))
 (suffix_subseq 0
  (suffix_subseq-1 nil 3507029426
   ("" (grind :if-match nil)
    (("" (inst + "LAMBDA i : i+n!1")
      (("1" (assert) nil nil)
       ("2" (skosimp) (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (n!1 skolem-const-decl "nat" monotone_subsequence nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (extraction type-eq-decl nil sequence_props nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (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)
    (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)
    (subseq const-decl "bool" sequence_props nil)
    (suffix const-decl "sequence[real]" monotone_subsequence nil))
   nil))
 (suffix_hasmin 0
  (suffix_hasmin-1 nil 3507029426
   ("" (grind :if-match nil)
    (("1" (inst? +)
      (("1" (assert)
        (("1" (skosimp)
          (("1" (inst - "j!1 - n!1")
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil)
     ("2" (inst + "i!1 - n!1")
      (("2" (skosimp) (("2" (inst?) (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (n!1 skolem-const-decl "nat" monotone_subsequence nil)
    (j!1 skolem-const-decl "nat" monotone_subsequence nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (has_minimum const-decl "bool" monotone_subsequence nil)
    (suffix const-decl "sequence[real]" monotone_subsequence nil))
   nil))
 (monotone_subsequence 0
  (monotone_subsequence-1 nil 3507029426
   ("" (skosimp)
    (("" (auto-rewrite "strict_decr_to_decr[nat]" "gseq_decreasing")
      (("" (case "FORALL n : has_minimum(u!1, n)")
        (("1" (assert)
          (("1" (inst + "hseq(u!1)")
            (("1" (ground)
              (("1" (rewrite "hseq_extraction") nil nil)
               ("2" (rewrite "hseq_increasing") nil nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (rewrite "suffix_hasmin" :dir rl)
            (("2" (assert)
              (("2" (inst + "gseq(suffix(u!1, n!1))")
                (("2" (ground)
                  (("2" (use "gseq_extraction")
                    (("2" (use "suffix_subseq")
                      (("2" (forward-chain "transitive_subseq") nil
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((gseq_decreasing formula-decl nil monotone_subsequence nil)
    (strict_decr_to_decr formula-decl nil real_fun_props "reals/")
    (suffix_subseq formula-decl nil monotone_subsequence nil)
    (transitive_subseq formula-decl nil sequence_props nil)
    (gseq_extraction formula-decl nil monotone_subsequence nil)
    (suffix const-decl "sequence[real]" monotone_subsequence nil)
    (gseq const-decl "sequence[real]" monotone_subsequence nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (suffix_hasmin formula-decl nil monotone_subsequence nil)
    (hseq_extraction formula-decl nil monotone_subsequence nil)
    (hseq_increasing formula-decl nil monotone_subsequence nil)
    (hseq const-decl "sequence[real]" monotone_subsequence nil)
    (u!1 skolem-const-decl "sequence[real]" monotone_subsequence 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)
    (sequence type-eq-decl nil sequences nil)
    (has_minimum const-decl "bool" monotone_subsequence nil))
   nil)))