Quelle  min_max.prf   Sprache: Lisp

(min_max
 (min_id 0
  (min_id-1 nil 3443553414 ("" (grind) nil nil)
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   shostak))
 (max_id 0
  (max_id-1 nil 3443553429 ("" (grind) nil nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (min_comm 0
  (min_comm-1 nil 3443451882 ("" (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))
   shostak))
 (max_nnreal_0 0
  (max_nnreal_0-1 nil 3521211301 ("" (grind) nil nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (max_0_nnreal 0
  (max_0_nnreal-1 nil 3521211306 ("" (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)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types 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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (min_nnreal_0 0
  (min_nnreal_0-1 nil 3521211406 ("" (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)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types 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))
   shostak))
 (min_0_nnreal 0
  (min_0_nnreal-1 nil 3521211411 ("" (grind) nil nil)
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   shostak))
 (min_npreal_0 0
  (min_npreal_0-1 nil 3521211311 ("" (grind) nil nil)
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   shostak))
 (min_0_npreal 0
  (min_0_npreal-1 nil 3521211360 ("" (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)
    (<= const-decl "bool" reals nil)
    (npreal type-eq-decl nil real_types 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))
   shostak))
 (max_npreal_0 0
  (max_npreal_0-1 nil 3521211456 ("" (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)
    (<= const-decl "bool" reals nil)
    (npreal type-eq-decl nil real_types 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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (max_0_npreal 0
  (max_0_npreal-1 nil 3521211462 ("" (grind) nil nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (max_comm 0
  (max_comm-1 nil 3443451991 ("" (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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (min_assoc 0
  (min_assoc-1 nil 3443553780 ("" (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))
   shostak))
 (max_assoc 0
  (max_assoc-1 nil 3443553788 ("" (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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (min_max_id 0
  (min_max_id-1 nil 3443552739 ("" (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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (min_max 0
  (min_max-1 nil 3443552095 ("" (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)
    (minus_real_is_real application-judgement "real" 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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (max_min 0
  (max_min-1 nil 3443552099 ("" (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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   shostak))
 (add_min 0
  (add_min-1 nil 3443550979 ("" (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))
   shostak))
 (min_sub 0
  (min_sub-1 nil 3443452433 ("" (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))
   shostak))
 (sub_min 0
  (sub_min-1 nil 3443551127 ("" (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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (add_max 0
  (add_max-1 nil 3443551279 ("" (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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (max_sub 0
  (max_sub-1 nil 3443452557 ("" (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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (sub_max 0
  (sub_max-1 nil 3443551346 ("" (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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   shostak))
 (abs_max 0
  (abs_max-1 nil 3443551431 ("" (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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   shostak))
 (abs_min 0
  (abs_min-1 nil 3443554387 ("" (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_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)
    (minus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   shostak))
 (max_abs 0
  (max_abs-1 nil 3443551513 ("" (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_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   shostak))
 (nneg_mult_min 0
  (nneg_mult_min-1 nil 3443552278
   ("" (skeep)
    (("" (grind)
      (("1" (mult-by -1 "nnx") (("1" (assert) nil nil)) nil)
       ("2" (mult-by 1 "nnx") (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_gt_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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil))
   shostak))
 (npos_mult_min 0
  (npos_mult_min-1 nil 3443552879
   ("" (skeep)
    (("" (lemma "nneg_mult_min")
      (("" (inst -1 "-npx" "y" "z")
        (("" (neg-formula -1)
          (("" (lemma "max_min")
            (("" (inst? -1) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nneg_mult_min formula-decl nil min_max nil)
    (mult_neg formula-decl nil extra_tegies nil)
    (neg_neg formula-decl nil extra_tegies nil)
    (neg_mult formula-decl nil extra_tegies nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (max_min formula-decl nil min_max nil)
    (npreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (nneg_mult_max 0
  (nneg_mult_max-1 nil 3443552336
   ("" (skeep)
    (("" (grind)
      (("1" (mult-by -1 "nnx") (("1" (assert) nil nil)) nil)
       ("2" (mult-by 1 "nnx") (("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil))
   shostak))
 (npos_mult_max 0
  (npos_mult_max-1 nil 3443553333
   ("" (skeep)
    (("" (lemma "nneg_mult_max")
      (("" (inst -1 "-npx" "y" "z")
        (("" (neg-formula -1)
          (("" (lemma "min_max")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nneg_mult_max formula-decl nil min_max nil)
    (mult_neg formula-decl nil extra_tegies nil)
    (neg_neg formula-decl nil extra_tegies nil)
    (neg_mult formula-decl nil extra_tegies nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (min_max formula-decl nil min_max nil)
    (npreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (min_div_pos 0
  (min_div_pos-1 nil 3443552582
   ("" (skeep)
    (("" (grind)
      (("1" (cross-mult 1) nil nil) ("2" (cross-mult -1) nil nil))
      nil))
    nil)
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (div_mult_pos_gt1 formula-decl nil extra_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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil))
   shostak))
 (max_div_pos 0
  (max_div_pos-1 nil 3443552607
   ("" (skeep)
    (("" (grind)
      (("1" (cross-mult 1) nil nil) ("2" (cross-mult -1) nil nil))
      nil))
    nil)
   ((max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (div_mult_pos_lt1 formula-decl nil 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil))
   shostak))
 (min_le_max_left 0
  (min_le_max_left-1 nil 3443554282 ("" (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_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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   shostak))
 (min_le_max_right 0
  (min_le_max_right-1 nil 3443554290 ("" (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_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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil))
   shostak))
 (max_rec_TCC1 0
  (max_rec_TCC1-1 nil 3609939685 ("" (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)
    (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))
   nil))
 (max_rec_TCC2 0
  (max_rec_TCC2-1 nil 3609939685 ("" (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)
    (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))
   nil))
 (max_rec_TCC3 0
  (max_rec_TCC3-1 nil 3609939685 ("" (termination-tcc) nil nil) nil
   nil))
 (max_rec_TCC4 0
  (max_rec_TCC4-1 nil 3609939685
   ("" (skeep)
    (("" (typepred "v(F,j,k-1)")
      (("1" (split)
        (("1" (expand "max" 1)
          (("1" (case "F(k)<v(F,j,k-1)")
            (("1" (assert)
              (("1" (skeep -2)
                (("1" (inst + "i") (("1" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (assert)
              (("2" (inst + "k") (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (skeep)
          (("2" (inst -4 "i") (("2" (assert) nil nil)) nil)) nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (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)
    (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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil))
   nil))
 (min_rec_TCC1 0
  (min_rec_TCC1-1 nil 3609939685 ("" (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)
    (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))
   nil))
 (min_rec_TCC2 0
  (min_rec_TCC2-2 nil 3609939850
   ("" (skeep)
    (("" (typepred "v(F,j,k-1)")
      (("1" (split)
        (("1" (expand "min" 1)
          (("1" (case "F(k)>v(F,j,k-1)")
            (("1" (assert)
              (("1" (skeep -2)
                (("1" (inst + "i") (("1" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (assert)
              (("2" (inst + "k") (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (skeep)
          (("2" (inst -4 "i") (("2" (assert) nil nil)) nil)) nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (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)
    (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)
    (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)
    (> const-decl "bool" reals nil))
   nil)
  (min_rec_TCC2-1 nil 3609939685 ("" (subtype-tcc) nil nil) nil nil)))