Quelle  numerical_bandb.prf

(numerical_bandb
 (evaluate_TCC1 0
  (evaluate_TCC1-1 nil 3546971207
   ("" (skosimp*)
    (("" (lift-if -6)
      (("" (split) (("1" (assert) nil nil) ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (Ubbox_Proper application-judgement "ProperBox" box nil)
    (Lbbox_Proper application-judgement "ProperBox" box nil))
   nil))
 (evaluate_TCC2 0
  (evaluate_TCC2-1 nil 3546971207
   ("" (skosimp*) (("" (lift-if -8) (("" (assert) nil nil)) nil)) nil)
   ((Lbbox_Proper application-judgement "ProperBox" box nil)
    (Ubbox_Proper application-judgement "ProperBox" box nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (mindir_maxvar_aux_TCC1 0
  (mindir_maxvar_aux_TCC1-1 nil 3547134405
   ("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil))
    nil)
   ((ProperBox type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (Box type-eq-decl nil box nil) (list type-decl nil list_adt 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)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Midbox_Proper application-judgement "ProperBox" box nil)
    (r2i_Proper application-judgement "ProperInterval" interval nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (Midbox const-decl "listn[Interval](length(box))" box nil)
    ([\|\|] const-decl "Interval" interval nil)
    (midpoint const-decl "real" interval nil)
    (slice const-decl "real" interval nil))
   nil))
 (mindir_maxvar_aux_TCC2 0
  (mindir_maxvar_aux_TCC2-1 nil 3547134405 ("" (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)
    (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (ProperBox type-eq-decl nil box nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (IntervalExpr type-decl nil IntervalExpr_adt nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (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)
    (length def-decl "nat" list_props nil)
    (listn type-eq-decl nil listn "structures/")
    (slice const-decl "real" interval nil)
    (midpoint const-decl "real" interval nil)
    ([\|\|] const-decl "Interval" interval nil)
    (Midbox const-decl "listn[Interval](length(box))" box nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (max_rec_TCC1 0
  (max_rec_TCC1-1 nil 3546365509 ("" (subtype-tcc) nil nil) nil nil))
 (max_rec_TCC2 0
  (max_rec_TCC2-1 nil 3546365509 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil))
   nil))
 (max_rec_TCC3 0
  (max_rec_TCC3-1 nil 3546365509 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (size const-decl "real" interval nil))
   nil))
 (max_rec_TCC4 0
  (max_rec_TCC4-1 nil 3546365509 ("" (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)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil))
   nil))
 (max_rec_TCC5 0
  (max_rec_TCC5-1 nil 3546365509 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (max_rec_TCC6 0
  (max_rec_TCC6-1 nil 3546365509 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil))
   nil))
 (max_rec_TCC7 0
  (max_rec_TCC7-1 nil 3546365509 ("" (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)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (size const-decl "real" interval nil))
   nil))
 (max_rec_TCC8 0
  (max_rec_TCC8-1 nil 3546365509 ("" (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)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil))
   nil))
 (max_rec_TCC9 0
  (max_rec_TCC9-1 nil 3546365509 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (max_rec_TCC10 0
  (max_rec_TCC10-1 nil 3546365509 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (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)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (size const-decl "real" interval nil))
   nil))
 (max_rec_TCC11 0
  (max_rec_TCC11-1 nil 3546365509 ("" (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)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (subrange type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (list type-decl nil list_adt nil)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (max_aux_TCC1 0
  (max_aux_TCC1-1 nil 3547134405 ("" (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)
    (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (ProperBox type-eq-decl nil box nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/"))
   nil))
 (max_aux_TCC2 0
  (max_aux_TCC2-1 nil 3547134405
   ("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil))
    nil)
   ((ProperBox type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (Box type-eq-decl nil box nil) (list type-decl nil list_adt 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)
    (every adt-def-decl "boolean" list_adt nil)
    (length def-decl "nat" list_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (max_aux_TCC3 0
  (max_aux_TCC3-1 nil 3547134405 ("" (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)
    (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (ProperBox type-eq-decl nil box nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/"))
   nil))
 (max_aux_TCC4 0
  (max_aux_TCC4-1 nil 3547134405
   ("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil))
    nil)
   ((ProperBox type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (Box type-eq-decl nil box nil) (list type-decl nil list_adt 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_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/"))
   nil))
 (max_aux_TCC5 0
  (max_aux_TCC5-1 nil 3547134405
   ("" (skeep)
    (("" (case-replace "box=null")
      (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
    nil)
   ((real nonempty-type-from-decl nil reals nil)
    (Interval type-eq-decl nil interval nil)
    (list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (ProperBox? const-decl "bool" box nil)
    (ProperBox type-eq-decl nil box nil)
    (null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
    (null adt-constructor-decl "(null?)" list_adt nil)
    (length def-decl "nat" list_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   nil))
 (altvar_TCC1 0
  (altvar_TCC1-1 nil 3547136696
   ("" (skeep :preds? t) (("" (grind) nil nil)) nil)
   ((ProperBox? const-decl "bool" box nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/"))
   nil))
 (altvar_TCC2 0
  (altvar_TCC2-1 nil 3547136696
   ("" (skeep :preds? t)
    (("" (lemma "mod_pos")
      (("" (inst?) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((mod_pos formula-decl nil mod nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (stack type-eq-decl nil stack "structures/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (IntervalMinMax type-eq-decl nil numerical_bandb nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (IntervalExpr type-decl nil IntervalExpr_adt 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)
    (Interval type-eq-decl nil interval nil)
    (list type-decl nil list_adt 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)
    (length def-decl "nat" list_props nil)
    (Box type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (ProperBox type-eq-decl nil box nil)
    (box skolem-const-decl "ProperBox" numerical_bandb nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (interval_minmax_soundness 0
  (interval_minmax_soundness-3 nil 3579703168
   ("" (skeep)
    (("" (lemma "b_and_b_id_sound")
      (("" (expand "interval_minmax")
        (("" (inst?)
          (("" (assert)
            (("" (hide 2)
              (("" (split)
                (("1" (expand "accomodates?")
                  (("1" (skeep)
                    (("1" (expand "sound?")
                      (("1" (flatten)
                        (("1"
                          (name-replace "ev" "evaluate(dom, obj)"
                           :hide? nil)
                          (("1" (copy -1)
                            (("1" (expand "evaluate" -1 :assert? none)
                              (("1"
                                (skoletin* -1 :old? t)
                                (("1"
                                  (decompose-equality -3)
                                  (("1"
                                    (case
                                     "Inclusion?(ev`lb_box, dom) AND Inclusion?(ev`ub_box, dom)")
                                    (("1"
                                      (flatten)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (split 1)
                                          (("1"
                                            (skeep)
                                            (("1"
                                              (lemma
                                               "Eval_inclusion_Proper")
                                              (("1"
                                                (inst?)
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (skeep :preds? t)
                                            (("2"
                                              (replaces -18)
                                              (("2"
                                                (hide
                                                 (-3 -7 -8 -9 -10))
                                                (("2"
                                                  (case-replace
                                                   "ub(P1) < ub(P2)")
                                                  (("1"
                                                    (lemma
                                                     "Eval_inclusion_Proper")
                                                    (("1"
                                                      (inst
                                                       -1
                                                       "Lb"
                                                       "vs"
                                                       "obj")
                                                      (("1"
                                                        (beta)
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (expand
                                                             "##")
                                                            (("1"
                                                              (lemma
                                                               "Proper_Inclusion")
                                                              (("1"
                                                                (inst?)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (inst?)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    (("2"
                                                      (lemma
                                                       "Eval_inclusion_Proper")
                                                      (("2"
                                                        (inst
                                                         -1
                                                         "Ub"
                                                         "vs"
                                                         "obj")
                                                        (("2"
                                                          (beta)
                                                          (("2"
                                                            (expand
                                                             "##")
                                                            (("2"
                                                              (lemma
                                                               "Proper_Inclusion")
                                                              (("2"
                                                                (inst?)
                                                                (("2"
                                                                  (assert)
                                                                  (("2"
                                                                    (inst?)
                                                                    (("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("3"
                                            (skeep :preds? t)
                                            (("3"
                                              (replaces -18)
                                              (("3"
                                                (hide
                                                 (-2 -4 -5 -11 -12))
                                                (("3"
                                                  (case-replace
                                                   "lb(P1) > lb(P2)")
                                                  (("1"
                                                    (lemma
                                                     "Eval_inclusion_Proper")
                                                    (("1"
                                                      (inst
                                                       -1
                                                       "Lb"
                                                       "vs"
                                                       "obj")
                                                      (("1"
                                                        (beta)
                                                        (("1"
                                                          (expand "##")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (lemma
                                                               "Proper_Inclusion")
                                                              (("1"
                                                                (inst?)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (inst?)
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    (("2"
                                                      (lemma
                                                       "Eval_inclusion_Proper")
                                                      (("2"
                                                        (inst
                                                         -1
                                                         "Ub"
                                                         "vs"
                                                         "obj")
                                                        (("2"
                                                          (expand "##")
                                                          (("2"
                                                            (lemma
                                                             "Proper_Inclusion")
                                                            (("2"
                                                              (inst?)
                                                              (("2"
                                                                (assert)
                                                                (("2"
                                                                  (inst?)
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (split 1)
                                        (("1"
                                          (hide (-4 -5 -6 -7))
                                          (("1"
                                            (case "ub(P1) < ub(P2)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (lemma
                                                 "Lbbox_Inclusion")
                                                (("1"
                                                  (inst?)
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (assert)
                                              (("2"
                                                (lemma
                                                 "Ubbox_Inclusion")
                                                (("2"
                                                  (inst?)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide (-1 -2 -8 -9))
                                          (("2"
                                            (case "lb(P1) > lb(P2)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (lemma
                                                 "Lbbox_Inclusion")
                                                (("1"
                                                  (inst?)
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (assert)
                                              (("2"
                                                (lemma
                                                 "Ubbox_Inclusion")
                                                (("2"
                                                  (inst? -1)
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "subdiv_presound?")
                  (("2" (skeep)
                    (("2" (expand "denorm")
                      (("2" (expand "branch")
                        (("2" (expand "subdivide")
                          (("2" (expand "sound?")
                            (("2" (flatten)
                              (("2"
                                (expand "combine" -3)
                                (("2"
                                  (use "Proper_Safe2")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (flatten)
                                      (("2"
                                        (expand "combine" 1 1)
                                        (("2"
                                          (replaces -3)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (flatten)
                                              (("2"
                                                (expand "combine")
                                                (("2"
                                                  (expand "sound_dir")
                                                  (("2"
                                                    (lemma
                                                     "split_Inclusion")
                                                    (("2"
                                                      (inst? -1)
                                                      (("2"
                                                        (skoletin*
                                                         -1
                                                         :old?
                                                         t)
                                                        (("2"
                                                          (lemma
                                                           "split_Proper")
                                                          (("2"
                                                            (inst? -1)
                                                            (("2"
                                                              (flatten)
                                                              (("2"
                                                                (replace
                                                                 -3
                                                                 :dir
                                                                 rl)
                                                                (("2"
                                                                  (replace
                                                                   -4
                                                                   :dir
                                                                   rl)
                                                                  (("2"
                                                                    (split
                                                                     1)
                                                                    (("1"
                                                                      (skeep
                                                                       :preds?
                                                                       t)
                                                                      (("1"
                                                                        (inst
                                                                         -
                                                                         "vs")
                                                                        (("1"
                                                                          (rewrite
                                                                           "Union_inclusion")
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (lift-if)
                                                                      (("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (split
                                                                           1)
                                                                          (("1"
                                                                            (flatten)
                                                                            (("1"
                                                                              (split
                                                                               -)
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (lemma
                                                                                   "Inclusion_trans")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -1
                                                                                     "ans1`lb_box"
                                                                                     "bl"
                                                                                     "dom")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (flatten)
                                                                                (("2"
                                                                                  (lemma
                                                                                   "Inclusion_trans")
                                                                                  (("2"
                                                                                    (inst
                                                                                     -1
                                                                                     "ans1`lb_box"
                                                                                     "br"
                                                                                     "dom")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("3"
                                                                      (lift-if)
                                                                      (("3"
                                                                        (assert)
                                                                        (("3"
                                                                          (split
                                                                           1)
                                                                          (("1"
                                                                            (flatten)
                                                                            (("1"
                                                                              (split
                                                                               -)
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (lemma
                                                                                   "Inclusion_trans")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -1
                                                                                     "ans1`ub_box"
                                                                                     "bl"
                                                                                     "dom")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (flatten)
                                                                                (("2"
                                                                                  (lemma
                                                                                   "Inclusion_trans")
                                                                                  (("2"
                                                                                    (inst
                                                                                     -1
                                                                                     "ans1`ub_box"
                                                                                     "br"
                                                                                     "dom")
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("4"
                                                                      (skeep
                                                                       :preds?
                                                                       t)
                                                                      (("4"
                                                                        (expand
                                                                         "combine")
                                                                        (("4"
                                                                          (case
                                                                           "ans1`lb_max < ans`lb_max")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (split
                                                                               -)
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (inst
                                                                                   -5
                                                                                   "vs")
                                                                                  (("1"
                                                                                    (lemma
                                                                                     "length_split_1")
                                                                                    (("1"
                                                                                      (inst?)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (flatten)
                                                                                (("2"
                                                                                  (inst
                                                                                   -4
                                                                                   "vs")
                                                                                  (("2"
                                                                                    (lemma
                                                                                     "length_split_1")
                                                                                    (("2"
                                                                                      (inst?)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (hide
                                                                               -15)
                                                                              (("2"
                                                                                (inst
                                                                                 -13
                                                                                 "vs")
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("5"
                                                                      (skeep
                                                                       :preds?
                                                                       t)
                                                                      (("5"
                                                                        (expand
                                                                         "combine")
                                                                        (("5"
                                                                          (case
                                                                           "ans1`ub_min > ans`ub_min")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (split
                                                                               -)
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (inst
                                                                                   -6
                                                                                   "vs")
                                                                                  (("1"
                                                                                    (lemma
                                                                                     "length_split_1")
                                                                                    (("1"
                                                                                      (inst?)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (flatten)
                                                                                (("2"
                                                                                  (inst
                                                                                   -5
                                                                                   "vs")
                                                                                  (("2"
                                                                                    (lemma
                                                                                     "length_split_1")
                                                                                    (("2"
                                                                                      (inst?)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (hide
                                                                               -15)
                                                                              (("2"
                                                                                (inst
                                                                                 -14
                                                                                 "vs")
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("3" (expand "subdiv_sound?")
                  (("3" (skeep)
                    (("3" (expand "denorm")
                      (("3" (expand "branch")
                        (("3" (expand "subdivide")
                          (("3" (expand "sound?")
                            (("3" (flatten)
                              (("3"
                                (expand "combine" -3)
                                (("3"
                                  (use "Proper_Safe2")
                                  (("3"
                                    (assert)
                                    (("3"
                                      (flatten)
                                      (("3"
                                        (expand "combine" 1 1)
                                        (("3"
                                          (replaces -3)
                                          (("3"
                                            (assert)
                                            (("3"
                                              (lemma "split_Inclusion")
                                              (("3"
                                                (inst? -1)
                                                (("3"
                                                  (skoletin*
                                                   -1
                                                   :old?
                                                   t)
                                                  (("3"
                                                    (lemma
                                                     "split_Proper")
                                                    (("3"
                                                      (inst? -1)
                                                      (("3"
                                                        (flatten)
                                                        (("3"
                                                          (replace
                                                           -3
                                                           :dir
                                                           rl)
                                                          (("3"
                                                            (replace
                                                             -4
                                                             :dir
                                                             rl)
                                                            (("3"
                                                              (expand
                                                               "combine")
                                                              (("3"
                                                                (split
                                                                 1)
                                                                (("1"
                                                                  (skeep
                                                                   :preds?
                                                                   t)
                                                                  (("1"
                                                                    (lemma
                                                                     "split_vars_in_box")
                                                                    (("1"
                                                                      (inst?
                                                                       -1)
                                                                      (("1"
                                                                        (inst?)
                                                                        (("1"
                                                                          (beta)
                                                                          (("1"
                                                                            (split
                                                                             -1)
                                                                            (("1"
                                                                              (inst?
                                                                               -11)
                                                                              (("1"
                                                                                (rewrite
                                                                                 "Union_inclusion")
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (inst?
                                                                               -16)
                                                                              (("1"
                                                                                (rewrite
                                                                                 "Union_inclusion")
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (lift-if)
                                                                  (("2"
                                                                    (split
                                                                     1)
                                                                    (("1"
                                                                      (flatten)
                                                                      (("1"
                                                                        (lemma
                                                                         "Inclusion_trans")
                                                                        (("1"
                                                                          (inst
                                                                           -1
                                                                           "ans1`lb_box"
                                                                           "bl"
                                                                           "dom")
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (flatten)
                                                                      (("2"
                                                                        (lemma
                                                                         "Inclusion_trans")
                                                                        (("2"
                                                                          (inst
                                                                           -1
                                                                           "ans2`lb_box"
                                                                           "br"
                                                                           "dom")
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("3"
                                                                  (lift-if)
                                                                  (("3"
                                                                    (split
                                                                     1)
                                                                    (("1"
                                                                      (flatten)
                                                                      (("1"
                                                                        (lemma
                                                                         "Inclusion_trans")
                                                                        (("1"
                                                                          (inst
                                                                           -1
                                                                           "ans1`ub_box"
                                                                           "bl"
                                                                           "dom")
                                                                          (("1"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (flatten)
                                                                      (("2"
                                                                        (lemma
                                                                         "Inclusion_trans")
                                                                        (("2"
                                                                          (inst
                                                                           -1
                                                                           "ans2`ub_box"
                                                                           "br"
                                                                           "dom")
                                                                          (("2"
                                                                            (assert)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("4"
                                                                  (skeep
                                                                   :preds?
                                                                   t)
                                                                  (("4"
                                                                    (expand
                                                                     "combine")
                                                                    (("4"
                                                                      (case
                                                                       "ans1`lb_max < ans2`lb_max")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (inst
                                                                           -14
                                                                           "vs")
                                                                          (("1"
                                                                            (lemma
                                                                             "length_split_1")
                                                                            (("1"
                                                                              (inst?)
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (inst
                                                                           -18
                                                                           "vs")
                                                                          (("2"
                                                                            (lemma
                                                                             "length_split_1")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("5"
                                                                  (skeep
                                                                   :preds?
                                                                   t)
                                                                  (("5"
                                                                    (expand
                                                                     "combine")
                                                                    (("5"
                                                                      (case
                                                                       "ans1`ub_min > ans2`ub_min")
                                                                      (("1"
                                                                        (assert)
                                                                        (("1"
                                                                          (inst
                                                                           -15
                                                                           "vs")
                                                                          (("1"
                                                                            (lemma
                                                                             "length_split_1")
                                                                            (("1"
                                                                              (inst?)
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (assert)
                                                                        (("2"
                                                                          (inst
                                                                           -19
                                                                           "vs")
                                                                          (("2"
                                                                            (lemma
                                                                             "length_split_1")
                                                                            (("2"
                                                                              (inst?)
                                                                              (("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    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)
    (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)
    (ProperBox? const-decl "bool" box nil)
    (Box type-eq-decl nil box nil) (list type-decl nil list_adt nil)
    (IntervalMinMax type-eq-decl nil numerical_bandb nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (ProperBox type-eq-decl nil box nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (IntervalExpr type-decl nil IntervalExpr_adt nil)
    (b_and_b_id_sound formula-decl nil branch_and_bound "structures/")
    (Accumulator type-eq-decl nil branch_and_bound "structures/")
    (accumulate const-decl "IntervalMinMax" numerical_bandb nil)
    (Brancher type-eq-decl nil branch_and_bound "structures/")
    (branch const-decl "[RealExpr, RealExpr]" numerical_bandb nil)
    (Combiner type-eq-decl nil branch_and_bound "structures/")
    (combine const-decl "IntervalMinMax" numerical_bandb nil)
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (DenormAns type-eq-decl nil branch_and_bound "structures/")
    (denorm const-decl "IntervalMinMax" numerical_bandb nil)
    (Evaluator type-eq-decl nil branch_and_bound "structures/")
    (evaluate const-decl "IntervalMinMax" numerical_bandb nil)
    (stack type-eq-decl nil stack "structures/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (length def-decl "nat" list_props nil)
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (ExitPred type-eq-decl nil branch_and_bound "structures/")
    (LocalExitPred type-eq-decl nil branch_and_bound "structures/")
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (SoundPred type-eq-decl nil branch_and_bound "structures/")
    (sound? const-decl "bool" numerical_bandb nil)
    (SubdivDomain type-eq-decl nil branch_and_bound "structures/")
    (subdivide const-decl "[ProperBox, ProperBox]" numerical_bandb nil)
    (subdiv_sound? const-decl "bool" branch_and_bound "structures/")
    (v skolem-const-decl "nat" numerical_bandb nil)
    (dom skolem-const-decl "ProperBox" numerical_bandb nil)
    (vs skolem-const-decl "(vars_in_box?(dom))" numerical_bandb nil)
    (split_vars_in_box formula-decl nil interval_expr nil)
    (subdiv_presound? const-decl "bool" branch_and_bound "structures/")
    (Proper_Safe2 formula-decl nil safe_arith nil)
    (Union const-decl "Interval" interval nil)
    (sound_dir const-decl "bool" branch_and_bound "structures/")
    (split_Proper judgement-tcc nil interval_expr nil)
    (length_split_1 formula-decl nil interval_expr nil)
    (Inclusion_trans formula-decl nil box nil)
    (eval def-decl "real" interval_expr nil)
    (Union_inclusion formula-decl nil interval nil)
    (below type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (nth def-decl "T" list_props nil)
    (HalfLeft const-decl "Interval" interval nil)
    (HalfRight const-decl "Interval" interval nil)
    (split def-decl "{lrb: [Box, Box] |
         LET (lb, rb) = lrb IN
           length(lb) = length(box) AND
            length(rb) = length(box) AND
             (FORALL (i: below(length(box))):
                IF i = v
                  THEN nth(lb, i) = HalfLeft(nth(box, i)) AND
                        nth(rb, i) = HalfRight(nth(box, i))
                ELSE nth(lb, i) = nth(box, i) AND nth(rb, i) = nth(box, i)
                ENDIF)}" interval_expr nil)
    (split_Inclusion formula-decl nil interval_expr nil)
    (split_Proper application-judgement "[ProperBox, ProperBox]"
     interval_expr nil)
    (accomodates? const-decl "bool" branch_and_bound "structures/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (Ubbox_Inclusion formula-decl nil box nil)
    (Lbbox_Inclusion formula-decl nil box nil)
    (Eval_inclusion_Proper formula-decl nil interval_expr nil)
    (Env type-eq-decl nil box nil)
    (vars_in_box? const-decl "bool" box nil)
    (dom skolem-const-decl "ProperBox" numerical_bandb nil)
    (Lb skolem-const-decl "listn[Interval](length(dom))"
     numerical_bandb nil)
    (obj skolem-const-decl "RealExpr" numerical_bandb nil)
    (vs skolem-const-decl "(vars_in_box?(evaluate(dom, obj)`lb_box))"
     numerical_bandb nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (le_realorder name-judgement "RealOrder" real_orders "reals/")
    (Proper_Inclusion formula-decl nil interval_expr nil)
    (|##| const-decl "bool" interval nil)
    (vs skolem-const-decl "(vars_in_box?(evaluate(dom, obj)`ub_box))"
     numerical_bandb nil)
    (ge_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Inclusion? const-decl "bool" box nil)
    (Lbbox const-decl "listn[Interval](length(box))" box nil)
    (Ubbox const-decl "listn[Interval](length(box))" box nil)
    (< const-decl "bool" reals nil) (> const-decl "bool" reals nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (listn type-eq-decl nil listn "structures/")
    (Ubbox_Proper application-judgement "ProperBox" box nil)
    (Lbbox_Proper application-judgement "ProperBox" box nil)
    (Eval def-decl "Interval" interval_expr nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (lt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (gt_realorder name-judgement "RealOrder" real_orders "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (interval_minmax const-decl "Output" numerical_bandb nil))
   nil))
 (numerical_soundness 0
  (numerical_soundness-1 nil 3567682854
   ("" (skeep)
    (("" (expand "numerical")
      (("" (rewrite "interval_minmax_soundness") nil nil)) nil))
    nil)
   ((numerical const-decl "Output" numerical_bandb nil)
    (DirVarSelector type-eq-decl nil branch_and_bound "structures/")
    (prune_mm const-decl "bool" numerical_bandb nil)
    (le_mm const-decl "bool" numerical_bandb nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (LocalExitPred type-eq-decl nil branch_and_bound "structures/")
    (ge_mm const-decl "bool" numerical_bandb nil)
    (ExitPred type-eq-decl nil branch_and_bound "structures/")
    (DirVarStack type-eq-decl nil branch_and_bound "structures/")
    (length def-decl "nat" list_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (stack type-eq-decl nil stack "structures/")
    (DirVar type-eq-decl nil branch_and_bound "structures/")
    (IntervalMinMax type-eq-decl nil numerical_bandb 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (RealExpr type-eq-decl nil IntervalExpr_adt nil)
    (letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (div? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (add? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (const? adt-recognizer-decl "[IntervalExpr -> boolean]"
     IntervalExpr_adt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (IntervalExpr type-decl nil IntervalExpr_adt nil)
    (ProperBox type-eq-decl nil box nil)
    (ProperBox? const-decl "bool" box nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Box type-eq-decl nil box nil) (list type-decl nil list_adt nil)
    (Interval type-eq-decl nil interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (interval_minmax_soundness formula-decl nil numerical_bandb nil))
   shostak)))