|
(numerical_bandb
(evaluate_TCC1 0
(evaluate_TCC1-1 nil 3546971207
("" (skosimp*)
(("" (lift-if -6)
(("" (split) (("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(Ubbox_Proper application-judgement "ProperBox" box nil)
(Lbbox_Proper application-judgement "ProperBox" box nil))
nil))
(evaluate_TCC2 0
(evaluate_TCC2-1 nil 3546971207
("" (skosimp*) (("" (lift-if -8) (("" (assert) nil nil)) nil)) nil)
((Lbbox_Proper application-judgement "ProperBox" box nil)
(Ubbox_Proper application-judgement "ProperBox" box nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(mindir_maxvar_aux_TCC1 0
(mindir_maxvar_aux_TCC1-1 nil 3547134405
("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Box type-eq-decl nil box nil) (list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Midbox_Proper application-judgement "ProperBox" box nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(ge_realorder name-judgement "RealOrder" real_orders "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(Midbox const-decl "listn[Interval](length(box))" box nil)
([\|\|] const-decl "Interval" interval nil)
(midpoint const-decl "real" interval nil)
(slice const-decl "real" interval nil))
nil))
(mindir_maxvar_aux_TCC2 0
(mindir_maxvar_aux_TCC2-1 nil 3547134405 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IntervalExpr type-decl nil IntervalExpr_adt nil)
(const? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(add? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(div? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(RealExpr type-eq-decl nil IntervalExpr_adt nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(listn type-eq-decl nil listn "structures/")
(slice const-decl "real" interval nil)
(midpoint const-decl "real" interval nil)
([\|\|] const-decl "Interval" interval nil)
(Midbox const-decl "listn[Interval](length(box))" box nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(max_rec_TCC1 0
(max_rec_TCC1-1 nil 3546365509 ("" (subtype-tcc) nil nil) nil nil))
(max_rec_TCC2 0
(max_rec_TCC2-1 nil 3546365509 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(size const-decl "real" interval nil))
nil))
(max_rec_TCC3 0
(max_rec_TCC3-1 nil 3546365509 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(size const-decl "real" interval nil))
nil))
(max_rec_TCC4 0
(max_rec_TCC4-1 nil 3546365509 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(size const-decl "real" interval nil))
nil))
(max_rec_TCC5 0
(max_rec_TCC5-1 nil 3546365509 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(size const-decl "real" interval nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(max_rec_TCC6 0
(max_rec_TCC6-1 nil 3546365509 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(size const-decl "real" interval nil))
nil))
(max_rec_TCC7 0
(max_rec_TCC7-1 nil 3546365509 ("" (termination-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(size const-decl "real" interval nil))
nil))
(max_rec_TCC8 0
(max_rec_TCC8-1 nil 3546365509 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(size const-decl "real" interval nil))
nil))
(max_rec_TCC9 0
(max_rec_TCC9-1 nil 3546365509 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(size const-decl "real" interval nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(max_rec_TCC10 0
(max_rec_TCC10-1 nil 3546365509 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(size const-decl "real" interval nil))
nil))
(max_rec_TCC11 0
(max_rec_TCC11-1 nil 3546365509 ("" (termination-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(max_aux_TCC1 0
(max_aux_TCC1-1 nil 3547134405 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/"))
nil))
(max_aux_TCC2 0
(max_aux_TCC2-1 nil 3547134405
("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Box type-eq-decl nil box nil) (list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(length def-decl "nat" list_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(max_aux_TCC3 0
(max_aux_TCC3-1 nil 3547134405 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/"))
nil))
(max_aux_TCC4 0
(max_aux_TCC4-1 nil 3547134405
("" (skosimp*) (("" (typepred "box!1") (("" (grind) nil nil)) nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Box type-eq-decl nil box nil) (list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/"))
nil))
(max_aux_TCC5 0
(max_aux_TCC5-1 nil 3547134405
("" (skeep)
(("" (case-replace "box=null")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(null adt-constructor-decl "(null?)" list_adt nil)
(length def-decl "nat" list_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(altvar_TCC1 0
(altvar_TCC1-1 nil 3547136696
("" (skeep :preds? t) (("" (grind) nil nil)) nil)
((ProperBox? const-decl "bool" box nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/"))
nil))
(altvar_TCC2 0
(altvar_TCC2-1 nil 3547136696
("" (skeep :preds? t)
(("" (lemma "mod_pos")
(("" (inst?) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil)
((mod_pos formula-decl nil mod nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" real_orders "reals/")
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(DirVarStack type-eq-decl nil branch_and_bound "structures/")
(= const-decl "[T, T -> boolean]" equalities nil)
(stack type-eq-decl nil stack "structures/")
(DirVar type-eq-decl nil branch_and_bound "structures/")
(IntervalMinMax type-eq-decl nil numerical_bandb nil)
(RealExpr type-eq-decl nil IntervalExpr_adt nil)
(letin? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(fun? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(div? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(pow? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(sq? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(mult? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(sub? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(neg? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(abs? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(add? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(varidx? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(const? adt-recognizer-decl "[IntervalExpr -> boolean]"
IntervalExpr_adt nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IntervalExpr type-decl nil IntervalExpr_adt nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(Box type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(box skolem-const-decl "ProperBox" numerical_bandb nil)
(gt_realorder name-judgement "RealOrder" real_orders "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(interval_minmax_soundness 0
(interval_minmax_soundness-3 nil 3579703168
("" (skeep)
(("" (lemma "b_and_b_id_sound")
(("" (expand "interval_minmax")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (split)
(("1" (expand "accomodates?")
(("1" (skeep)
(("1" (expand "sound?")
(("1" (flatten)
(("1"
(name-replace "ev" "evaluate(dom, obj)"
:hide? nil)
(("1" (copy -1)
(("1" (expand "evaluate" -1 :assert? none)
(("1"
(skoletin* -1 :old? t)
(("1"
(decompose-equality -3)
(("1"
(case
"Inclusion?(ev`lb_box, dom) AND Inclusion?(ev`ub_box, dom)")
(("1"
(flatten)
(("1"
(assert)
(("1"
(split 1)
(("1"
(skeep)
(("1"
(lemma
"Eval_inclusion_Proper")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(skeep :preds? t)
(("2"
(replaces -18)
(("2"
(hide
(-3 -7 -8 -9 -10))
(("2"
(case-replace
"ub(P1) < ub(P2)")
(("1"
(lemma
"Eval_inclusion_Proper")
(("1"
(inst
-1
"Lb"
"vs"
"obj")
(("1"
(beta)
(("1"
(assert)
(("1"
(expand
"##")
(("1"
(lemma
"Proper_Inclusion")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"Eval_inclusion_Proper")
(("2"
(inst
-1
"Ub"
"vs"
"obj")
(("2"
(beta)
(("2"
(expand
"##")
(("2"
(lemma
"Proper_Inclusion")
(("2"
(inst?)
(("2"
(assert)
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skeep :preds? t)
(("3"
(replaces -18)
(("3"
(hide
(-2 -4 -5 -11 -12))
(("3"
(case-replace
"lb(P1) > lb(P2)")
(("1"
(lemma
"Eval_inclusion_Proper")
(("1"
(inst
-1
"Lb"
"vs"
"obj")
(("1"
(beta)
(("1"
(expand "##")
(("1"
(assert)
(("1"
(lemma
"Proper_Inclusion")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"Eval_inclusion_Proper")
(("2"
(inst
-1
"Ub"
"vs"
"obj")
(("2"
(expand "##")
(("2"
(lemma
"Proper_Inclusion")
(("2"
(inst?)
(("2"
(assert)
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(split 1)
(("1"
(hide (-4 -5 -6 -7))
(("1"
(case "ub(P1) < ub(P2)")
(("1"
(assert)
(("1"
(lemma
"Lbbox_Inclusion")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"Ubbox_Inclusion")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide (-1 -2 -8 -9))
(("2"
(case "lb(P1) > lb(P2)")
(("1"
(assert)
(("1"
(lemma
"Lbbox_Inclusion")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"Ubbox_Inclusion")
(("2"
(inst? -1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "subdiv_presound?")
(("2" (skeep)
(("2" (expand "denorm")
(("2" (expand "branch")
(("2" (expand "subdivide")
(("2" (expand "sound?")
(("2" (flatten)
(("2"
(expand "combine" -3)
(("2"
(use "Proper_Safe2")
(("2"
(assert)
(("2"
(flatten)
(("2"
(expand "combine" 1 1)
(("2"
(replaces -3)
(("2"
(assert)
(("2"
(flatten)
(("2"
(expand "combine")
(("2"
(expand "sound_dir")
(("2"
(lemma
"split_Inclusion")
(("2"
(inst? -1)
(("2"
(skoletin*
-1
:old?
t)
(("2"
(lemma
"split_Proper")
(("2"
(inst? -1)
(("2"
(flatten)
(("2"
(replace
-3
:dir
rl)
(("2"
(replace
-4
:dir
rl)
(("2"
(split
1)
(("1"
(skeep
:preds?
t)
(("1"
(inst
-
"vs")
(("1"
(rewrite
"Union_inclusion")
nil
nil))
nil))
nil)
("2"
(lift-if)
(("2"
(assert)
(("2"
(split
1)
(("1"
(flatten)
(("1"
(split
-)
(("1"
(flatten)
(("1"
(lemma
"Inclusion_trans")
(("1"
(inst
-1
"ans1`lb_box"
"bl"
"dom")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(lemma
"Inclusion_trans")
(("2"
(inst
-1
"ans1`lb_box"
"br"
"dom")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil)
("3"
(lift-if)
(("3"
(assert)
(("3"
(split
1)
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.34 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.
|
