SSL minmax_ineq.prf

(minmax_ineq
 (min_le 0
  (min_le-1 nil 3276016566 ("" (grind) 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)
    (real_gt_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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (min_lt 0
  (min_lt-1 nil 3276016566 ("" (grind) 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)
    (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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (min_ge 0
  (min_ge-1 nil 3276016566 ("" (grind) 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)
    (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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (min_gt 0
  (min_gt-1 nil 3276016566 ("" (grind) 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (le_min 0
  (le_min-1 nil 3276016566 ("" (grind) 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)
    (real_gt_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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (lt_min 0
  (lt_min-1 nil 3276016566 ("" (grind) 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)
    (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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (ge_min 0
  (ge_min-1 nil 3276016566 ("" (grind) 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)
    (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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (gt_min 0
  (gt_min-1 nil 3276016566 ("" (grind) 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   nil))
 (max_le 0
  (max_le-1 nil 3276016566
   ("" (skosimp*)
    (("" (expand "max")
      (("" (case "a!1 < b!1")
        (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil))
 (max_lt 0
  (max_lt-1 nil 3276016566
   ("" (skosimp*)
    (("" (expand "max")
      (("" (case "a!1 < b!1")
        (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil))
 (max_ge 0
  (max_ge-1 nil 3276016566
   ("" (skosimp*)
    (("" (expand "max")
      (("" (case "a!1 < b!1")
        (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_ge_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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil))
 (max_gt 0
  (max_gt-1 nil 3276016566
   ("" (skosimp*)
    (("" (expand "max")
      (("" (case "a!1 < b!1")
        (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil))
 (le_max 0
  (le_max-1 nil 3276016566
   ("" (skosimp*)
    (("" (expand "max")
      (("" (case "b!1 < c!1")
        (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil))
 (lt_max 0
  (lt_max-1 nil 3276016566
   ("" (skosimp*)
    (("" (expand "max")
      (("" (case "b!1 < c!1")
        (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil))
 (ge_max 0
  (ge_max-1 nil 3276016566
   ("" (skosimp*)
    (("" (expand "max")
      (("" (case "b!1 < c!1")
        (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_ge_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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil))
 (gt_max 0
  (gt_max-1 nil 3276016566
   ("" (skosimp*)
    (("" (expand "max")
      (("" (case "b!1 < c!1")
        (("1" (assert) (("1" (prop) (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) (("2" (prop) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil))
   nil))
 (max_triangle 0
  (max_triangle-1 nil 3276016567
   ("" (skosimp*)
    (("" (expand "max")
      (("" (assert)
        (("" (lift-if)
          (("" (lift-if)
            (("" (lift-if)
              (("" (assert)
                (("" (prop)
                  (("" (lift-if)
                    (("" (assert)
                      (("" (prop)
                        (("" (lift-if) (("" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs 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_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (min_commutative 0
  (min_commutative-1 nil 3276018406
   ("" (skosimp*)
    (("" (expand "min")
      (("" (lift-if)
        (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (max_commutative 0
  (max_commutative-1 nil 3276018453
   ("" (skosimp*)
    (("" (expand "max")
      (("" (lift-if)
        (("" (assert) (("" (lift-if) (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((max 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))
   shostak)))