Quelle  interval.prf

(interval
 (Member_Proper 0
  (Member_Proper-1 nil 3545739152 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Proper_Member 0
  (Proper_Member-1 nil 3545739170 ("" (grind) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Interval type-eq-decl nil interval 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)
    (Proper? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil))
   nil))
 (r2i_Proper 0
  (r2i_Proper-1 nil 3549199013 ("" (judgement-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Proper_eq_NonEmpty 0
  (Proper_eq_NonEmpty-1 nil 3546812344 ("" (grind) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Proper? const-decl "bool" interval nil)
    (EmptyInterval? const-decl "bool" interval nil))
   shostak))
 (Proper_NonEmpty 0
  (Proper_NonEmpty-1 nil 3577002288 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (eq_Incl 0
  (eq_Incl-1 nil 3545738788
   ("" (grind) (("" (decompose-equality) nil nil)) nil)
   ((Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil))
   shostak))
 (Incl_Member 0
  (Incl_Member-1 nil 3545739626 ("" (grind) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (<< const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil))
   shostak))
 (Member_Incl 0
  (Member_Incl-1 nil 3545739631 ("" (grind) nil nil)
   ((real_le_is_total_order name-judgement "(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)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil))
   shostak))
 (Incl_Proper 0
  (Incl_Proper-1 nil 3546770863 ("" (grind) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    (Proper? const-decl "bool" interval nil))
   shostak))
 (midpoint_inclusion 0
  (midpoint_inclusion-1 nil 3546711487 ("" (grind) nil nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Proper? const-decl "bool" interval nil)
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    (|##| const-decl "bool" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (Lt_Ge 0
  (Lt_Ge-1 nil 3318335123 ("" (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_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)
    (Lt const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (EmptyInterval? const-decl "bool" interval nil))
   shostak))
 (Le_Gt 0
  (Le_Gt-1 nil 3318335128 ("" (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)
    (Le const-decl "bool" interval nil)
    (Gt const-decl "bool" interval nil)
    (EmptyInterval? const-decl "bool" interval nil))
   shostak))
 (Trichotomy 0
  (Trichotomy-1 nil 3545736267 ("" (grind) nil 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)
    (Proper? const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (Le const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval nil))
   shostak))
 (Abs_TCC1 0
  (Abs_TCC1-1 nil 3579649336 ("" (subtype-tcc) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (nonneg_real_max application-judgement
     "{z: nonneg_real | z >= x AND z >= y}" 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)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (Zeroin? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Abs_TCC2 0
  (Abs_TCC2-1 nil 3579649336 ("" (grind) nil 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Zeroin? const-decl "bool" interval 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)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Sq_TCC1 0
  (Sq_TCC1-1 nil 3318333335 ("" (subtype-tcc) nil nil)
   ((Ge const-decl "bool" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    ([\|\|] const-decl "Interval" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Sq_TCC2 0
  (Sq_TCC2-1 nil 3579649506 ("" (subtype-tcc) nil nil)
   ((Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    ([\|\|] const-decl "Interval" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Sq_TCC3 0
  (Sq_TCC3-1 nil 3579649506 ("" (subtype-tcc) nil 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    ([\|\|] const-decl "Interval" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Pow_TCC1 0
  (Pow_TCC1-1 nil 3350326108 ("" (subtype-tcc) nil nil)
   ((Ge const-decl "bool" interval nil)
    (odd? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil))
   nil))
 (Pow_TCC2 0
  (Pow_TCC2-1 nil 3350326108 ("" (subtype-tcc) nil nil)
   ((Ge const-decl "bool" interval nil)
    (odd? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil))
   nil))
 (Pow_TCC3 0
  (Pow_TCC3-1 nil 3350326108 ("" (subtype-tcc) nil nil)
   ((Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (odd? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil))
   nil))
 (Pow_TCC4 0
  (Pow_TCC4-1 nil 3350326108 ("" (subtype-tcc) nil nil)
   ((Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (odd? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil))
   nil))
 (Pow_TCC5 0
  (Pow_TCC5-1 nil 3350326108 ("" (subtype-tcc) nil nil)
   ((Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (odd? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil))
   nil))
 (Pow_TCC6 0
  (Pow_TCC6-1 nil 3350326108 ("" (subtype-tcc) nil nil)
   ((Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (odd? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil))
   nil))
 (Intersection_inclusion 0
  (Intersection_inclusion-1 nil 3577002526 ("" (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)
    (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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Intersection const-decl "Interval" interval nil)
    (|##| const-decl "bool" interval nil))
   nil))
 (Intersection_left_Empty 0
  (Intersection_left_Empty-1 nil 3579697131 ("" (grind) nil 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)
    (EmptyInterval? const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Intersection const-decl "Interval" interval nil))
   shostak))
 (Intersection_right_Empty 0
  (Intersection_right_Empty-1 nil 3579697162 ("" (grind) nil 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)
    (EmptyInterval? const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Intersection const-decl "Interval" interval nil))
   shostak))
 (Add_comm 0
  (Add_comm-1 nil 3318335139 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil))
   shostak))
 (Mult_comm 0
  (Mult_comm-1 nil 3318334112 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil))
   shostak))
 (Neg_Incl 0
  (Neg_Incl-1 nil 3545739708 ("" (grind) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil))
   nil))
 (Zeroless0 0
  (Zeroless0-1 nil 3318335234 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (|##| const-decl "bool" interval nil)
    (Zeroless? const-decl "bool" interval nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (Neg_Ge_0 0
  (Neg_Ge_0-1 nil 3318335239 ("" (grind) nil nil)
   ((minus_real_is_real application-judgement "real" 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)
    (Le const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil))
   shostak))
 (Strict_Lt 0
  (Strict_Lt-1 nil 3320961671 ("" (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_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)
    (|##| const-decl "bool" interval nil)
    (StrictInterval? const-decl "bool" interval nil))
   shostak))
 (Halves 0
  (Halves-1 nil 3321035367 ("" (skeep) (("" (grind) nil nil)) nil)
   ((slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (HalfRight const-decl "Interval" interval nil)
    (size const-decl "real" interval nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (HalfLeft const-decl "Interval" interval nil))
   shostak))
 (Halves_Incl 0
  (Halves_Incl-1 nil 3321095140 ("" (grind) nil nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Proper? const-decl "bool" interval nil)
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (HalfLeft const-decl "Interval" interval nil)
    (<< const-decl "bool" interval nil)
    (HalfRight const-decl "Interval" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (Halves_inclusion 0
  (Halves_inclusion-1 nil 3546810076 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (|##| const-decl "bool" interval nil)
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (HalfLeft const-decl "Interval" interval nil)
    (HalfRight const-decl "Interval" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (Incl_trans 0
  (Incl_trans-1 nil 3321095152 ("" (grind) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil))
   shostak))
 (Pow2_Sq 0
  (Pow2_Sq-1 nil 3321310186 ("" (grind) nil nil)
   ((Ge const-decl "bool" interval nil)
    (odd? const-decl "bool" integers nil)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Pow const-decl "Interval" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Sq const-decl "(NonNeg?)" interval nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil))
   shostak))
 (Mult_Neg_Neg 0
  (Mult_Neg_Neg-1 nil 3545736683 ("" (grind) nil nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (Mult_Neg_left 0
  (Mult_Neg_left-1 nil 3545736690 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (Mult_Neg_right 0
  (Mult_Neg_right-1 nil 3545736695 ("" (grind) nil nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (Sq_Neg_eq 0
  (Sq_Neg_eq-1 nil 3545818757 ("" (grind) nil 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Ge const-decl "bool" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    ([\|\|] const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Sq const-decl "(NonNeg?)" interval nil)
    (Neg const-decl "Interval" interval nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (Union_id 0
  (Union_id-1 nil 3546381093
   ("" (skeep)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((Union const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals 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)
    ([\|\|] const-decl "Interval" interval nil))
   shostak))
 (Union_symm 0
  (Union_symm-1 nil 3546381143 ("" (grind) nil 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Union const-decl "Interval" interval nil))
   shostak))
 (Union_Incl_left 0
  (Union_Incl_left-1 nil 3546812242 ("" (grind) nil 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Union const-decl "Interval" interval nil)
    (<< const-decl "bool" interval nil))
   shostak))
 (Union_Incl_right 0
  (Union_Incl_right-1 nil 3546812266 ("" (grind) nil 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Union const-decl "Interval" interval nil)
    (<< const-decl "bool" interval nil))
   shostak))
 (Add_0_r 0
  (Add_0_r-1 nil 3320066346
   ("" (skeep)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((r2i_Proper application-judgement "ProperInterval" interval nil)
    (Add const-decl "Interval" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil))
   shostak))
 (Add_0_l 0
  (Add_0_l-1 nil 3320066375
   ("" (skeep)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((r2i_Proper application-judgement "ProperInterval" interval nil)
    (Add const-decl "Interval" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil))
   nil))
 (Mult_1_r 0
  (Mult_1_r-1 nil 3320066384
   ("" (skeep)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((r2i_Proper application-judgement "ProperInterval" interval nil)
    (Mult const-decl "Interval" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (pXm const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (Mult_1_l 0
  (Mult_1_l-1 nil 3320066393
   ("" (skeep)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((r2i_Proper application-judgement "ProperInterval" interval nil)
    (Mult const-decl "Interval" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (pXm const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (pXp const-decl "Interval" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (Div_1 0
  (Div_1-1 nil 3318335177
   ("" (skosimp)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((r2i_Proper application-judgement "ProperInterval" interval nil)
    (Div const-decl "Interval" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (pXm const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (Pow_0 0
  (Pow_0-1 nil 3318335195
   ("" (skosimp)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((r2i_Proper application-judgement "ProperInterval" interval 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)
    (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)
    (Pow const-decl "Interval" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil))
   shostak))
 (Pow_1 0
  (Pow_1-1 nil 3318335202
   ("" (skosimp)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) 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)
    (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)
    (Pow const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (^ const-decl "real" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (Ge const-decl "bool" interval nil))
   shostak))
 (lb_interval 0
  (lb_interval-1 nil 3318621128 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)) shostak))
 (lb_r2i 0
  (lb_r2i-1 nil 3319735236 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)) shostak))
 (ub_interval 0
  (ub_interval-1 nil 3318621141 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)) shostak))
 (ub_r2i 0
  (ub_r2i-1 nil 3319735241 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)) shostak))
 (Incl_reflx 0
  (Incl_reflx-1 nil 3549125759 ("" (grind) nil nil)
   ((<< const-decl "bool" interval nil)) shostak))
 (Incl_r2i 0
  (Incl_r2i-1 nil 3549125766 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (<< const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil))
   shostak))
 (Neg_Neg 0
  (Neg_Neg-1 nil 3318335220
   ("" (skosimp)
    (("" (decompose-equality)
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((Neg const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil))
   shostak))
 (ub_inclusion 0
  (ub_inclusion-1 nil 3545739421 ("" (grind) nil nil)
   ((Proper? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil))
   shostak))
 (lb_inclusion 0
  (lb_inclusion-1 nil 3545739427 ("" (grind) nil nil)
   ((Proper? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil))
   shostak))
 (Neg_interval 0
  (Neg_interval-1 nil 3318621148 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil))
   shostak))
 (Pos_Gt_0 0
  (Pos_Gt_0-1 nil 3318335249 ("" (grind) nil nil)
   ((Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   shostak))
 (NonNeg_Ge_0 0
  (NonNeg_Ge_0-1 nil 3318335254 ("" (grind) nil nil)
   ((Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   shostak))
 (Pos_Neg_Lt_0 0
  (Pos_Neg_Lt_0-1 nil 3318335259 ("" (grind) nil 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Lt const-decl "bool" interval nil))
   shostak))
 (NonNeg_Neg_Le_0 0
  (NonNeg_Neg_Le_0-1 nil 3318335264 ("" (grind) nil nil)
   ((minus_real_is_real application-judgement "real" reals 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)
    (Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil))
   shostak))
 (r2i_sharp_eq 0
  (r2i_sharp_eq-1 nil 3567640507 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    ([\|\|] const-decl "Interval" interval nil)
    (|##| const-decl "bool" interval nil))
   shostak))
 (r2i_Le 0
  (r2i_Le-1 nil 3319587327 ("" (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 "Interval" interval nil)
    (Le const-decl "bool" interval nil))
   shostak))
 (r2i_Lt 0
  (r2i_Lt-1 nil 3319587332 ("" (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 "Interval" interval nil)
    (Lt const-decl "bool" interval nil))
   shostak))
 (r2i_Ge 0
  (r2i_Ge-1 nil 3319587338 ("" (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 "Interval" interval nil)
    (Ge const-decl "bool" interval nil))
   shostak))
 (r2i_Gt 0
  (r2i_Gt-1 nil 3319587343 ("" (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 "Interval" interval nil)
    (Gt const-decl "bool" interval nil))
   shostak))
 (Lt_Le 0
  (Lt_Le-1 nil 3318335287 ("" (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_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)
    (Lt const-decl "bool" interval nil)
    (Le const-decl "bool" interval nil))
   shostak))
 (Gt_Ge 0
  (Gt_Ge-1 nil 3318335291 ("" (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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Gt const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil))
   shostak))
 (inclusion_Gt 0
  (inclusion_Gt-1 nil 3318335303 ("" (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)
    (|##| const-decl "bool" interval nil)
    (Gt const-decl "bool" interval nil))
   shostak))
 (inclusion_Ge 0
  (inclusion_Ge-1 nil 3318335308 ("" (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_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)
    (|##| const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil))
   shostak))
 (inclusion_Lt 0
  (inclusion_Lt-1 nil 3318335312 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (Lt const-decl "bool" interval nil))
   shostak))
 (inclusion_Le 0
  (inclusion_Le-1 nil 3318335316 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (Le const-decl "bool" interval nil))
   shostak))
 (r2i_trans 0
  (r2i_trans-1 nil 3303814164 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil))
   shostak))
 (add2sub 0
  (add2sub-1 nil 3350326109 ("" (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_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Sub const-decl "Interval" interval nil))
   shostak))
 (sub2add 0
  (sub2add-1 nil 3350326116 ("" (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_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil))
   shostak))
 (Member_trans 0
  (Member_trans-1 nil 3318335334 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil))
   shostak))
 (r2i_inclusion 0
  (r2i_inclusion-1 nil 3302519809 ("" (grind) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (|##| const-decl "bool" interval nil))
   shostak))
 (Add_inclusion 0
  (Add_inclusion-1 nil 3318335347 ("" (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_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil))
   shostak))
 (Sub_inclusion 0
  (Sub_inclusion-1 nil 3318335352 ("" (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_minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Sub const-decl "Interval" interval nil))
   shostak))
 (Neg_inclusion 0
  (Neg_inclusion-1 nil 3318335356 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil))
   shostak))
 (pXp 0
  (pXp-1 nil 3278260700 ("" (grind :theories "real_props") nil nil)
   ((pXp const-decl "Interval" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (|##| const-decl "bool" interval nil)
    (Ge const-decl "bool" interval 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_times_real_is_real application-judgement "real" reals nil)
    (le_times_le_pos formula-decl nil real_props 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))
   shostak))
 (nXp 0
  (nXp-1 nil 3278260739
   ("" (skeep)
    (("" (expand "nXp")
      (("" (lemma "Neg_inclusion")
        (("" (inst -1 "X" "x")
          (("" (assert)
            (("" (lemma "pXp")
              (("" (inst -1 "Neg(X)" "Y" "-x" "y")
                (("" (assert)
                  (("" (split -1)
                    (("1" (lemma "Neg_inclusion")
                      (("1" (inst -1 "pXp(Neg(X),Y)" "-x*y")
                        (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nXp const-decl "Interval" interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval 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)
    (pXp formula-decl nil interval nil)
    (Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval 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)
    (pXp const-decl "Interval" interval nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Neg const-decl "Interval" interval nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (Neg_inclusion formula-decl nil interval nil))
   nil))
 (pXn 0
  (pXn-1 nil 3278260788
   ("" (skeep)
    (("" (expand "pXn")
      (("" (lemma "nXp")
        (("" (inst -1 "Y" "X" "y" "x") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((pXn const-decl "Interval" interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval 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_times_real_is_real application-judgement "real" reals nil)
    (nXp formula-decl nil interval nil))
   nil))
 (nXn 0
  (nXn-2 nil 3278261218 ("" (grind :theories "real_props") nil nil)
   ((nXn const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (neg_times_neg formula-decl nil real_props nil)
    (Neg const-decl "Interval" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (|##| const-decl "bool" interval nil)
    (Le const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (le_times_le_neg formula-decl nil real_props 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))
 (pXm 0
  (pXm-1 nil 3301392992
   ("" (skeep)
    (("" (case "y >= 0")
      (("1" (grind :theories "real_props")
        (("1" (case "x * y >= 0")
          (("1" (case "ub(X) * lb(Y) <= 0")
            (("1" (assert) nil nil) ("2" (grind-reals) nil nil)) nil)
           ("2" (grind-reals) nil nil))
          nil))
        nil)
       ("2" (grind :theories "real_props")
        (("1" (case "x*y <= 0")
          (("1" (case "ub(X) * ub(Y) >= 0")
            (("1" (assert) nil nil) ("2" (grind-reals) nil nil)) nil)
           ("2" (grind-reals) nil nil))
          nil)
         ("2" (mult-ineq -6 -7 (+ -)) nil nil))
        nil))
      nil))
    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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (neg_times_le formula-decl nil real_props nil)
    (pos_times_ge formula-decl nil real_props nil)
    (Interval type-eq-decl nil interval nil)
    (<= const-decl "bool" reals nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (Ge const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (le_times_le_any1 formula-decl nil extra_real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   shostak))
 (mXp 0
  (mXp-1 nil 3301397382
   ("" (skeep)
    (("" (expand "mXp")
      (("" (lemma "pXm")
        (("" (inst -1 "Y" "X" "y" "x") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((mXp const-decl "Interval" interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval 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_times_real_is_real application-judgement "real" reals nil)
    (pXm formula-decl nil interval nil))
   shostak))
 (nXm 0
  (nXm-2 nil 3579693670
   ("" (skeep)
    (("" (expand "nXm")
      (("" (lemma "pXm")
        (("" (inst -1 "Neg(X)" "Y" "-x" "y")
          (("" (assert)
            (("" (split)
              (("1" (lemma "Neg_inclusion")
                (("1" (inst? -1) (("1" (assert) nil nil)) nil)) nil)
               ("2" (rewrite "Neg_Ge_0") nil nil)
               ("3" (rewrite "Neg_inclusion") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nXm const-decl "Interval" interval nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Neg const-decl "Interval" interval 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (pXm const-decl "Interval" interval nil)
    (Neg_inclusion formula-decl nil interval nil)
    (Neg_Ge_0 formula-decl nil interval nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (pXm formula-decl nil interval nil))
   nil))
 (mXn 0
  (mXn-1 nil 3301399245
   ("" (skeep)
    (("" (expand "mXn")
      (("" (lemma "nXm")
        (("" (inst -1 "Y" "X" "y" "x") (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((mXn const-decl "Interval" interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval 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_times_real_is_real application-judgement "real" reals nil)
    (nXm formula-decl nil interval nil))
   shostak))
 (mXm 0
  (mXm-1 nil 3301399821
   ("" (skeep)
    (("" (expand "mXm")
      (("" (expand "Zeroin?")
        ((""
          (case "ub(X) * ub(Y) >=0"
            "lb(X) * lb(Y) >= 0"
            "ub(X) * lb(Y) <= 0"
            "lb(X) * ub(Y) <= 0")
          (("1" (label "H" (-1 -2 -3 -4))
            (("1" (hide "H")
              (("1" (grind :theories "real_props")
                (("1" (case "x*y >= 0")
                  (("1" (grind-reals)
                    (("1" (mult-ineq -7 -9 (- -))
                      (("1" (assert) nil nil)) nil))
                    nil)
                   ("2" (reveal "H")
                    (("2" (name-replace "A" "x*y")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (case "x*y >= 0")
                  (("1" (grind-reals)
                    (("1" (mult-ineq -8 -10 (+ +))
                      (("1" (assert) nil nil)) nil))
                    nil)
                   ("2" (reveal "H")
                    (("2" (name-replace "A" "x*y")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("3" (case "x*y >= 0")
                  (("1" (reveal "H")
                    (("1" (name-replace "A" "x*y")
                      (("1" (assert) nil nil)) nil))
                    nil)
                   ("2" (grind-reals)
                    (("1" (mult-ineq -5 -8 (- +))
                      (("1" (assert) nil nil)) nil)
                     ("2" (mult-ineq -6 -7 (+ -)) nil nil))
                    nil))
                  nil)
                 ("4" (case "x*y >= 0")
                  (("1" (reveal "H")
                    (("1" (name-replace "A" "x*y")
                      (("1" (assert) nil nil)) nil))
                    nil)
                   ("2" (grind-reals)
                    (("1" (mult-ineq -5 -8 (- +)) nil nil)
                     ("2" (mult-ineq -6 -7 (+ -))
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2) (("2" (grind-reals) nil nil)) nil)
           ("3" (hide 2) (("3" (grind-reals) nil nil)) nil)
           ("4" (hide 2) (("4" (grind-reals) nil nil)) nil)
           ("5" (hide 2) (("5" (grind-reals) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((mXm const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (<= const-decl "bool" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (le_times_le_any1 formula-decl nil extra_real_props nil)
    (le_times_le_neg formula-decl nil real_props nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (pos_times_ge formula-decl nil real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (neg_times_le formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_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)
    (|##| const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Zeroin? const-decl "bool" interval nil))
   shostak))
 (Mult_inclusion 0
  (Mult_inclusion-2 nil 3579648824
   ("" (skeep)
    (("" (expand "Mult")
      (("" (case-replace "Ge(X, 0) AND Ge(Y, 0)")
        (("1" (rewrite "pXp") nil nil)
         ("2" (replace 1)
          (("2" (case-replace "Ge(X, 0) AND Le(Y, 0)")
            (("1" (rewrite "pXn") nil nil)
             ("2" (replace 1)
              (("2" (case-replace "Ge(X, 0)")
                (("1" (rewrite "pXm")
                  (("1" (hide 4) (("1" (grind) nil nil)) nil)) nil)
                 ("2" (replace 1)
                  (("2" (case-replace "Le(X, 0) AND Le(Y, 0)")
                    (("1" (rewrite "nXn") nil nil)
                     ("2" (replace 1)
                      (("2" (case-replace "Le(X, 0) AND Ge(Y, 0)")
                        (("1" (rewrite "nXp") nil nil)
                         ("2" (replace 1)
                          (("2" (case-replace "Le(X, 0)")
                            (("1" (rewrite "nXm")
                              (("1"
                                (hide 5)
                                (("1" (grind) nil nil))
                                nil))
                              nil)
                             ("2" (replace 1)
                              (("2"
                                (case-replace "Ge(Y, 0)")
                                (("1"
                                  (rewrite "mXp")
                                  (("1"
                                    (hide 4)
                                    (("1" (grind) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (replace 1)
                                  (("2"
                                    (case-replace "Le(Y, 0)")
                                    (("1"
                                      (rewrite "mXn")
                                      (("1"
                                        (hide 5)
                                        (("1" (grind) nil nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (replace 1)
                                      (("2"
                                        (rewrite "mXm")
                                        (("1"
                                          (hide 6)
                                          (("1" (grind) nil nil))
                                          nil)
                                         ("2"
                                          (hide 6)
                                          (("2" (grind) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Mult const-decl "Interval" interval nil)
    (mXm formula-decl nil interval nil)
    (mXn formula-decl nil interval nil)
    (mXp formula-decl nil interval nil)
    (nXm formula-decl nil interval nil)
    (nXp formula-decl nil interval nil)
    (nXn formula-decl nil interval nil)
    (pXm formula-decl nil interval 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Zeroin? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (pXn formula-decl nil interval nil)
    (Le const-decl "bool" interval nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (pXp formula-decl nil interval nil)
    (Ge const-decl "bool" interval 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)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)
  (Mult_inclusion-1 nil 3318335639
   ("" (skeep) (("" (rewrite "Mult__inclusion") nil nil)) nil) nil
   nil))
 (Abs_inclusion 0
  (Abs_inclusion-1 nil 3318335650 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (|##| const-decl "bool" interval nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (Zeroin? const-decl "bool" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    ([\|\|] const-decl "Interval" interval nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (Abs const-decl "(NonNeg?)" interval nil))
   shostak))
 (abs_sharp_le 0
  (abs_sharp_le-1 nil 3567637838 ("" (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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    ([\|\|] const-decl "Interval" interval nil)
    (|##| const-decl "bool" interval nil))
   shostak))
 (abs_sharp_lt 0
  (abs_sharp_lt-1 nil 3567637891 ("" (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_le_is_total_order name-judgement "(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)
    ([\|\|] const-decl "Interval" interval nil)
    (|##| const-decl "bool" interval nil))
   shostak))
 (pow_0_0 0
  (pow_0_0-1 nil 3307281813 ("" (grind) nil nil)
   ((expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (nat_expt application-judgement "nat" exponentiation nil))
   shostak))
 (pow_sq_TCC1 0
  (pow_sq_TCC1-1 nil 3318335667 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (pow_sq 0
  (pow_sq-1 nil 3318335670 ("" (grind) nil nil)
   ((expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (sq const-decl "nonneg_real" sq "reals/"))
   shostak))
 (pow_neg_n_odd_TCC1 0
  (pow_neg_n_odd_TCC1-1 nil 3546006073 ("" (subtype-tcc) nil nil)
   ((nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (pow_neg_n_odd_TCC2 0
  (pow_neg_n_odd_TCC2-1 nil 3546006073 ("" (subtype-tcc) nil nil)
   ((nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (pow_neg_n_odd 0
  (pow_neg_n_odd-1 nil 3546006073
   ("" (skeep)
    (("" (case "x=0")
      (("1" (grind) nil nil)
       ("2" (rewrite "expt_plus")
        (("2" (rewrite "expt_plus")
          (("2" (rewrite "expt_times")
            (("2" (rewrite "expt_times")
              (("2" (rewrite "pow_sq")
                (("2" (rewrite "pow_sq")
                  (("2" (rewrite "sq_neg")
                    (("2" (rewrite "expt_x1")
                      (("2" (rewrite "expt_x1")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (^ const-decl "real" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (nnreal_exp application-judgement "nnreal" exponentiation nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (sq_neg formula-decl nil sq "reals/")
    (pow_sq formula-decl nil interval nil)
    (expt_times formula-decl nil exponentiation nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (expt_plus formula-decl nil exponentiation nil))
   nil))
 (pow_neg_odd_TCC1 0
  (pow_neg_odd_TCC1-1 nil 3546003881 ("" (subtype-tcc) nil nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (/= const-decl "boolean" notequal nil)
    (odd? const-decl "bool" integers nil))
   nil))
 (pow_neg_odd_TCC2 0
  (pow_neg_odd_TCC2-1 nil 3546003881 ("" (subtype-tcc) nil nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (/= const-decl "boolean" notequal nil)
    (odd? const-decl "bool" integers nil))
   nil))
 (pow_neg_odd 0
  (pow_neg_odd-1 nil 3307287721
   ("" (skeep)
    (("" (expand "odd?")
      (("" (skeep -1)
        (("" (case "j>=0")
          (("1" (replaces -2) (("1" (rewrite "pow_neg_n_odd") nil nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (odd? const-decl "bool" integers 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)
    (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)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pow_neg_n_odd formula-decl nil interval nil))
   nil))
 (pow_neg_n_even_TCC1 0
  (pow_neg_n_even_TCC1-1 nil 3546006109 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (pow_neg_n_even_TCC2 0
  (pow_neg_n_even_TCC2-1 nil 3546006109 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (pow_neg_n_even 0
  (pow_neg_n_even-1 nil 3546006109
   ("" (skeep)
    (("" (case "x=0")
      (("1" (grind) nil nil)
       ("2" (rewrite "expt_times")
        (("2" (rewrite "expt_times")
          (("2" (rewrite "pow_sq")
            (("2" (rewrite "pow_sq") (("2" (rewrite "sq_neg") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (^ const-decl "real" exponentiation nil)
    (sq_neg formula-decl nil sq "reals/")
    (pow_sq formula-decl nil interval nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (expt_times formula-decl nil exponentiation nil))
   nil))
 (pow_neg_even_TCC1 0
  (pow_neg_even_TCC1-1 nil 3546006176 ("" (subtype-tcc) nil nil)
   ((even? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (pow_neg_even_TCC2 0
  (pow_neg_even_TCC2-1 nil 3546006176 ("" (subtype-tcc) nil nil)
   ((even? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (pow_neg_even 0
  (pow_neg_even-1 nil 3307287744
   ("" (skeep)
    (("" (expand "even?")
      (("" (skeep -1)
        (("" (case "j>=0")
          (("1" (replaces -2)
            (("1" (rewrite "pow_neg_n_even") nil nil)) nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((even? const-decl "bool" integers 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)
    (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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pow_neg_n_even formula-decl nil interval nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
 (pow_pos_TCC1 0
  (pow_pos_TCC1-1 nil 3307288079 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) shostak))
 (pow_pos 0
  (pow_pos-1 nil 3307282465
   ("" (skeep)
    (("" (case "x=0")
      (("1" (grind) nil nil)
       ("2" (use "posreal_exp")
        (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
      nil))
    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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nat_expt application-judgement "nat" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (> const-decl "bool" reals nil)
    (x skolem-const-decl "real" interval nil)
    (>= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (posreal_exp judgement-tcc nil exponentiation nil))
   nil))
 (pow_even_n_pos 0
  (pow_even_n_pos-1 nil 3545998410
   ("" (skeep)
    (("" (case "x>=0")
      (("1" (rewrite "pow_pos") nil nil)
       ("2" (lemma "pow_neg_n_even")
        (("2" (inst?)
          (("2" (replaces -1 :dir rl)
            (("2" (rewrite "pow_pos") nil nil)) nil))
          nil))
        nil))
      nil))
    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)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (pow_pos formula-decl nil interval nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (pow_neg_n_even formula-decl nil interval nil))
   nil))
 (pow_even_pos 0
  (pow_even_pos-1 nil 3307282506
   ("" (skeep)
    (("" (expand "even?")
      (("" (skeep -1)
        (("" (case "j>=0")
          (("1" (replaces -2)
            (("1" (rewrite "pow_even_n_pos") nil nil)) nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((even? const-decl "bool" integers 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)
    (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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pow_even_n_pos formula-decl nil interval nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil))
 (pow_odd_n_neg 0
  (pow_odd_n_neg-1 nil 3545998363
   ("" (skeep)
    (("" (case "x=0")
      (("1" (grind) nil nil)
       ("2" (rewrite "expt_plus")
        (("2" (case-replace "2*n=n*2")
          (("1" (hide -1)
            (("1" (rewrite "expt_times")
              (("1" (rewrite "expt_x1")
                (("1" (rewrite "pow_sq") (("1" (grind-reals) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    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)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (^ const-decl "real" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (expt_times formula-decl nil exponentiation nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (pow_sq formula-decl nil interval nil)
    (neg_times_le formula-decl nil real_props nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (expt_plus formula-decl nil exponentiation nil))
   nil))
 (pow_odd_neg 0
  (pow_odd_neg-1 nil 3307282587
   ("" (skeep)
    (("" (expand "odd?")
      (("" (skeep -1)
        (("" (case "j >= 0")
          (("1" (replaces -2) (("1" (rewrite "pow_odd_n_neg") nil nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (odd? const-decl "bool" integers 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)
    (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)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pow_odd_n_neg formula-decl nil interval nil))
   shostak))
 (pow_incr_pos_TCC1 0
  (pow_incr_pos_TCC1-1 nil 3307288079 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) shostak))
 (pow_incr_pos 0
  (pow_incr_pos-1 nil 3307282932
   ("" (skeep)
    (("" (splash -3)
      (("1" (case-replace "x=0")
        (("1" (rewrite "pow_0_0")
          (("1" (use "pow_pos") (("1" (assert) nil nil)) nil)) nil)
         ("2" (assert) nil nil))
        nil)
       ("2" (rewrite "both_sides_expt_pos_le") (("2" (grind) nil nil))
        nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pow_0_0 formula-decl nil interval nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil 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)
    (pow_pos formula-decl nil interval nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (both_sides_expt_pos_le formula-decl nil exponentiation nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil))
   nil))
 (pow_incr_odd_TCC1 0
  (pow_incr_odd_TCC1-1 nil 3307288079 ("" (subtype-tcc) nil nil)
   ((even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (/= const-decl "boolean" notequal nil)
    (odd? const-decl "bool" integers nil))
   shostak))
 (pow_incr_odd 0
  (pow_incr_odd-1 nil 3307284124
   ("" (skeep)
    (("" (case "x>=0")
      (("1" (rewrite "pow_incr_pos")
        (("1" (flatten) (("1" (grind) nil nil)) nil)) nil)
       ("2" (assert)
        (("2" (hide -2)
          (("2" (expand "odd?")
            (("2" (skeep -1)
              (("2" (case "j >=0")
                (("1" (replace -2)
                  (("1" (lemma "pow_odd_n_neg")
                    (("1" (inst -1 "j" "x")
                      (("1" (assert)
                        (("1" (case "y<=0")
                          (("1" (lemma "pow_neg_n_odd")
                            (("1" (inst -1 "j" "-x")
                              (("1"
                                (assert)
                                (("1"
                                  (replaces -1)
                                  (("1"
                                    (lemma "pow_neg_n_odd")
                                    (("1"
                                      (inst -1 "j" "-y")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (replaces -1)
                                          (("1"
                                            (replaces -4 :dir rl)
                                            (("1"
                                              (lemma "pow_incr_pos")
                                              (("1"
                                                (inst -1 "n" "-y" "-x")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma "pow_pos")
                            (("2" (inst -1 "n" "y")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (odd? const-decl "bool" 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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (pow_incr_pos formula-decl nil interval nil)
    (j skolem-const-decl "int" interval nil)
    (<= const-decl "bool" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (pow_neg_n_odd formula-decl nil interval nil)
    (pow_pos formula-decl nil interval nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (pow_odd_n_neg formula-decl nil interval nil))
   shostak))
 (pow_decr_even_TCC1 0
  (pow_decr_even_TCC1-1 nil 3307288080 ("" (subtype-tcc) nil nil)
   ((even? const-decl "bool" integers nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (pow_decr_even 0
  (pow_decr_even-1 nil 3307287495
   ("" (skeep)
    (("" (assert)
      (("" (expand "even?")
        (("" (skeep -1)
          (("" (replace -1)
            (("" (case "j >= 0")
              (("1" (lemma "pow_neg_n_even")
                (("1" (inst -1 "j" "-x")
                  (("1" (lemma "pow_neg_n_even")
                    (("1" (inst -1 "j" "-y")
                      (("1" (assert)
                        (("1" (replaces (-1 -2))
                          (("1" (replaces -2 :dir rl)
                            (("1" (rewrite "pow_incr_pos")
                              (("1"
                                (flatten)
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (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)
    (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)
    (j skolem-const-decl "int" interval nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (pow_incr_pos formula-decl nil interval nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (pow_neg_n_even formula-decl nil interval nil)
    (even? const-decl "bool" integers nil))
   shostak))
 (Pow_Neg_even 0
  (Pow_Neg_even-1 nil 3545855075
   ("" (skeep)
    (("" (lemma "even_or_odd")
      (("" (inst? -1)
        (("" (assert)
          (("" (expand "Pow")
            (("" (assert)
              (("" (case "n=0")
                (("1" (assert) nil nil)
                 ("2" (assert)
                  (("2" (expand "Neg")
                    (("2" (expand "[||]")
                      (("2" (lemma "pow_neg_even")
                        (("2" (inst-cp -1 "n" "lb(X)")
                          (("2" (inst -1 "n" "ub(X)")
                            (("2" (assert)
                              (("2"
                                (replaces (-1 -2))
                                (("2" (grind :exclude "^") nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((even_or_odd formula-decl nil naturalnumbers nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (Proper? const-decl "bool" interval nil)
    (even? const-decl "bool" integers nil)
    (odd? const-decl "bool" integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides 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)
    (pow_neg_even formula-decl nil interval nil)
    (Neg const-decl "Interval" interval nil)
    (r2i_Proper application-judgement "ProperInterval" interval nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Pow const-decl "Interval" interval 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))
   shostak))
 (Pow_inclusion_TCC1 0
  (Pow_inclusion_TCC1-1 nil 3318333335 ("" (subtype-tcc) nil nil)
   ((|##| const-decl "bool" interval nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (Pow_inclusion 0
  (Pow_inclusion-1 nil 3318335744
   ("" (skeep)
    (("" (case "n=0")
      (("1" (replaces) (("1" (grind) nil nil)) nil)
       ("2" (expand "Pow")
        (("2" (assert)
          (("2" (expand "##")
            (("2" (flatten)
              (("2" (ground)
                (("1" (lift-if)
                  (("1" (ground)
                    (("1" (expand "Ge" -1)
                      (("1" (rewrite "pow_incr_pos") nil nil)) nil)
                     ("2" (rewrite "pow_incr_odd") nil nil)
                     ("3" (expand "Le" -1)
                      (("3" (rewrite "pow_decr_even")
                        (("3" (rewrite "even_or_odd") nil nil)) nil))
                      nil)
                     ("4" (lemma "even_or_odd")
                      (("4" (inst?)
                        (("4" (assert)
                          (("4" (lemma "pow_even_pos")
                            (("4" (inst?) (("4" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (lift-if)
                  (("2" (ground)
                    (("1" (expand "Ge" -1)
                      (("1" (rewrite "pow_incr_pos") nil nil)) nil)
                     ("2" (rewrite "pow_incr_odd") nil nil)
                     ("3" (expand "Le" -1)
                      (("3" (rewrite "pow_decr_even")
                        (("3" (rewrite "even_or_odd") nil nil)) nil))
                      nil)
                     ("4" (case "x>=0")
                      (("1" (expand "max")
                        (("1" (lift-if)
                          (("1" (split)
                            (("1" (flatten)
                              (("1" (rewrite "pow_incr_pos") nil nil))
                              nil)
                             ("2" (flatten)
                              (("2"
                                (case "x^n <= ub(X)^n")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (rewrite "pow_incr_pos")
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand "max")
                        (("2" (lift-if)
                          (("2" (split)
                            (("1" (flatten)
                              (("1"
                                (case "x^n <=  lb(X) ^ n")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (rewrite "pow_decr_even")
                                  (("2"
                                    (rewrite "even_or_odd")
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (flatten)
                              (("2"
                                (rewrite "pow_decr_even")
                                (("2" (rewrite "even_or_odd") nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (|##| const-decl "bool" interval nil)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Pow const-decl "Interval" interval nil)
    (r2i_Proper application-judgement "ProperInterval" interval 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)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (pow_even_pos formula-decl nil interval nil)
    (Le const-decl "bool" interval nil)
    (even_or_odd formula-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pow_decr_even formula-decl nil interval nil)
    (pow_incr_odd formula-decl nil interval nil)
    (Ge const-decl "bool" interval nil)
    (pow_incr_pos formula-decl nil interval nil)
    (Interval type-eq-decl nil interval nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lb_interval formula-decl nil interval nil)
    (ub_interval formula-decl nil interval nil))
   nil))
 (Sq_inclusion 0
  (Sq_inclusion-2 nil 3318335884
   ("" (skeep)
    (("" (rewrite "Pow2_Sq" :dir rl)
      (("" (case-replace "sq(x)=x^2")
        (("1" (hide -1) (("1" (rewrite "Pow_inclusion") nil nil)) nil)
         ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((Pow2_Sq formula-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (expt def-decl "real" exponentiation nil)
    (Pow_inclusion formula-decl nil interval nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" 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)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (Div_inclusion_TCC1 0
  (Div_inclusion_TCC1-1 nil 3318333335 ("" (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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Zeroless? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (Div_inclusion 0
  (Div_inclusion-1 nil 3318336029
   ("" (skeep)
    (("" (expand "Div")
      (("" (case-replace "ub(Y) /= 0 AND lb(Y) /= 0")
        (("1" (flatten)
          (("1" (case "x/y = x*(1/y)")
            (("1" (replaces -1)
              (("1" (rewrite "Mult_inclusion")
                (("1" (hide 4)
                  (("1" (grind)
                    (("1" (cross-mult) nil nil)
                     ("2" (cross-mult) nil nil)
                     ("3" (cross-mult) nil nil)
                     ("4" (cross-mult) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil)
         ("2" (replace 1) (("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((Div const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (div_mult_neg_le1 formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (times_div2 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals 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)
    (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)
    (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)
    (|##| const-decl "bool" interval nil)
    (Zeroless? const-decl "bool" interval nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (Mult_inclusion formula-decl nil interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (Union_inclusion 0
  (Union_inclusion-1 nil 3318336071 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (|##| const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Union const-decl "Interval" interval nil))
   shostak))
 (Reunion 0
  (Reunion-1 nil 3318336078 ("" (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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (|##| const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Union const-decl "Interval" interval nil)
    (<< const-decl "bool" interval nil)
    (Overlap? const-decl "bool" interval nil))
   shostak))
 (Sigma_TCC1 0
  (Sigma_TCC1-1 nil 3318333335 ("" (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (Sigma_TCC2 0
  (Sigma_TCC2-1 nil 3318333335 ("" (termination-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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
 (Sigma_inclusion_TCC1 0
  (Sigma_inclusion_TCC1-1 nil 3391527110 ("" (subtype-tcc) nil nil) nil
   nil))
 (Sigma_inclusion_TCC2 0
  (Sigma_inclusion_TCC2-1 nil 3391527110 ("" (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)
    (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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil))
   nil))
 (Sigma_inclusion 0
  (Sigma_inclusion-2 nil 3318336332
   ("" (skolem 1 ("F" "f" _ "n"))
    ((""
      (case "FORALL (m: nat):
                             (FORALL (k: subrange(n, m)): f(k) ## F(k)) IMPLIES
                              sigma(n, m, f) ## Sigma(n, m, F)")
      (("1" (skeep)
        (("1" (case "i < 0")
          (("1" (hide -2 -3)
            (("1" (expand* "sigma" "Sigma")
              (("1" (assert) (("1" (rewrite "r2i_inclusion") nil nil))
                nil))
              nil))
            nil)
           ("2" (inst -1 "i")
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (induct "m")
          (("1" (flatten)
            (("1" (case "n > 0")
              (("1" (grind) nil nil)
               ("2" (inst -1 "n")
                (("1" (grind) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil)
           ("2" (skeep)
            (("2" (expand "Sigma" 1)
              (("2" (expand "sigma" 1)
                (("2" (lift-if)
                  (("2" (rewrite "r2i_inclusion")
                    (("2" (split 1)
                      (("1" (propax) nil nil)
                       ("2" (flatten)
                        (("2" (rewrite "Add_inclusion")
                          (("1" (inst -2 "1+j") nil nil)
                           ("2" (skeep 4) (("2" (inst -1 "k") nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Sigma def-decl "Interval" interval nil)
    (sigma def-decl "real" sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (|##| const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (subrange type-eq-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (< const-decl "bool" reals nil)
    (r2i_inclusion formula-decl nil interval 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)
    (r2i_Proper application-judgement "ProperInterval" interval nil)
    (i skolem-const-decl "int" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pred type-eq-decl nil defined_types nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (> const-decl "bool" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    ([\|\|] const-decl "Interval" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil)
    (n skolem-const-decl "nat" interval nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (Add_inclusion formula-decl nil interval nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (Add_fundamental 0
  (Add_fundamental-1 nil 3545739791 ("" (grind) nil nil)
   ((real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil))
   shostak))
 (Sub_fundamental 0
  (Sub_fundamental-1 nil 3545739796 ("" (grind) nil nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Sub const-decl "Interval" interval nil))
   shostak))
 (Abs_fundamental 0
  (Abs_fundamental-1 nil 3545739801 ("" (grind) 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (Proper? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (Abs const-decl "(NonNeg?)" interval nil))
   shostak))
 (Neg_fundamental 0
  (Neg_fundamental-1 nil 3545739806 ("" (grind) nil nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil))
   shostak))
 (pXp_fundamental 0
  (pXp_fundamental-1 nil 3545739812
   ("" (grind)
    (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)) nil)
   ((le_times_le_pos formula-decl nil 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (Mult const-decl "Interval" interval nil)
    (mXm const-decl "Interval" interval 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)
    (mXn const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (pXp const-decl "Interval" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (<< const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (Proper? const-decl "bool" interval nil))
   shostak))
 (pXpm_fundamental 0
  (pXpm_fundamental-1 nil 3545739862
   ("" (skeep)
    (("" (grind)
      (("1" (grind-reals) nil nil)
       ("2" (case "lb(X1) * lb(Y1) >= 0")
        (("1" (case "ub(X) * lb(Y) <= 0")
          (("1" (assert) nil nil)
           ("2" (hide -1 2) (("2" (grind-reals) nil nil)) nil))
          nil)
         ("2" (hide 2) (("2" (grind-reals) nil nil)) nil))
        nil))
      nil))
    nil)
   ((Proper? const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (pos_times_ge formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (neg_times_le formula-decl nil real_props nil)
    (Interval type-eq-decl nil interval nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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))
   shostak))
 (pXmm_fundamental 0
  (pXmm_fundamental-1 nil 3545739892
   ("" (skeep)
    (("" (grind)
      (("1" (grind-reals) nil nil)
       ("2" (mult-by -8 "lb(Y)" -)
        (("2" (case "ub(X1) * lb(Y) <= ub(X1) * lb(Y1)")
          (("1" (assert) nil nil)
           ("2" (hide -1 2) (("2" (grind-reals) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((Proper? const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (both_sides_times_pos_le2 formula-decl nil real_props nil)
    (Interval type-eq-decl nil interval nil)
    (nonpos_real nonempty-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)
    (both_sides_times_neg_le1_imp formula-decl nil extra_real_props
     nil))
   shostak))
 (pX_fundamental 0
  (pX_fundamental-3 nil 3579650676
   ("" (skeep)
    (("" (case "Ge(Y,0)")
      (("1" (rewrite "pXp_fundamental") nil nil)
       ("2" (case "Le(Y,0)")
        (("1" (rewrite "Mult_Neg_right")
          (("1" (lemma "Mult_Neg_right")
            (("1" (inst -1 "X" "Y")
              (("1" (replaces -1)
                (("1" (rewrite "Neg_fundamental")
                  (("1" (hide 2 3)
                    (("1" (rewrite "pXp_fundamental")
                      (("1" (hide 2) (("1" (grind) nil nil)) nil)
                       ("2" (hide 2) (("2" (grind) nil nil)) nil)
                       ("3" (hide 2) (("3" (grind) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case "Ge(Y1,0)")
          (("1" (rewrite "pXpm_fundamental")
            (("1" (hide 4) (("1" (grind) nil nil)) nil)) nil)
           ("2" (case "Le(Y1,0)")
            (("1" (rewrite "Mult_Neg_right")
              (("1" (lemma "Mult_Neg_right")
                (("1" (inst -1 "X" "Y")
                  (("1" (replaces -1)
                    (("1" (rewrite "Neg_fundamental")
                      (("1" (hide 5)
                        (("1" (rewrite "pXpm_fundamental")
                          (("1" (hide 2) (("1" (grind) nil nil)) nil)
                           ("2" (hide 2) (("2" (grind) nil nil)) nil)
                           ("3" (hide 2) (("3" (grind) nil nil)) nil)
                           ("4" (hide 2) (("4" (grind) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (rewrite "pXmm_fundamental")
              (("1" (hide 6) (("1" (grind) nil nil)) nil)
               ("2" (hide 6) (("2" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Ge const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (pXp_fundamental formula-decl nil interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pXpm_fundamental formula-decl nil interval nil)
    (pXmm_fundamental formula-decl nil interval nil)
    (Mult_Neg_right formula-decl nil interval nil)
    (Neg const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (Neg_fundamental formula-decl nil interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    (Le const-decl "bool" interval nil))
   nil))
 (nX_fundamental 0
  (nX_fundamental-1 nil 3545740595
   ("" (skeep)
    (("" (rewrite "Mult_Neg_left")
      (("" (lemma "Mult_Neg_left")
        (("" (inst -1 "X" "Y")
          (("" (replaces -1)
            (("" (rewrite "Neg_fundamental")
              (("" (hide 2)
                (("" (rewrite "pX_fundamental")
                  (("1" (hide 2) (("1" (grind) nil nil)) nil)
                   ("2" (hide 2) (("2" (grind) nil nil)) nil)
                   ("3" (hide 2) (("3" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Mult_Neg_left formula-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Neg_fundamental formula-decl nil interval nil)
    (Mult const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (pX_fundamental formula-decl nil interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Ge const-decl "bool" interval nil)
    (Le const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil))
   nil))
 (pmXpm_fundamental 0
  (pmXpm_fundamental-1 nil 3545740621
   ("" (skeep)
    (("" (grind)
      (("1" (grind-reals) nil nil)
       ("2" (flip-ineq 1)
        (("2" (swap-rel -1)
          (("2" (case "ub(X1) * ub(Y1) <= ub(X) * ub(Y)")
            (("1" (assert) nil nil)
             ("2" (hide -1 2) (("2" (grind-reals) nil nil)) nil))
            nil))
          nil))
        nil)
       ("3" (case "lb(X1) * lb(Y1) >= 0")
        (("1" (case "ub(X) * lb(Y) <= 0")
          (("1" (assert) nil nil)
           ("2" (hide -1 2) (("2" (grind-reals) nil nil)) nil))
          nil)
         ("2" (hide 2) (("2" (grind-reals) nil nil)) nil))
        nil)
       ("4" (case "lb(X1) * lb(Y1) >= 0")
        (("1" (case "lb(X) * ub(Y) <= 0")
          (("1" (assert) nil nil)
           ("2" (hide -1 2 3) (("2" (grind-reals) nil nil)) nil))
          nil)
         ("2" (hide 2 3) (("2" (grind-reals) nil nil)) nil))
        nil))
      nil))
    nil)
   ((Proper? const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval 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)
    (real_times_real_is_real application-judgement "real" 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)
    (le_times_le_pos formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Interval type-eq-decl nil interval nil)
    (pos_times_ge formula-decl nil real_props nil)
    (neg_times_le formula-decl nil real_props nil))
   nil))
 (pmXmm_fundamental 0
  (pmXmm_fundamental-2 nil 3579650852
   ("" (skeep)
    (("" (lemma "Member_Incl")
      (("" (inst -1 "Mult(X1,Y1)" "Mult(X,Y)")
        (("" (assert)
          (("" (hide 2)
            (("" (split 1)
              (("1" (grind) (("1" (grind-reals) nil nil)) nil)
               ("2" (case-replace "Mult(X1,Y1) = pXm(X1,Y1)")
                (("1" (hide -1)
                  (("1" (skeep)
                    (("1"
                      (case "EXISTS(x1,y1:real):x = x1*y1 AND x1 ## X AND y1 ## Y")
                      (("1" (skeep -1)
                        (("1" (replaces -1)
                          (("1" (rewrite "Mult_inclusion") nil nil))
                          nil))
                        nil)
                       ("2" (hide 2)
                        (("2" (expand "pXm")
                          (("2" (expand "[||]")
                            (("2" (case-replace "ub(X1) = 0")
                              (("1" (grind) nil nil)
                               ("2"
                                (inst 2 "ub(X1)" "x/ub(X1)")
                                (("1"
                                  (grind)
                                  (("1"
                                    (case "x/ub(X1) <= ub(Y1)")
                                    (("1" (assert) nil nil)
                                     ("2" (grind-reals) nil nil))
                                    nil)
                                   ("2"
                                    (case "x/ub(X1) >= lb(Y1)")
                                    (("1" (assert) nil nil)
                                     ("2" (grind-reals) nil nil))
                                    nil))
                                  nil)
                                 ("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2) (("2" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Member_Incl formula-decl nil interval nil)
    (both_sides_times_pos_le2 formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (Proper? const-decl "bool" interval nil)
    (pXm const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (pXp const-decl "Interval" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Mult_inclusion formula-decl nil interval nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (>= const-decl "bool" reals nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (X1 skolem-const-decl "Interval" interval nil)
    (/= const-decl "boolean" notequal nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Mult const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil))
   nil))
 (mmXmm_fundamental 0
  (mmXmm_fundamental-4 nil 3579650959
   ("" (skeep)
    (("" (expand "Zeroin?")
      (("" (flatten)
        (("" (lemma "Member_Incl")
          (("" (inst -1 "Mult(X1,Y1)" "Mult(X,Y)")
            (("" (assert)
              (("" (hide 2)
                (("" (split 1)
                  (("1" (grind)
                    (("1" (grind-reals) nil nil)
                     ("2" (grind-reals) nil nil)
                     ("3" (grind-reals) nil nil)
                     ("4" (grind-reals) nil nil))
                    nil)
                   ("2" (case-replace "Mult(X1,Y1) = mXm(X1,Y1)")
                    (("1" (hide -1)
                      (("1" (skeep)
                        (("1"
                          (case "EXISTS(x1,y1:real):x = x1*y1 AND x1 ## X AND y1 ## Y")
                          (("1" (skeep -1)
                            (("1" (replaces -1)
                              (("1"
                                (rewrite "Mult_inclusion")
                                nil
                                nil))
                              nil))
                            nil)
                           ("2" (hide 2)
                            (("2" (expand "##" -1)
                              (("2"
                                (flatten)
                                (("2"
                                  (expand "mXm")
                                  (("2"
                                    (expand "[||]")
                                    (("2"
                                      (rewrite "min_le")
                                      (("2"
                                        (rewrite "le_max")
                                        (("2"
                                          (ground)
                                          (("1"
                                            (inst
                                             1
                                             "lb(X1)"
                                             "x/lb(X1)")
                                            (("1"
                                              (grind)
                                              (("1"
                                                (case
                                                 "x/lb(X1) <= ub(Y1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (grind-reals)
                                                  nil
                                                  nil))
                                                nil)
                                               ("2"
                                                (case
                                                 "x/lb(X1) >= lb(Y1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (hide 2)
                                                  (("2"
                                                    (grind-reals)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (inst
                                             1
                                             "x/ub(Y1)"
                                             "ub(Y1)")
                                            (("2"
                                              (grind)
                                              (("1"
                                                (case
                                                 "x/ub(Y1) <= ub(X1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (grind-reals)
                                                  nil
                                                  nil))
                                                nil)
                                               ("2"
                                                (case
                                                 "x/ub(Y1) >= lb(X1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (grind-reals)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("3"
                                            (inst
                                             1
                                             "x/lb(Y1)"
                                             "lb(Y1)")
                                            (("3"
                                              (grind)
                                              (("1"
                                                (case
                                                 "x/lb(Y1) <= ub(X1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (grind-reals)
                                                  nil
                                                  nil))
                                                nil)
                                               ("2"
                                                (case
                                                 "x/lb(Y1) >= lb(X1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (grind-reals)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("4"
                                            (inst
                                             1
                                             "ub(X1)"
                                             "x/ub(X1)")
                                            (("4"
                                              (grind)
                                              (("1"
                                                (case
                                                 "x/ub(X1) <= ub(Y1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (grind-reals)
                                                  nil
                                                  nil))
                                                nil)
                                               ("2"
                                                (case
                                                 "x/ub(X1) >= lb(Y1)")
                                                (("1" (assert) nil nil)
                                                 ("2"
                                                  (grind-reals)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide 2) (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Zeroin? const-decl "bool" interval nil)
    (Member_Incl formula-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (both_sides_times_neg_le2 formula-decl nil real_props nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (both_sides_times_neg_le1 formula-decl nil real_props nil)
    (both_sides_times_pos_le2 formula-decl nil real_props 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)
    (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)
    (Ge const-decl "bool" interval nil)
    (Le const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (mXm const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Mult_inclusion formula-decl nil interval nil)
    (min_le formula-decl nil real_defs nil)
    (div_mult_neg_le1 formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (div_mult_neg_ge1 formula-decl nil real_props nil)
    (>= const-decl "bool" reals nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (le_max formula-decl nil real_defs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Mult const-decl "Interval" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil))
   nil))
 (mX_fundamental 0
  (mX_fundamental-3 nil 3579651173
   ("" (skeep)
    (("" (case "Ge(Y,0)")
      (("1" (rewrite "Mult_comm")
        (("1" (lemma "Mult_comm")
          (("1" (inst -1 "X" "Y")
            (("1" (replaces -1)
              (("1" (rewrite "pX_fundamental") nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (case "Le(Y,0)")
        (("1" (hide 1)
          (("1" (rewrite "Mult_comm")
            (("1" (lemma "Mult_comm")
              (("1" (inst -1 "X" "Y")
                (("1" (replaces -1)
                  (("1" (rewrite "nX_fundamental") nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case "Zeroin?(Y)")
          (("1" (hide 1 2)
            (("1" (case "Ge(X1,0) AND Ge(Y1,0)")
              (("1" (flatten)
                (("1" (rewrite "pmXpm_fundamental") nil nil)) nil)
               ("2" (case "Ge(X1,0) AND Le(Y1,0)")
                (("1" (hide 1)
                  (("1" (flatten)
                    (("1" (rewrite "Mult_Neg_right")
                      (("1" (lemma "Mult_Neg_right")
                        (("1" (inst -1 "X" "Y")
                          (("1" (replaces -1)
                            (("1" (rewrite "Neg_fundamental")
                              (("1"
                                (hide 2)
                                (("1"
                                  (rewrite "pmXpm_fundamental")
                                  (("1"
                                    (hide 2)
                                    (("1" (grind) nil nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2" (grind) nil nil))
                                    nil)
                                   ("3"
                                    (hide 2)
                                    (("3" (grind) nil nil))
                                    nil)
                                   ("4"
                                    (hide 2)
                                    (("4" (grind) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (case "Le(X1,0) AND Ge(Y1,0)")
                  (("1" (hide 1 2)
                    (("1" (flatten)
                      (("1" (rewrite "Mult_Neg_left")
                        (("1" (lemma "Mult_Neg_left")
                          (("1" (inst -1 "X" "Y")
                            (("1" (replaces -1)
                              (("1"
                                (rewrite "Neg_fundamental")
                                (("1"
                                  (hide 2)
                                  (("1"
                                    (rewrite "pmXpm_fundamental")
                                    (("1"
                                      (hide 2)
                                      (("1" (grind) nil nil))
                                      nil)
                                     ("2"
                                      (hide 2)
                                      (("2" (grind) nil nil))
                                      nil)
                                     ("3"
                                      (hide 2)
                                      (("3" (grind) nil nil))
                                      nil)
                                     ("4"
                                      (hide 2)
                                      (("4" (grind) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (case "Le(X1,0) AND Le(Y1,0)")
                    (("1" (hide 1 2 3)
                      (("1" (flatten)
                        (("1" (rewrite "Mult_Neg_Neg")
                          (("1" (lemma "Mult_Neg_Neg")
                            (("1" (inst -1 "X" "Y")
                              (("1"
                                (replaces -1)
                                (("1"
                                  (rewrite "pmXpm_fundamental")
                                  (("1"
                                    (hide 2)
                                    (("1" (grind) nil nil))
                                    nil)
                                   ("2"
                                    (hide 2)
                                    (("2" (grind) nil nil))
                                    nil)
                                   ("3"
                                    (hide 2)
                                    (("3" (grind) nil nil))
                                    nil)
                                   ("4"
                                    (hide 2)
                                    (("4" (grind) nil nil))
                                    nil)
                                   ("5"
                                    (hide 2)
                                    (("5" (grind) nil nil))
                                    nil)
                                   ("6"
                                    (hide 2)
                                    (("6" (grind) nil nil))
                                    nil)
                                   ("7"
                                    (hide 2)
                                    (("7" (grind) nil nil))
                                    nil)
                                   ("8"
                                    (hide 2)
                                    (("8" (grind) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (case "Ge(X1,0) AND Zeroin?(Y1)")
                      (("1" (hide 1 2 3 4)
                        (("1" (flatten)
                          (("1" (rewrite "pmXmm_fundamental") nil nil))
                          nil))
                        nil)
                       ("2" (case "Le(X1,0) AND Zeroin?(Y1)")
                        (("1" (hide 1 2 3 4 5)
                          (("1" (flatten)
                            (("1" (rewrite "Mult_Neg_left")
                              (("1"
                                (lemma "Mult_Neg_left")
                                (("1"
                                  (inst -1 "X" "Y")
                                  (("1"
                                    (replaces -1)
                                    (("1"
                                      (rewrite "Neg_fundamental")
                                      (("1"
                                        (hide 2)
                                        (("1"
                                          (rewrite "pmXmm_fundamental")
                                          (("1"
                                            (hide 2)
                                            (("1" (grind) nil nil))
                                            nil)
                                           ("2"
                                            (hide 2)
                                            (("2" (grind) nil nil))
                                            nil)
                                           ("3"
                                            (hide 2)
                                            (("3" (grind) nil nil))
                                            nil)
                                           ("4" (grind) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (case "Ge(Y1,0) AND Zeroin?(X1)")
                          (("1" (hide 1 2 3 4 5 6)
                            (("1" (flatten)
                              (("1"
                                (rewrite "Mult_comm")
                                (("1"
                                  (lemma "Mult_comm")
                                  (("1"
                                    (inst -1 "X" "Y")
                                    (("1"
                                      (replaces -1)
                                      (("1"
                                        (rewrite "pmXmm_fundamental")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (case "Le(Y1,0) AND Zeroin?(X1)")
                            (("1" (hide 1 2 3 4 5 6 7)
                              (("1"
                                (flatten)
                                (("1"
                                  (rewrite "Mult_comm")
                                  (("1"
                                    (lemma "Mult_comm")
                                    (("1"
                                      (inst -1 "X" "Y")
                                      (("1"
                                        (replaces -1)
                                        (("1"
                                          (rewrite "Mult_Neg_left")
                                          (("1"
                                            (lemma "Mult_Neg_left")
                                            (("1"
                                              (inst -1 "Y" "X")
                                              (("1"
                                                (replaces -1)
                                                (("1"
                                                  (rewrite
                                                   "Neg_fundamental")
                                                  (("1"
                                                    (hide 2)
                                                    (("1"
                                                      (rewrite
                                                       "pmXmm_fundamental")
                                                      (("1"
                                                        (hide 2)
                                                        (("1"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide 2)
                                                        (("2"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("3"
                                                        (hide 2)
                                                        (("3"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("4"
                                                        (hide 2)
                                                        (("4"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (case "Zeroin?(X1) AND Zeroin?(Y1)")
                              (("1"
                                (hide 1 2 3 4 5 6 7 8)
                                (("1"
                                  (flatten)
                                  (("1"
                                    (rewrite "mmXmm_fundamental")
                                    nil
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (lemma "Trichotomy")
                                (("2"
                                  (inst-cp -1 "X1")
                                  (("2"
                                    (inst -1 "Y1")
                                    (("2"
                                      (assert)
                                      (("2" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 4) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((Ge const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (pX_fundamental formula-decl nil interval nil)
    (Mult_comm formula-decl nil interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pmXpm_fundamental formula-decl nil interval nil)
    (Mult_Neg_left formula-decl nil interval nil)
    (pmXmm_fundamental formula-decl nil interval nil)
    (mmXmm_fundamental formula-decl nil interval nil)
    (Trichotomy formula-decl nil interval nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (mXm const-decl "Interval" interval 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)
    (mXn const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Mult_Neg_Neg formula-decl nil interval nil)
    (Mult_Neg_right formula-decl nil interval nil)
    (Neg const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (Neg_fundamental formula-decl nil interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (<< const-decl "bool" interval nil)
    (nX_fundamental formula-decl nil interval nil)
    (Le const-decl "bool" interval nil))
   nil))
 (Mult_fundamental 0
  (Mult_fundamental-3 nil 3579693747
   ("" (skeep)
    (("" (case "Ge(X,0)")
      (("1" (rewrite "pX_fundamental") nil nil)
       ("2" (case "Le(X,0)")
        (("1" (rewrite "nX_fundamental") nil nil)
         ("2" (case "Zeroin?(X)")
          (("1" (rewrite "mX_fundamental") nil nil)
           ("2" (hide -2 -4 4) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((Ge const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (pX_fundamental formula-decl nil interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (mX_fundamental formula-decl nil interval 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)
    (Proper? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (nX_fundamental formula-decl nil interval nil)
    (Le const-decl "bool" interval nil))
   nil)
  (Mult_fundamental-2 nil 3545749620
   ("" (skeep)
    (("" (case "X>=0")
      (("1" (rewrite "pX_fundamental") nil nil)
       ("2" (case "X<=0")
        (("1" (rewrite "nX_fundamental") nil nil)
         ("2" (case "Zeroin?(X)")
          (("1" (rewrite "mX_fundamental") nil nil)
           ("2" (hide -2 -4 4) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   nil nil)
  (Mult_fundamental-1 nil 3545749608
   ("" (skeep)
    (("" (case "Y >= 0")
      (("1" (rewrite "Mult_comm")
        (("1" (lemma "Mult_comm")
          (("1" (inst -1 "X" "Y")
            (("1" (replaces -1)
              (("1" (rewrite "pX_fundamental") nil)))))))))
       ("2" (case "Y<=0")
        (("1" (hide 1)
          (("1" (rewrite "Mult_comm")
            (("1" (lemma "Mult_comm")
              (("1" (inst -1 "X" "Y")
                (("1" (replaces -1)
                  (("1" (rewrite "nX_fundamental") nil)))))))))))
         ("2" (case "Zeroin?(Y)")
          (("1" (flatten)
            (("1" (hide 1 2)
              (("1" (case "X1 >= 0 AND Y1 >= 0")
                (("1" (flatten)
                  (("1" (rewrite "pmXpm_fundamental") nil)))
                 ("2" (case "X1 >= 0 AND Y1 <= 0")
                  (("1" (hide 1)
                    (("1" (flatten)
                      (("1" (rewrite "Mult_neg_right")
                        (("1" (lemma "Mult_neg_right")
                          (("1" (inst -1 "X" "Y")
                            (("1" (replaces -1)
                              (("1"
                                (rewrite "Neg_fundamental")
                                (("1"
                                  (hide 2)
                                  (("1"
                                    (rewrite "pmXpm_fundamental")
                                    (("1" (hide 2) (("1" (grind) nil)))
                                     ("2" (hide 2) (("2" (grind) nil)))
                                     ("3" (hide 2) (("3" (grind) nil)))
                                     ("4" (hide 2) (("4" (grind) nil)))
                                     ("5"
                                      (hide 2)
                                      (("5"
                                        (grind)
                                        nil)))))))))))))))))))))
                   ("2" (case "X1 <= 0 AND Y1 >= 0")
                    (("1" (hide 1 2)
                      (("1" (flatten)
                        (("1" (rewrite "Mult_neg_left")
                          (("1" (lemma "Mult_neg_left")
                            (("1" (inst -1 "X" "Y")
                              (("1"
                                (replaces -1)
                                (("1"
                                  (rewrite "Neg_fundamental")
                                  (("1"
                                    (hide 2)
                                    (("1"
                                      (rewrite "pmXpm_fundamental")
                                      (("1"
                                        (hide 2)
                                        (("1" (grind) nil)))
                                       ("2"
                                        (hide 2)
                                        (("2" (grind) nil)))
                                       ("3"
                                        (hide 2)
                                        (("3" (grind) nil)))
                                       ("4"
                                        (hide 2)
                                        (("4" (grind) nil)))
                                       ("5"
                                        (hide 2)
                                        (("5"
                                          (grind)
                                          nil)))))))))))))))))))))
                     ("2" (case "X1 <= 0 AND Y1 <= 0")
                      (("1" (hide 1 2 3)
                        (("1" (flatten)
                          (("1" (rewrite "Mult_neg_neg")
                            (("1" (lemma "Mult_neg_neg")
                              (("1"
                                (inst -1 "X" "Y")
                                (("1"
                                  (replaces -1)
                                  (("1"
                                    (rewrite "pmXpm_fundamental")
                                    (("1" (hide 2) (("1" (grind) nil)))
                                     ("2" (hide 2) (("2" (grind) nil)))
                                     ("3" (hide 2) (("3" (grind) nil)))
                                     ("4" (hide 2) (("4" (grind) nil)))
                                     ("5" (hide 2) (("5" (grind) nil)))
                                     ("6" (hide 2) (("6" (grind) nil)))
                                     ("7" (hide 2) (("7" (grind) nil)))
                                     ("8" (hide 2) (("8" (grind) nil)))
                                     ("9" (hide 2) (("9" (grind) nil)))
                                     ("10"
                                      (hide 2)
                                      (("10"
                                        (grind)
                                        nil)))))))))))))))))
                       ("2" (case "X1 >= 0 AND Zeroin?(Y1)")
                        (("1" (hide 1 2 3 4)
                          (("1" (flatten)
                            (("1" (rewrite "pmXmm_fundamental")
                              nil)))))
                         ("2" (case "X1 <= 0 AND Zeroin?(Y1)")
                          (("1" (hide 1 2 3 4 5)
                            (("1" (flatten)
                              (("1"
                                (rewrite "Mult_neg_left")
                                (("1"
                                  (lemma "Mult_neg_left")
                                  (("1"
                                    (inst -1 "X" "Y")
                                    (("1"
                                      (replaces -1)
                                      (("1"
                                        (rewrite "Neg_fundamental")
                                        (("1"
                                          (hide 2)
                                          (("1"
                                            (rewrite
                                             "pmXmm_fundamental")
                                            (("1"
                                              (hide 2)
                                              (("1" (grind) nil)))
                                             ("2"
                                              (hide 2)
                                              (("2" (grind) nil)))
                                             ("3"
                                              (hide 2)
                                              (("3" (grind) nil)))
                                             ("4"
                                              (hide 2)
                                              (("4" (grind) nil)))
                                             ("5"
                                              (hide 2)
                                              (("5"
                                                (grind)
                                                nil)))))))))))))))))))))
                           ("2" (case "Y1 >= 0 AND Zeroin?(X1)")
                            (("1" (hide 1 2 3 4 5 6)
                              (("1"
                                (flatten)
                                (("1"
                                  (rewrite "Mult_comm")
                                  (("1"
                                    (lemma "Mult_comm")
                                    (("1"
                                      (inst -1 "X" "Y")
                                      (("1"
                                        (replaces -1)
                                        (("1"
                                          (rewrite "pmXmm_fundamental")
                                          nil)))))))))))))
                             ("2" (case "Y1 <= 0 AND Zeroin?(X1)")
                              (("1"
                                (hide 1 2 3 4 5 6 7)
                                (("1"
                                  (flatten)
                                  (("1"
                                    (rewrite "Mult_comm")
                                    (("1"
                                      (lemma "Mult_comm")
                                      (("1"
                                        (inst -1 "X" "Y")
                                        (("1"
                                          (replaces -1)
                                          (("1"
                                            (rewrite "Mult_neg_left")
                                            (("1"
                                              (lemma "Mult_neg_left")
                                              (("1"
                                                (inst -1 "Y" "X")
                                                (("1"
                                                  (replaces -1)
                                                  (("1"
                                                    (rewrite
                                                     "Neg_fundamental")
                                                    (("1"
                                                      (hide 2)
                                                      (("1"
                                                        (rewrite
                                                         "pmXmm_fundamental")
                                                        (("1"
                                                          (hide 2)
                                                          (("1"
                                                            (grind)
                                                            nil)))
                                                         ("2"
                                                          (hide 2)
                                                          (("2"
                                                            (grind)
                                                            nil)))
                                                         ("3"
                                                          (hide 2)
                                                          (("3"
                                                            (grind)
                                                            nil)))
                                                         ("4"
                                                          (hide 2)
                                                          (("4"
                                                            (grind)
                                                            nil)))
                                                         ("5"
                                                          (hide 2)
                                                          (("5"
                                                            (grind)
                                                            nil)))))))))))))))))))))))))))))
                               ("2"
                                (case "Zeroin?(X1) AND Zeroin?(Y1)")
                                (("1"
                                  (hide 1 2 3 4 5 6 7 8)
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (rewrite "mmXmm_fundamental")
                                      nil)))))
                                 ("2"
                                  (hide 10)
                                  (("2"
                                    (grind)
                                    nil)))))))))))))))))))))))))
           ("2" (hide 4) (("2" (grind) nil))))))))))
    nil)
   nil nil))
 (Sq_p_fundamental 0
  (Sq_p_fundamental-1 nil 3545819118
   ("" (grind)
    (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)) nil)
   ((le_times_le_pos formula-decl nil real_props nil)
    (real_times_real_is_real application-judgement "real" 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)
    (Sq const-decl "(NonNeg?)" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Le const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Ge const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Sq_pm_fundamental 0
  (Sq_pm_fundamental-1 nil 3545819157
   ("" (skeep)
    (("" (grind)
      (("1" (grind-reals) nil nil)
       ("2" (flip-ineq 1)
        (("2" (swap-rel -1)
          (("2" (case "ub(X1) * ub(X1) <= ub(X) * ub(X)")
            (("1" (assert) nil nil)
             ("2" (hide -1 2) (("2" (grind-reals) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Proper? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    ([\|\|] const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Sq const-decl "(NonNeg?)" interval 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)
    (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)
    (le_times_le_pos formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Interval type-eq-decl nil interval nil))
   shostak))
 (Sq_fundamental 0
  (Sq_fundamental-1 nil 3545818077
   ("" (skeep)
    (("" (case "Proper?(X)")
      (("1" (lemma "Trichotomy")
        (("1" (inst -1 "X")
          (("1" (assert)
            (("1" (split -1)
              (("1" (rewrite "Sq_p_fundamental") nil nil)
               ("2" (rewrite "Sq_Neg_eq")
                (("2" (lemma "Sq_Neg_eq")
                  (("2" (inst -1 "X")
                    (("2" (replaces -1)
                      (("2" (rewrite "Sq_p_fundamental")
                        (("1" (hide 2) (("1" (grind) nil nil)) nil)
                         ("2" (hide 2) (("2" (grind) nil nil)) nil)
                         ("3" (hide 2) (("3" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (lemma "Trichotomy")
                (("3" (inst -1 "X1")
                  (("3" (assert)
                    (("3" (split -1)
                      (("1" (rewrite "Sq_pm_fundamental") nil nil)
                       ("2" (rewrite "Sq_Neg_eq")
                        (("2" (lemma "Sq_Neg_eq")
                          (("2" (inst -1 "X")
                            (("2" (replaces -1)
                              (("2"
                                (rewrite "Sq_pm_fundamental")
                                (("1"
                                  (hide 2)
                                  (("1" (grind) nil nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2" (grind) nil nil))
                                  nil)
                                 ("3"
                                  (hide 2)
                                  (("3" (grind) nil nil))
                                  nil)
                                 ("4"
                                  (hide 2)
                                  (("4" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (grind)
                        (("1" (grind-reals) nil nil)
                         ("2" (flip-ineq 1)
                          (("2" (swap-rel -1)
                            (("2"
                              (case "ub(X1) * ub(X1) <= ub(X) * ub(X)")
                              (("1" (assert) nil nil)
                               ("2"
                                (hide -1 2)
                                (("2" (grind-reals) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("3" (case "lb(X1) * lb(X1) <= lb(X) * lb(X)")
                          (("1" (assert) nil nil)
                           ("2" (grind-reals) nil nil))
                          nil)
                         ("4" (grind-reals) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2) (("2" (grind) nil nil)) nil))
      nil))
    nil)
   ((Proper? const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Sq_p_fundamental formula-decl nil interval nil)
    (Ge const-decl "bool" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Le const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Sq_Neg_eq formula-decl nil interval nil)
    (Sq_pm_fundamental formula-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Zeroin? const-decl "bool" interval nil)
    (le_times_le_neg formula-decl nil real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" 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)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (le_times_le_pos formula-decl nil real_props 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)
    (Sq const-decl "(NonNeg?)" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Trichotomy formula-decl nil interval nil))
   shostak))
 (Div_fundamental 0
  (Div_fundamental-1 nil 3545820842
   ("" (skeep)
    (("" (expand "Div")
      ((""
        (case "ub(Y1) /= 0 AND lb(Y1) /= 0 AND ub(Y) /= 0 AND lb(Y) /= 0")
        (("1" (flatten)
          (("1" (assert)
            (("1" (rewrite "Mult_fundamental")
              (("1" (hide 6)
                (("1" (grind)
                  (("1" (grind-reals) nil nil)
                   ("2" (grind-reals) nil nil))
                  nil))
                nil)
               ("2" (hide 6)
                (("2" (grind)
                  (("1" (grind-reals) nil nil)
                   ("2" (grind-reals) nil nil)
                   ("3" (grind-reals) nil nil)
                   ("4" (grind-reals) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2) (("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((Div const-decl "Interval" interval nil)
    (Mult_fundamental formula-decl nil interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (Zeroless? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (Proper? const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_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)
    (le_div_le_pos formula-decl nil real_props nil)
    (both_sides_div_neg_le2 formula-decl nil real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (/= const-decl "boolean" notequal nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil))
   shostak))
 (Pow_p_fundamental 0
  (Pow_p_fundamental-2 nil 3579693818
   ("" (skeep)
    (("" (expand "Pow")
      (("" (assert)
        (("" (split -4)
          (("1" (assert)
            (("1" (expand "<<")
              (("1" (expand "[||]")
                (("1" (flatten)
                  (("1" (rewrite "pow_incr_odd")
                    (("1" (rewrite "pow_incr_odd") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert)
            (("2" (case "Ge(X1,0)")
              (("1" (assert)
                (("1" (expand "<<")
                  (("1" (expand "[||]")
                    (("1" (expand "Ge")
                      (("1" (flatten)
                        (("1" (rewrite "pow_incr_pos")
                          (("1" (rewrite "pow_incr_pos") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2) (("2" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Pow const-decl "Interval" interval nil)
    (<< const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval 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)
    (pow_incr_odd formula-decl nil interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (pow_incr_pos formula-decl nil interval 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)
    (Proper? const-decl "bool" interval nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (Pow_pm_fundamental 0
  (Pow_pm_fundamental-2 nil 3579693886
   ("" (skeep)
    (("" (expand "Pow")
      (("" (assert)
        (("" (lemma "even_or_odd")
          (("" (inst?)
            (("" (assert)
              (("" (case "NOT Ge(X,0) AND NOT Le(X,0)")
                (("1" (flatten)
                  (("1" (assert)
                    (("1" (expand "<<")
                      (("1" (expand "[||]")
                        (("1" (flatten)
                          (("1" (lemma "pow_even_pos")
                            (("1" (inst?)
                              (("1"
                                (assert)
                                (("1"
                                  (expand "max")
                                  (("1"
                                    (lift-if)
                                    (("1"
                                      (expand "Ge")
                                      (("1"
                                        (expand "Le")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (split 4)
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (rewrite
                                                 "pow_incr_pos")
                                                nil
                                                nil))
                                              nil)
                                             ("2"
                                              (flatten)
                                              (("2"
                                                (expand "Zeroin?")
                                                (("2"
                                                  (flatten)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (hide 3 4)
                                                      (("2"
                                                        (case
                                                         "ub(X1)^n <= ub(X)^n")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil)
                                                         ("2"
                                                          (rewrite
                                                           "pow_incr_pos")
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide -4 2 3) (("2" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Pow const-decl "Interval" interval nil)
    (even_or_odd formula-decl nil naturalnumbers nil)
    (Proper? const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (Zeroin? const-decl "bool" interval nil)
    (pow_incr_pos formula-decl nil interval 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)
    (pow_even_pos formula-decl nil interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (Pow_m_fundamental 0
  (Pow_m_fundamental-2 nil 3579693961
   ("" (skeep)
    (("" (case "Ge(X1,0)")
      (("1" (rewrite "Pow_pm_fundamental") nil nil)
       ("2" (case "Le(X1,0)")
        (("1" (rewrite "Pow_Neg_even")
          (("1" (lemma "Pow_Neg_even")
            (("1" (inst -1 "X" "n")
              (("1" (assert)
                (("1" (split -1)
                  (("1" (replaces -1)
                    (("1" (rewrite "Pow_pm_fundamental")
                      (("1" (hide -5 3) (("1" (grind) nil nil)) nil)
                       ("2" (hide -5 3) (("2" (grind) nil nil)) nil)
                       ("3" (hide -5 3) (("3" (grind) nil nil)) nil)
                       ("4" (hide -5 3) (("4" (grind) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (hide -5 3) (("2" (grind) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case "Zeroin?(X1)")
          (("1" (expand "Pow")
            (("1" (assert)
              (("1" (lemma "even_or_odd")
                (("1" (inst? -)
                  (("1" (assert)
                    (("1" (case "NOT Ge(X,0) AND NOT Le(X,0)")
                      (("1" (flatten)
                        (("1" (assert)
                          (("1" (expand "<<")
                            (("1" (expand "[||]")
                              (("1"
                                (flatten)
                                (("1"
                                  (rewrite "max_le")
                                  (("1"
                                    (rewrite "le_max")
                                    (("1"
                                      (rewrite "le_max")
                                      (("1"
                                        (expand "Zeroin?")
                                        (("1"
                                          (expand "Ge")
                                          (("1"
                                            (expand "Le")
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (split 6)
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (lemma
                                                     "pow_decr_even")
                                                    (("1"
                                                      (inst
                                                       -1
                                                       "n"
                                                       "lb(X1)"
                                                       "lb(X)")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (flatten)
                                                  (("2"
                                                    (lemma
                                                     "pow_incr_pos")
                                                    (("2"
                                                      (inst
                                                       -1
                                                       "n"
                                                       "ub(X1)"
                                                       "ub(X)")
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide -5 2 5) (("2" (grind) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide (-4 4)) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((Ge const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil 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)
    (Pow_pm_fundamental formula-decl nil interval nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (max_le formula-decl nil real_defs nil)
    (pow_incr_pos formula-decl nil interval nil)
    (pow_decr_even formula-decl nil interval nil)
    (le_max formula-decl nil real_defs nil)
    (even_or_odd formula-decl nil naturalnumbers nil)
    (Pow const-decl "Interval" interval nil)
    (Pow_Neg_even formula-decl nil interval nil)
    (Neg const-decl "Interval" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (<< const-decl "bool" interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Le const-decl "bool" interval nil))
   nil))
 (Pow_fundamental 0
  (Pow_fundamental-2 nil 3579694094
   ("" (skeep)
    (("" (case "n=0")
      (("1" (expand "Pow") (("1" (assert) nil nil)) nil)
       ("2" (case "odd?(n) OR Ge(X,0)")
        (("1" (rewrite "Pow_p_fundamental") nil nil)
         ("2" (flatten)
          (("2" (lemma "even_or_odd")
            (("2" (inst?)
              (("2" (assert)
                (("2" (case "Le(X,0)")
                  (("1" (rewrite "Pow_Neg_even")
                    (("1" (lemma "Pow_Neg_even")
                      (("1" (inst -1 "X" "n")
                        (("1" (assert)
                          (("1" (split -1)
                            (("1" (replaces -1)
                              (("1"
                                (rewrite "Pow_p_fundamental")
                                (("1"
                                  (hide -2 2 4 5)
                                  (("1" (grind) nil nil))
                                  nil)
                                 ("2"
                                  (hide -2 2 4 5)
                                  (("2" (grind) nil nil))
                                  nil)
                                 ("3"
                                  (hide -2 2 4 5)
                                  (("3" (grind) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide -2 2 4 5)
                              (("2" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (case "Zeroin?(X)")
                    (("1" (lemma "Pow_m_fundamental")
                      (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
                     ("2" (hide -1 3 5 6) (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (Incl_reflx formula-decl nil interval nil)
    (r2i_Proper application-judgement "ProperInterval" interval nil)
    (Pow const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (<< const-decl "bool" interval nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (Proper? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Pow_Neg_even formula-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Pow_m_fundamental formula-decl nil interval nil)
    (Zeroin? const-decl "bool" interval nil)
    (even_or_odd formula-decl nil naturalnumbers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Pow_p_fundamental formula-decl nil interval nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (odd? const-decl "bool" integers nil)
    (Interval type-eq-decl nil interval nil)
    (Ge const-decl "bool" interval nil))
   nil)
  (Pow_fundamental-1 nil 3545821701
   ("" (skeep)
    (("" (case "n=0")
      (("1" (expand "Pow") (("1" (assert) nil nil)) nil)
       ("2" (case "odd?(n) OR X >= 0")
        (("1" (rewrite "Pow_p_fundamental") nil nil)
         ("2" (flatten)
          (("2" (lemma "even_or_odd")
            (("2" (inst?)
              (("2" (assert)
                (("2" (case "X <= 0")
                  (("1" (rewrite "Pow_Neg_even")
                    (("1" (lemma "Pow_Neg_even")
                      (("1" (inst -1 "X" "n")
                        (("1" (assert)
                          (("1" (split -1)
                            (("1" (replaces -1)
                              (("1"
                                (rewrite "Pow_p_fundamental")
                                (("1"
                                  (hide -2 2 4 5)
                                  (("1" (grind) nil nil))
                                  nil)
                                 ("2"
                                  (hide -2 2 4 5)
                                  (("2" (grind) nil nil))
                                  nil)
                                 ("3"
                                  (hide -2 2 4 5)
                                  (("3" (grind) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide -2 2 4 5)
                              (("2" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (case "Zeroin?(X)")
                    (("1" (lemma "Pow_m_fundamental")
                      (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
                     ("2" (hide -1 3 5 6) (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (Union_fundamental 0
  (Union_fundamental-1 nil 3546381205 ("" (grind) 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (<< const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Union const-decl "Interval" interval nil))
   shostak))
 (Mult_Strict_r2i 0
  (Mult_Strict_r2i-1 nil 3320581805
   ("" (skeep)
    (("" (grind)
      (("1" (grind-reals :theories "extra_tegies") nil nil)
       ("2" (grind-reals :theories "extra_tegies") nil nil)
       ("3" (grind-reals :theories "extra_tegies") nil nil)
       ("4" (grind-reals :theories "extra_tegies") nil nil)
       ("5" (grind-reals :theories "extra_tegies") nil nil)
       ("6" (grind-reals :theories "extra_tegies") nil nil)
       ("7" (grind-reals :theories "extra_tegies") nil nil)
       ("8" (grind-reals :theories "extra_tegies") nil nil))
      nil))
    nil)
   ((StrictInterval? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (r2i_Proper application-judgement "ProperInterval" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_times_lt_pos1 formula-decl nil real_props nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (neg_neg formula-decl nil extra_tegies nil)
    (neg_mult formula-decl nil extra_tegies nil)
    (both_sides_times_pos_lt2 formula-decl nil real_props nil)
    (lt_times_lt_neg1 formula-decl nil real_props nil)
    (mult_neg formula-decl nil extra_tegies nil)
    (both_sides_times_neg_lt2 formula-decl nil real_props nil))
   shostak))
 (Mult_r2i_Strict 0
  (Mult_r2i_Strict-1 nil 3320581969
   ("" (skeep)
    (("" (grind)
      (("1" (grind-reals :theories "extra_tegies") nil nil)
       ("2" (grind-reals :theories "extra_tegies") nil nil)
       ("3" (grind-reals :theories "extra_tegies") nil nil)
       ("4" (grind-reals :theories "extra_tegies") nil nil)
       ("5" (grind-reals :theories "extra_tegies") nil nil)
       ("6" (grind-reals :theories "extra_tegies") nil nil)
       ("7" (grind-reals :theories "extra_tegies") nil nil)
       ("8" (grind-reals :theories "extra_tegies") nil nil))
      nil))
    nil)
   ((StrictInterval? const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (r2i_Proper application-judgement "ProperInterval" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_times_lt_pos1 formula-decl nil real_props nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (neg_neg formula-decl nil extra_tegies nil)
    (neg_mult formula-decl nil extra_tegies nil)
    (both_sides_times_pos_lt2 formula-decl nil real_props nil)
    (lt_times_lt_neg1 formula-decl nil real_props nil)
    (mult_neg formula-decl nil extra_tegies nil)
    (both_sides_times_neg_lt2 formula-decl nil real_props nil))
   nil))
 (Pos_Zeroless 0
  (Pos_Zeroless-1 nil 3318333335 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Pos? const-decl "bool" interval 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)
    (Gt const-decl "bool" interval nil)
    (Zeroless? const-decl "bool" interval nil))
   nil))
 (Neg_Zeroless 0
  (Neg_Zeroless-1 nil 3318333335 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Neg? const-decl "bool" interval 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)
    (Lt const-decl "bool" interval nil)
    (Zeroless? const-decl "bool" interval nil))
   nil))
 (Pos_NonNeg 0
  (Pos_NonNeg-1 nil 3318333335 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Pos? const-decl "bool" interval nil)
    (Gt const-decl "bool" interval 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)
    (Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Pos_Add_NonNeg 0
  (Pos_Add_NonNeg-1 nil 3319587443 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (NonNeg? const-decl "bool" interval nil)
    (Ge const-decl "bool" interval 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (NonNeg_Add_Pos 0
  (NonNeg_Add_Pos-1 nil 3319587443 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (NonNeg? const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (Neg_Add 0
  (Neg_Add-1 nil 3318333335 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil)
    (Lt const-decl "bool" interval nil)
    (Neg? const-decl "bool" interval nil))
   nil))
 (NonNeg_Add 0
  (NonNeg_Add-1 nil 3318333335 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Neg_Pos 0
  (Neg_Pos-1 nil 3318333335 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Neg? const-decl "bool" interval nil)
    (Lt const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (Pos_Neg 0
  (Pos_Neg-1 nil 3318333335 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Pos? const-decl "bool" interval nil)
    (Gt const-decl "bool" interval 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)
    (minus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Lt const-decl "bool" interval nil)
    (Neg? const-decl "bool" interval nil))
   nil))
 (Pos_Mult 0
  (Pos_Mult-1 nil 3318333335
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)
       ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil))
      nil))
    nil)
   ((Gt const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (pos_times_gt formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (Neg_Mult 0
  (Neg_Mult-1 nil 3318333673
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)
       ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil))
      nil))
    nil)
   ((Lt const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pos_times_gt formula-decl nil real_props nil)
    (neg_times_neg formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Neg? const-decl "bool" interval nil))
   nil))
 (NonNeg_Mult 0
  (NonNeg_Mult-1 nil 3318333335
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)) nil))
    nil)
   ((Ge const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (pos_times_ge formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Pos_Div 0
  (Pos_Div-1 nil 3318333335
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)
       ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil)
       ("5" (grind-reals) nil nil) ("6" (grind-reals) nil nil)
       ("7" (grind-reals) nil nil) ("8" (grind-reals) nil nil)
       ("9" (grind-reals) nil nil) ("10" (grind-reals) nil nil)
       ("11" (grind-reals) nil nil) ("12" (grind-reals) nil nil)
       ("13" (grind-reals) nil nil) ("14" (grind-reals) nil nil))
      nil))
    nil)
   ((Gt const-decl "bool" interval nil)
    (/= const-decl "boolean" notequal nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (Div const-decl "Interval" interval nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (pos_div_gt formula-decl nil real_props nil)
    (times_div1 formula-decl nil real_props nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (zero_times1 formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (Neg_Div 0
  (Neg_Div-1 nil 3318333823
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)
       ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil)
       ("5" (grind-reals) nil nil) ("6" (grind-reals) nil nil)
       ("7" (grind-reals) nil nil) ("8" (grind-reals) nil nil)
       ("9" (grind-reals) nil nil) ("10" (grind-reals) nil nil)
       ("11" (grind-reals) nil nil) ("12" (grind-reals) nil nil)
       ("13" (grind-reals) nil nil) ("14" (grind-reals) nil nil)
       ("15" (grind-reals) nil nil) ("16" (grind-reals) nil nil))
      nil))
    nil)
   ((Lt const-decl "bool" interval nil)
    (/= const-decl "boolean" notequal nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (Div const-decl "Interval" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (pos_div_gt formula-decl nil real_props nil)
    (neg_times_neg formula-decl nil real_props nil)
    (times_div1 formula-decl nil real_props nil)
    (div_mult_neg_le1 formula-decl nil real_props nil)
    (zero_times1 formula-decl nil real_props nil)
    (div_mult_neg_ge1 formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Neg? const-decl "bool" interval nil))
   nil))
 (NonNeg_Div 0
  (NonNeg_Div-1 nil 3318333951
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)
       ("3" (grind-reals) nil nil) ("4" (grind-reals) nil nil)
       ("5" (grind-reals) nil nil) ("6" (grind-reals) nil nil)
       ("7" (grind-reals) nil nil) ("8" (grind-reals) nil nil)
       ("9" (grind-reals) nil nil) ("10" (grind-reals) nil nil))
      nil))
    nil)
   ((Ge const-decl "bool" interval nil)
    (Gt const-decl "bool" interval nil)
    (/= const-decl "boolean" notequal nil)
    ([\|\|] const-decl "Interval" interval nil)
    (pXp const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (Neg const-decl "Interval" interval nil)
    (nXp const-decl "Interval" interval nil)
    (pXn const-decl "Interval" interval nil)
    (pXm const-decl "Interval" interval nil)
    (nXn const-decl "Interval" interval nil)
    (nXm const-decl "Interval" interval nil)
    (mXp const-decl "Interval" interval nil)
    (mXn const-decl "Interval" interval 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)
    (mXm const-decl "Interval" interval nil)
    (Mult const-decl "Interval" interval nil)
    (EmptyInterval const-decl "Interval" interval nil)
    (Div const-decl "Interval" interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals 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_div_nzreal_is_real application-judgement "real" reals nil)
    (times_div1 formula-decl nil real_props nil)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (zero_times1 formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (NonNeg? const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (r2i_Pos 0
  (r2i_Pos-1 nil 3318333335 ("" (judgement-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (r2i_Neg 0
  (r2i_Neg-1 nil 3318333335 ("" (judgement-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (Lt const-decl "bool" interval nil)
    (Neg? const-decl "bool" interval nil))
   nil))
 (r2i_Nneg 0
  (r2i_Nneg-1 nil 3318333335 ("" (judgement-tcc) nil nil)
   (([\|\|] const-decl "Interval" interval nil)
    (Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil))
   nil))
 (Sq_Pos 0
  (Sq_Pos-1 nil 3318333335
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)) nil))
    nil)
   ((Gt const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    ([\|\|] const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Sq const-decl "(NonNeg?)" interval 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (pos_times_gt formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (Sq_Neg 0
  (Sq_Neg-2 nil 3319587456
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)) nil))
    nil)
   ((Lt const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    ([\|\|] const-decl "Interval" interval nil)
    (Le const-decl "bool" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Sq const-decl "(NonNeg?)" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval 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)
    (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)
    (pos_times_gt formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Neg? const-decl "bool" interval nil))
   nil))
 (Abs_Pos 0
  (Abs_Pos-1 nil 3318333335 ("" (grind) nil nil)
   ((Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Zeroin? const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (Abs const-decl "(NonNeg?)" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (Abs_Neg 0
  (Abs_Neg-2 nil 3319587494 ("" (grind) nil nil)
   ((Neg? const-decl "bool" interval nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals 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)
    (Lt const-decl "bool" interval 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)
    (Zeroin? const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (Abs const-decl "(NonNeg?)" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil))
   nil))
 (Proper_midpoint 0
  (Proper_midpoint-1 nil 3320961402 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    (|##| const-decl "bool" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (Includes_Proper 0
  (Includes_Proper-1 nil 3567527616 ("" (judgement-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)
    (Interval type-eq-decl nil interval nil)
    (Includes? const-decl "bool" interval nil)
    (|##| const-decl "bool" interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Strict_Proper 0
  (Strict_Proper-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval 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)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Strict_Add 0
  (Strict_Add-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil)
    (StrictInterval? const-decl "bool" interval nil))
   nil))
 (Add_Strict 0
  (Add_Strict-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (StrictInterval type-eq-decl nil interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil)
    (StrictInterval? const-decl "bool" interval nil))
   nil))
 (Proper_Add 0
  (Proper_Add-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Add const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Strict_Sub 0
  (Strict_Sub-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Sub const-decl "Interval" interval nil)
    (StrictInterval? const-decl "bool" interval nil))
   nil))
 (Sub_Strict 0
  (Sub_Strict-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (StrictInterval type-eq-decl nil interval 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_minus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Sub const-decl "Interval" interval nil)
    (StrictInterval? const-decl "bool" interval nil))
   nil))
 (Proper_Sub 0
  (Proper_Sub-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Sub const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Strict_Neg 0
  (Strict_Neg-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (StrictInterval? const-decl "bool" interval nil))
   nil))
 (Proper_Neg 0
  (Proper_Neg-1 nil 3320020995 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Neg const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Strict_Abs 0
  (Strict_Abs-1 nil 3320020995
   ("" (skosimp :preds? t) (("" (grind) nil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Zeroin? const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (Abs const-decl "(NonNeg?)" interval 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)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil))
   nil))
 (Proper_Abs 0
  (Proper_Abs-1 nil 3579693294 ("" (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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (Zeroin? const-decl "bool" interval 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)
    ([\|\|] const-decl "Interval" interval nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (Abs const-decl "(NonNeg?)" interval nil)
    (Proper? const-decl "bool" interval nil))
   nil))
 (Proper_Mult 0
  (Proper_Mult-2 nil 3579694493
   ("" (skeep :preds? t)
    (("" (lemma "Proper_Member")
      (("" (inst-cp -1 "X")
        (("" (inst -1 "Y")
          (("" (assert)
            (("" (skolem -1 "y")
              (("" (skolem -2 "x")
                (("" (lemma "Member_Proper")
                  (("" (inst? -1 :where 1)
                    (("" (inst -1 "x*y")
                      (("" (assert)
                        (("" (rewrite "Mult_inclusion") nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Proper_Member formula-decl nil interval nil)
    (Member_Proper formula-decl nil interval nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (Mult_inclusion formula-decl nil interval nil)
    (Mult const-decl "Interval" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil))
   nil)
  (Proper_Mult-1 nil 3579694424 ("" (judgement-tcc) nil nil) nil nil))
 (Proper_Div 0
  (Proper_Div-2 nil 3579695210
   ("" (skeep :preds? t)
    (("" (lemma "Proper_Member")
      (("" (inst-cp -1 "X")
        (("" (inst -1 "Y")
          (("" (assert)
            (("" (skolem -1 "y")
              (("" (skolem -2 "x")
                (("" (lemma "Member_Proper")
                  (("" (inst? -1 :where 1)
                    (("" (inst -1 "x/y")
                      (("1" (assert)
                        (("1" (rewrite "Div_inclusion") nil nil)) nil)
                       ("2" (hide-all-but (-1 -5 1))
                        (("2" (grind) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Proper_Member formula-decl nil interval nil)
    (Zeroless? const-decl "bool" interval nil)
    (Member_Proper formula-decl nil interval nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (/= const-decl "boolean" notequal 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)
    (y skolem-const-decl "real" interval nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (Div_inclusion formula-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (|##| const-decl "bool" interval nil)
    (Div const-decl "Interval" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil))
   nil))
 (Strict_Sq 0
  (Strict_Sq-1 nil 3579695478
   ("" (skosimp :preds? t)
    (("" (grind)
      (("1" (mult-ineq -1 -1) nil nil)
       ("2" (mult-ineq -1 -1 (- -)) nil nil)
       ("3" (mult-ineq -1 -1 (- -)) (("3" (grind) nil nil)) nil)
       ("4" (grind-reals) nil nil))
      nil))
    nil)
   ((Sq const-decl "(NonNeg?)" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Le const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Ge const-decl "bool" interval 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)
    (real_times_real_is_real application-judgement "real" reals 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)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (lt_times_lt_any1 formula-decl nil extra_real_props 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)
    (pos_times_lt formula-decl nil 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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil))
   nil))
 (Proper_Pow 0
  (Proper_Pow-2 nil 3579694648
   ("" (skeep :preds? t)
    (("" (lemma "Proper_Member")
      (("" (inst?)
        (("" (assert)
          (("" (skeep)
            (("" (lemma "Member_Proper")
              (("" (inst? -1 :where 1)
                (("" (inst -1 "x^n")
                  (("" (assert)
                    (("" (rewrite "Pow_inclusion") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Proper_Member formula-decl nil interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Member_Proper formula-decl nil interval nil)
    (^ const-decl "real" exponentiation nil)
    (/= const-decl "boolean" notequal nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (Pow_inclusion formula-decl nil interval nil)
    (Pow const-decl "Interval" interval 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_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)
    (ProperInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil))
   nil)
  (Proper_Pow-1 nil 3579694643 ("" (judgement-tcc) nil nil) nil nil))
 (Proper_Sq 0
  (Proper_Sq-1 nil 3579695307
   ("" (grind)
    (("1" (grind-reals) nil nil) ("2" (grind-reals) nil nil)
     ("3" (grind-reals) nil nil))
    nil)
   ((le_times_le_neg formula-decl nil real_props nil)
    (le_times_le_pos formula-decl nil real_props nil)
    (real_times_real_is_real application-judgement "real" 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)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (Sq const-decl "(NonNeg?)" interval nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (Le const-decl "bool" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Ge const-decl "bool" interval nil))
   shostak))
 (Proper_size 0
  (Proper_size-1 nil 3321035309 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval 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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil))
   nil))
 (Strict_size 0
  (Strict_size-1 nil 3321035309 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil))
   nil))
 (Proper_HalfLeft 0
  (Proper_HalfLeft-1 nil 3321037291 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (HalfLeft const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (Strict_HalfLeft 0
  (Strict_HalfLeft-1 nil 3321037291 ("" (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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (HalfLeft const-decl "Interval" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (Proper_HalfRight 0
  (Proper_HalfRight-1 nil 3321037361 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (HalfRight const-decl "Interval" interval nil)
    (Proper? const-decl "bool" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (Strict_HalfRightt 0
  (Strict_HalfRightt-1 nil 3321037361 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (StrictInterval type-eq-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (HalfRight const-decl "Interval" interval nil)
    (StrictInterval? const-decl "bool" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (Zeroless_Precondition 0
  (Zeroless_Precondition-1 nil 3546810075 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (<< const-decl "bool" interval nil)
    (Zeroless? const-decl "bool" interval nil)
    (Precondition? const-decl "bool" interval nil))
   nil))
 (NonNeg_Precondition 0
  (NonNeg_Precondition-1 nil 3546810075 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval 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)
    (<< const-decl "bool" interval nil)
    (Ge const-decl "bool" interval nil)
    (NonNeg? const-decl "bool" interval nil)
    (Precondition? const-decl "bool" interval nil))
   nil))
 (Pos_Precondition 0
  (Pos_Precondition-1 nil 3546810075 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval 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)
    (<< const-decl "bool" interval nil)
    (Gt const-decl "bool" interval nil)
    (Pos? const-decl "bool" interval nil)
    (Precondition? const-decl "bool" interval nil))
   nil))
 (Neg_Precondition 0
  (Neg_Precondition-1 nil 3546810075 ("" (judgement-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)
    (real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (Proper? const-decl "bool" interval nil)
    (ProperInterval type-eq-decl nil interval 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)
    (<< const-decl "bool" interval nil)
    (Lt const-decl "bool" interval nil)
    (Neg? const-decl "bool" interval nil)
    (Precondition? const-decl "bool" interval nil))
   nil)))