|
(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
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.64 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
