| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/interval_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 246 kB |
|
Quelle interval_bandb.prfSprache: Lisp |
|||||||||||||||
|
(interval_bandb (evaluate_TCC1 0 (evaluate_TCC1-1 nil 3569523672 ("" (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) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (listn_0 name-judgement "listn[real](0)" interval_bandb nil) (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)) (combine_TCC1 0 (combine_TCC1-1 nil 3569523672 ("" (skeep :preds? t) (("" (typepred "M1`counterex") (("" (hide -1) (("" (typepred "M2`counterex") (("" (hide -1) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((IntervalOutput type-eq-decl nil interval_bandb nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (Maybe type-decl nil Maybe "structures/") (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (listn_0 name-judgement "listn[real](0)" interval_bandb 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/") (IntervalOutput type-eq-decl nil interval_bandb nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (Maybe type-decl nil Maybe "structures/") (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? 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" interval_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_soundness 0 (interval_soundness-3 nil 3577544019 ("" (skeep) (("" (lemma "b_and_b_id_sound") (("" (expand "interval") (("" (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) (("1" (decompose-equality -1) (("1" (lemma "BEval_inclusion_Proper") (("1" (case "some?(bet)") (("1" (assert) (("1" (replaces -5) (("1" (inst? -) (("1" (assert) (("1" (flatten) (("1" (typepred "ev`counterex") (("1" (hide -1) (("1" (assert) (("1" (assert) (("1" (case-replace "list2array(0)(counterex(ev)) = midvars(dom)") (("1" (assert) (("1" (skeep) (("1" (lemma "BEval_inclusion") (("1" (inst -1 "dom" "midvars(dom)" "obj") (("1" (beta) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "map_length[Interval,real]") (("2" (inst?) (("2" (decompose-equality 1) (("2" (lemma "list2array_sound") (("2" (inst?) (("2" (expand "midvars") (("2" (case-replace "x!1 < length(counterex(ev))") (("1" (assert) (("1" (replaces -2) (("1" (replaces -3 :dir rl) (("1" (rewrite "map_nth_rw") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "some?(BEval(obj, Midbox(dom))) AND NOT val(BEval(obj, Midbox(dom)))") (("1" (flatten) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (case-replace "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs, length(dom))") (("1" (skeep) (("1" (rewrite "length_Midbox") (("1" (inst? -1) (("1" (lemma "Midbox_Inclusion") (("1" (inst?) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst? -) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (lemma "BEval_inclusion") (("2" (inst? - :where -5) (("2" (inst? -) (("1" (beta) (("1" (assert) (("1" (case-replace "list2array(0)(counterex(ev)) = midvars(dom)") (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "map_length[Interval,real]") (("2" (inst?) (("2" (decompose-equality 1) (("2" (lemma "list2array_sound") (("2" (inst?) (("2" (expand "midvars") (("2" (case-replace "x!1 < length(counterex(ev))") (("1" (assert) (("1" (replaces -2) (("1" (replaces -3 :dir rl) (("1" (rewrite "map_nth_rw") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "vars_in_box?" 1) (("2" (skeep) (("2" (expand "Midbox" 1) (("2" (rewrite "map_nth_rw") (("2" (replaces -3 1 :dir rl) (("2" (lemma "list2array_sound") (("2" (inst?) (("2" (rewrite "map_length") (("2" (replaces -1) (("2" (assert) (("2" (rewrite "map_nth_rw") (("2" (rewrite "r2i_inclusion") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) 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" (name-replace "COMB" "combine(v,ans1,ans)" :hide? nil) (("2" (expand "combine" -1) (("2" (case-replace "(some?(ans1`answer) AND NOT val(ans1`answer)) OR (some?(ans`answer) AND NOT val(ans`answer))") (("1" (replaces -2 :dir rl) (("1" (assert) (("1" (lemma "split_Inclusion") (("1" (inst? -1) (("1" (beta) (("1" (flatten) (("1" (case-replace "some?(ans1`answer) AND NOT val(ans1`answer)") (("1" (flatten) (("1" (expand "sound_dir") (("1" (assert) (("1" (split -5) (("1" (flatten) (("1" (case "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs, length(dom))") (("1" (replace -1) (("1" (case-replace "length(split(v, dom)`1) = length(dom)") (("1" (skeep) (("1" (inst? -) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (subtype-tcc) nil nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case-replace "cons?(ans1`counterex)") (("1" (flatten) (("1" (assert) (("1" (hide -6) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst? :where 5) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (typepred "ans`counterex") (("2" (hide -1) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs, length(dom))") (("1" (replace -1) (("1" (case-replace "length(split(v, dom)`2) = length(dom)") (("1" (skeep) (("1" (inst?) (("1" (hide -4) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (subtype-tcc) nil nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case-replace "cons?(ans1`counterex)") (("1" (flatten) (("1" (assert) (("1" (hide -4) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst? :where 6) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (typepred "ans`counterex") (("2" (hide -1) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (assert) (("2" (hide -5) (("2" (flatten) (("2" (replace 3) (("2" (typepred "ans1`counterex") (("2" (hide -1) (("2" (replace 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (case-replace "some?(ans1`answer) AND some?(ans`answer)") (("1" (flatten) (("1" (assert) (("1" (replaces -5 :dir rl) (("1" (beta) (("1" (assert) (("1" (typepred "ans1`counterex") (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (replaces -1 :dir rl) (("2" (beta) (("2" (propax) 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" (name-replace "COMB" "combine(v,ans1,ans2)" :hide? nil) (("3" (expand "combine" -1) (("3" (lemma "split_Inclusion") (("3" (inst?) (("3" (beta) (("3" (flatten) (("3" (case-replace "(some?(ans1`answer) AND NOT val(ans1`answer)) OR (some?(ans2`answer) AND NOT val(ans2`answer))") (("1" (case-replace "some?(ans1`answer) AND NOT val(ans1`answer)") (("1" (flatten) (("1" (assert) (("1" (replaces -4 :dir rl) (("1" (assert) (("1" (flatten) (("1" (case-replace "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs, length(dom))") (("1" (hide -4) (("1" (case-replace "length(split(v, dom)`1) = length(dom)") (("1" (skeep) (("1" (inst?) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (subtype-tcc) nil nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case "cons?(ans1`counterex)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst? :where 5) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -4) (("2" (typepred "ans2`counterex") (("2" (hide -1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "vars_in_box_Inclusion") (("2" (inst? :where 8) (("2" (hide -4) (("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) ("2" (replace 1) (("2" (flatten) (("2" (assert) (("2" (replaces -4 :dir rl) (("2" (assert) (("2" (flatten) (("2" (case-replace "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs, length(dom))") (("1" (hide -3) (("1" (case-replace "length(split(v, dom)`2) = length(dom)") (("1" (skeep) (("1" (inst? :where 3) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (subtype-tcc) nil nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case "cons?(ans1`counterex)") (("1" (assert) (("1" (typepred "ans1`counterex") (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "vars_in_box_Inclusion") (("2" (inst? :where 7) (("2" (hide -3) (("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) ("2" (replace 1) (("2" (case-replace "some?(ans1`answer) AND some?(ans2`answer)") (("1" (flatten) (("1" (assert) (("1" (replaces -7 :dir rl) (("1" (assert) (("1" (typepred "ans1`counterex") (("1" (hide -1) (("1" (assert) (("1" (typepred "ans2`counterex") (("1" (hide -1) (("1" (assert) (("1" (skeep) (("1" (lemma "split_vars_in_box") (("1" (inst? -1) (("1" (inst?) (("1" (beta) (("1" (case-replace "length(split(v, dom)`1) = length(dom)") (("1" (case-replace "length(split(v, dom)`2) = length(dom)") (("1" (hide -7 -9) (("1" (hide (-1 -2)) (("1" (split -1) (("1" (hide -7) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide -6) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (subtype-tcc) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (subtype-tcc) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (replaces -3 :dir rl) (("2" (beta) (("2" (propax) 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) (ProperBox type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (Interval type-eq-decl nil interval nil) (IntervalOutput type-eq-decl nil interval_bandb nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (NOT const-decl "[bool -> bool]" booleans nil) (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (Maybe type-decl nil Maybe "structures/") (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bletin? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bnot? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? 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 "IntervalOutput" interval_bandb nil) (Brancher type-eq-decl nil branch_and_bound "structures/") (branch const-decl "[BoolExpr, BoolExpr]" interval_bandb nil) (Combiner type-eq-decl nil branch_and_bound "structures/") (combine const-decl "IntervalOutput" interval_bandb nil) (DirVar type-eq-decl nil branch_and_bound "structures/") (DenormAns type-eq-decl nil branch_and_bound "structures/") (denorm const-decl "IntervalOutput" interval_bandb nil) (Evaluator type-eq-decl nil branch_and_bound "structures/") (evaluate const-decl "IntervalOutput" interval_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/") (ge_chk const-decl "bool" interval_bandb nil) (LocalExitPred type-eq-decl nil branch_and_bound "structures/") (le_chk const-decl "bool" interval_bandb nil) (prune_chk const-decl "bool" interval_bandb nil) (DirVarSelector type-eq-decl nil branch_and_bound "structures/") (SoundPred type-eq-decl nil branch_and_bound "structures/") (sound? const-decl "bool" interval_bandb nil) (SubdivDomain type-eq-decl nil branch_and_bound "structures/") (subdivide const-decl "[ProperBox, ProperBox]" interval_bandb nil) (subdiv_sound? const-decl "bool" branch_and_bound "structures/") (vs skolem-const-decl "(vars_in_box?(dom))" interval_bandb nil) (split_vars_in_box formula-decl nil interval_expr nil) (dom skolem-const-decl "ProperBox" interval_bandb nil) (v skolem-const-decl "nat" interval_bandb nil) (vs skolem-const-decl "(vars_in_box?(split(v, dom)`1))" interval_bandb nil) (vs skolem-const-decl "(vars_in_box?(split(v, dom)`2))" interval_bandb nil) (subdiv_presound? const-decl "bool" branch_and_bound "structures/") (split_Inclusion formula-decl nil interval_expr nil) (sound_dir const-decl "bool" branch_and_bound "structures/") (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) (HalfRight const-decl "Interval" interval nil) (HalfLeft const-decl "Interval" interval nil) (dom skolem-const-decl "ProperBox" interval_bandb nil) (v skolem-const-decl "nat" interval_bandb nil) (vs skolem-const-decl "(vars_in_box?(split(v, dom)`1))" interval_bandb nil) (vs skolem-const-decl "(vars_in_box?(split(v, dom)`2))" interval_bandb nil) (split_Proper application-judgement "[ProperBox, ProperBox]" interval_expr nil) (accomodates? const-decl "bool" branch_and_bound "structures/") (midvars const-decl "(vars_in_box?(pox))" box nil) (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (list2array def-decl "T" array2list "structures/") (BEval_inclusion formula-decl nil interval_bexpr nil) (map_length formula-decl nil more_map_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (map_nth_rw formula-decl nil more_map_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (list2array_sound formula-decl nil array2list "structures/") (ev skolem-const-decl "IntervalOutput" interval_bandb nil) ([\|\|] const-decl "Interval" interval nil) (r2i_Proper application-judgement "ProperInterval" interval nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (r2i_inclusion formula-decl nil interval nil) (dom skolem-const-decl "ProperBox" interval_bandb nil) (vs skolem-const-decl "(vars_in_box?(Midbox(dom)))" interval_bandb nil) (vars_in_box_Inclusion formula-decl nil box nil) (Midbox_Inclusion formula-decl nil box nil) (length_Midbox formula-decl nil box nil) (beval def-decl "bool" interval_bexpr nil) (BEval_inclusion_Proper formula-decl nil interval_bexpr nil) (listn_0 name-judgement "listn[real](0)" interval_bandb nil) (Midbox_Proper application-judgement "ProperBox" box nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (Midbox const-decl "listn[Interval](length(box))" box nil) (listn type-eq-decl nil listn "structures/") (BEval def-decl "Maybe[bool]" interval_bexpr nil) (none? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (midpoint const-decl "real" interval nil) (map adt-def-decl "list[T1]" list_adt_map nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (interval const-decl "Output" interval_bandb nil)) nil) (interval_soundness-2 nil 3576920930 ("" (skeep) (("" (lemma "b_and_b_id_sound") (("" (expand "interval") (("" (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) (("1" (decompose-equality -1) (("1" (lemma "BEval_inclusion_Proper") (("1" (case "some?(bet)") (("1" (assert) (("1" (replaces -5) (("1" (inst? -) (("1" (assert) (("1" (flatten) (("1" (typepred "ev`counterex") (("1" (hide -1) (("1" (assert) (("1" (assert) (("1" (case-replace "list2array(0)(counterex(ev)) = midvars(dom)") (("1" (assert) (("1" (skeep) (("1" (lemma "BEval_inclusion") (("1" (inst -1 "dom" "midvars(dom)" "obj") (("1" (beta) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "map_length[Interval,real]") (("2" (inst?) (("2" (decompose-equality 1) (("2" (lemma "list2array_sound") (("2" (inst?) (("2" (expand "midvars") (("2" (case-replace "x!1 < length(counterex(ev))") (("1" (assert) (("1" (replaces -2) (("1" (replaces -3 :dir rl) (("1" (rewrite "map_nth_rw") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "some?(BEval(obj, Midbox(dom))) AND NOT val(BEval(obj, Midbox(dom)))") (("1" (flatten) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (case-replace "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs)") (("1" (skeep) (("1" (inst? -1) (("1" (lemma "Midbox_Inclusion") (("1" (inst?) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst? -) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (lemma "BEval_inclusion") (("2" (inst? -) (("2" (inst? -) (("1" (beta) (("1" (assert) (("1" (case-replace "list2array(0)(counterex(ev)) = midvars(dom)") (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (lemma "map_length[Interval,real]") (("2" (inst?) (("2" (decompose-equality 1) (("2" (lemma "list2array_sound") (("2" (inst?) (("2" (expand "midvars") (("2" (case-replace "x!1 < length(counterex(ev))") (("1" (assert) (("1" (replaces -2) (("1" (replaces -3 :dir rl) (("1" (rewrite "map_nth_rw") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "vars_in_box?" 1) (("2" (skeep) (("2" (expand "Midbox" 1) (("2" (rewrite "map_nth_rw") (("2" (replaces -3 1 :dir rl) (("2" (lemma "list2array_sound") (("2" (inst?) (("2" (rewrite "map_length") (("2" (replaces -1) (("2" (assert) (("2" (rewrite "map_nth_rw") (("2" (rewrite "r2i_inclusion") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (assert) 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" (name-replace "COMB" "combine(v,ans1,ans)" :hide? nil) (("2" (expand "combine" -1) (("2" (case-replace "(some?(ans1`answer) AND NOT val(ans1`answer)) OR (some?(ans`answer) AND NOT val(ans`answer))") (("1" (replaces -2 :dir rl) (("1" (assert) (("1" (lemma "split_Inclusion") (("1" (inst? -1) (("1" (beta) (("1" (flatten) (("1" (case-replace "some?(ans1`answer) AND NOT val(ans1`answer)") (("1" (flatten) (("1" (expand "sound_dir") (("1" (assert) (("1" (split -5) (("1" (flatten) (("1" (case "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs)") (("1" (replace -1) (("1" (skeep) (("1" (inst? -1) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case-replace "cons?(ans1`counterex)") (("1" (flatten) (("1" (assert) (("1" (hide -6) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst? :where 5) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (typepred "ans`counterex") (("2" (hide -1) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs)") (("1" (replace -1) (("1" (skeep) (("1" (inst?) (("1" (hide -3) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case-replace "cons?(ans1`counterex)") (("1" (flatten) (("1" (assert) (("1" (hide -4) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst? :where 6) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (typepred "ans`counterex") (("2" (hide -1) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (assert) (("2" (hide -5) (("2" (flatten) (("2" (replace 3) (("2" (typepred "ans1`counterex") (("2" (hide -1) (("2" (replace 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (case-replace "some?(ans1`answer) AND some?(ans`answer)") (("1" (flatten) (("1" (assert) (("1" (replaces -5 :dir rl) (("1" (beta) (("1" (assert) (("1" (typepred "ans1`counterex") (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (replaces -1 :dir rl) (("2" (beta) (("2" (propax) 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" (name-replace "COMB" "combine(v,ans1,ans2)" :hide? nil) (("3" (expand "combine" -1) (("3" (lemma "split_Inclusion") (("3" (inst?) (("3" (beta) (("3" (flatten) (("3" (case-replace "(some?(ans1`answer) AND NOT val(ans1`answer)) OR (some?(ans2`answer) AND NOT val(ans2`answer))") (("1" (case-replace "some?(ans1`answer) AND NOT val(ans1`answer)") (("1" (flatten) (("1" (assert) (("1" (replaces -4 :dir rl) (("1" (assert) (("1" (flatten) (("1" (case-replace "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs)") (("1" (hide -4) (("1" (skeep) (("1" (inst?) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case "cons?(ans1`counterex)") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst? :where 5) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -4) (("2" (typepred "ans2`counterex") (("2" (hide -1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "vars_in_box_Inclusion") (("2" (inst? :where 8) (("2" (hide -4) (("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) ("2" (replace 1) (("2" (flatten) (("2" (assert) (("2" (replaces -4 :dir rl) (("2" (assert) (("2" (flatten) (("2" (case-replace "FORALL (vs: (vars_in_box?(dom))): beval(obj, vs)") (("1" (hide -3) (("1" (skeep) (("1" (inst? :where 3) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case "cons?(ans1`counterex)") (("1" (assert) (("1" (typepred "ans1`counterex") (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "vars_in_box_Inclusion") (("2" (inst? :where 7) (("2" (hide -3) (("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) ("2" (replace 1) (("2" (case-replace "some?(ans1`answer) AND some?(ans2`answer)") (("1" (flatten) (("1" (assert) (("1" (replaces -7 :dir rl) (("1" (assert) (("1" (typepred "ans1`counterex") (("1" (hide -1) (("1" (assert) (("1" (typepred "ans2`counterex") (("1" (hide -1) (("1" (assert) (("1" (skeep) (("1" (lemma "split_vars_in_box") (("1" (inst? -1) (("1" (inst?) (("1" (beta) (("1" (split -1) (("1" (hide -7 -9) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide -6 -8) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (replaces -3 :dir rl) (("2" (beta) (("2" (propax) 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) ((ProperBox type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (Interval type-eq-decl nil interval nil) (val adt-accessor-decl "[(some?) -> T]" Maybe "structures/") (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (list type-decl nil list_adt nil) (Maybe type-decl nil Maybe "structures/") (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bite? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt 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/") (Brancher type-eq-decl nil branch_and_bound "structures/") (Combiner type-eq-decl nil branch_and_bound "structures/") (DirVar type-eq-decl nil branch_and_bound "structures/") (DenormAns type-eq-decl nil branch_and_bound "structures/") (Evaluator type-eq-decl nil branch_and_bound "structures/") (stack type-eq-decl nil stack "structures/") (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/") (SubdivDomain type-eq-decl nil branch_and_bound "structures/") (subdiv_sound? const-decl "bool" branch_and_bound "structures/") (split_vars_in_box formula-decl nil interval_expr nil) (subdiv_presound? const-decl "bool" branch_and_bound "structures/") (split_Inclusion formula-decl nil interval_expr nil) (sound_dir const-decl "bool" branch_and_bound "structures/") (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_Proper application-judgement "[ProperBox, ProperBox]" interval_expr nil) (accomodates? const-decl "bool" branch_and_bound "structures/") (midvars const-decl "(vars_in_box?(pox))" box nil) (vars_in_box? const-decl "bool" box nil) (Env type-eq-decl nil box nil) (list2array def-decl "T" array2list "structures/") (BEval_inclusion formula-decl nil interval_bexpr nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (list2array_sound formula-decl nil array2list "structures/") (r2i_Proper application-judgement "ProperInterval" interval nil) (r2i_inclusion formula-decl nil interval nil) (Midbox_Inclusion formula-decl nil box nil) (vars_in_box_Inclusion formula-decl nil box nil) (beval def-decl "bool" interval_bexpr nil) (BEval_inclusion_Proper formula-decl nil interval_bexpr nil) (Midbox_Proper application-judgement "ProperBox" box nil) (Midbox const-decl "listn[Interval](length(box))" box nil) (listn type-eq-decl nil listn "structures/") (BEval def-decl "Maybe[bool]" interval_bexpr nil) (none? adt-recognizer-decl "[Maybe -> boolean]" Maybe "structures/") (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (midpoint const-decl "real" interval nil)) nil) (interval_soundness-1 nil 3546813162 ("" (skeep) (("" (lemma "b_and_b_id_sound") (("" (expand "interval") (("" (inst?) (("" (assert) (("" (hide 2) (("" (split) (("1" (expand "accomodates?") (("1" (skeep) (("1" (expand "sound?") (("1" (flatten) (("1" (name-replace "ev" "evaluate(b)(dom, obj)" :hide? nil) (("1" (copy -1) (("1" (expand "evaluate" -1 :assert? none) (("1" (skoletin* -1) (("1" (decompose-equality -1) (("1" (case-replace "bet") (("1" (assert) (("1" (skeep 2) (("1" (lemma "BEval_inclusion") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "bef") (("1" (flatten) (("1" (lemma "bwell_typed_Inclusion") (("1" (inst -1 "dom" "Midbox(dom)" "obj") (("1" (assert) (("1" (splash -1) (("1" (lemma "BEval_inclusion") (("1" (inst? -1) (("1" (tccs-step (inst? -1)) (("1" (assert) (("1" (replaces -2 :dir rl) (("1" (assert) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst -1 "Midbox(dom)" "dom" _) (("1" (inst? -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 5) (("2" (expand "vars_in_box?") (("2" (skeep) (("2" (lemma "list2array_sound") (("2" (inst?) (("2" (typepred "i") (("2" (case-replace "i < length(counterex(ev))") (("1" (replaces -3) (("1" (replaces -6 :dir rl) (("1" (expand "Midbox" 1) (("1" (rewrite "map_nth_rw") (("1" (rewrite "map_nth_rw") (("1" (rewrite "r2i_inclusion") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "Midbox(dom)") (("2" (hide-all-but (-1 -3 -8 1)) (("2" (replaces -3 :dir rl) (("2" (rewrite "map_length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "Midbox_Inclusion") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) 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" (assert) (("2" (flatten) (("2" (expand "combine") (("2" (expand "sound_dir") (("2" (lemma "split_Inclusion") (("2" (inst? -1) (("2" (skoletin* -1) (("2" (lemma "split_Proper") (("2" (inst? -1) (("2" (flatten) (("2" (lemma "bwell_typed_Inclusion") (("2" (assert) (("2" (inst -1 "dom" "bl" "obj") (("2" (assert) (("2" (lemma "bwell_typed_Inclusion") (("2" (inst -1 "dom" "br" "obj") (("2" (assert) (("2" (replace -7 :dir rl) (("2" (replace -8 :dir rl) (("2" (case-replace "ans1`isTrue AND ans`isTrue") (("1" (flatten) (("1" (assert) (("1" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (typepred "ans1`counterex") (("2" (hide -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case-replace "cons?(ans1`counterex)") (("1" (split -12) (("1" (flatten) (("1" (assert) (("1" (hide-all-but (-3 -10 2)) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst -1 "bl" "dom" _) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide-all-but (-2 -10 3)) (("2" (lemma "vars_in_box_Inclusion") (("2" (inst -1 "br" "dom" _) (("2" (inst? -) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("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) ("3" (expand "subdiv_sound?") (("3" (skeep) (("3" (expand "denorm") (("3" (expand "branch") (("3" (expand "subdivide") (("3" (expand "sound?") (("3" (flatten) (("3" (lemma "split_Inclusion") (("3" (inst? -1) (("3" (skoletin* -1) (("3" (lemma "split_Proper") (("3" (inst? -1) (("3" (flatten) (("3" (lemma "bwell_typed_Inclusion") (("3" (inst -1 "dom" "bl" "obj") (("3" (assert) (("3" (lemma "bwell_typed_Inclusion") (("3" (inst -1 "dom" "br" "obj") (("3" (assert) (("3" (replace -7 :dir rl) (("3" (replace -8 :dir rl) (("3" (flatten) (("3" (expand "combine") (("3" (case-replace "ans1`isTrue AND ans2`isTrue") (("1" (flatten) (("1" (assert) (("1" (split 1) (("1" (skeep) (("1" (lemma "split_vars_in_box") (("1" (inst? -1) (("1" (inst? -1) (("1" (beta) (("1" (split -1) (("1" (inst? -12) (("1" (assert) nil nil)) nil) ("2" (inst? -14) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "ans1`counterex") (("2" (hide -1) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "vars_in_box_Inclusion") (("2" (inst -1 "br" "dom" _) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (flatten) (("2" (case-replace "cons?(ans1`counterex)") (("1" (flatten) (("1" (assert) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst -1 "bl" "dom" _) (("1" (inst? -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (split -12) (("1" (flatten) (("1" (assert) (("1" (lemma "vars_in_box_Inclusion") (("1" (inst -1 "br" "dom" _) (("1" (inst? -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) 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) ((ProperBox type-eq-decl nil box nil) (ProperBox? const-decl "bool" box nil) (Box type-eq-decl nil box nil) (Interval type-eq-decl nil interval nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (list type-decl nil list_adt nil) (BoolExpr type-eq-decl nil IntervalExpr_adt nil) (bincludes? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (brel? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bimplies? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bor? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (band? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt nil) (bconst? adt-recognizer-decl "[IntervalExpr -> boolean]" IntervalExpr_adt 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/") (Brancher type-eq-decl nil branch_and_bound "structures/") (Combiner type-eq-decl nil branch_and_bound "structures/") (DirVar type-eq-decl nil branch_and_bound "structures/") (DenormAns type-eq-decl nil branch_and_bound "structures/") (Evaluator type-eq-decl nil branch_and_bound "structures/") (stack type-eq-decl nil stack "structures/") (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/") (SubdivDomain type-eq-decl nil branch_and_bound "structures/") (subdiv_sound? const-decl "bool" branch_and_bound "structures/") (split_vars_in_box formula-decl nil interval_expr nil) (subdiv_presound? const-decl "bool" branch_and_bound "structures/") (sound_dir const-decl "bool" branch_and_bound "structures/") (split_Proper judgement-tcc nil interval_expr nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt 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/") (Inclusion? const-decl "bool" box nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (r2i_inclusion formula-decl nil interval nil) (r2i_Proper application-judgement "ProperInterval" interval nil) (list2array_sound formula-decl nil array2list "structures/") (vars_in_box_Inclusion formula-decl nil box nil) (list2array def-decl "T" array2list "structures/") (Midbox_Inclusion formula-decl nil box nil) (BEval_inclusion formula-decl nil interval_bexpr nil) (Env type-eq-decl nil box nil) (vars_in_box? const-decl "bool" box nil) (Midbox_Proper application-judgement "ProperBox" box nil) (Midbox const-decl "listn[Interval](length(box))" box nil) (listn type-eq-decl nil listn "structures/") (null adt-constructor-decl "(null?)" list_adt nil) (midpoint const-decl "real" interval nil) (BEval def-decl "Maybe[bool]" interval_bexpr nil)) nil)))
¤ Dauer der Verarbeitung: 0.294 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26