|
(boxes
(unpack_TCC1 0
(unpack_TCC1-1 nil 3506383942 ("" (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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" util nil))
nil))
(neg_mp_TCC1 0
(neg_mp_TCC1-2 nil 3510769198
("" (skeep)
(("" (typepred "mp`rel")
(("" (expand "realorder?")
(("" (flatten)
(("" (split -1)
(("1" (decompose-equality 4) (("1" (grind) nil nil)) nil)
("2" (decompose-equality 3) (("2" (grind) nil nil)) nil)
("3" (decompose-equality 2) (("3" (grind) nil nil)) nil)
("4" (decompose-equality 1) (("4" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((MPolyRel type-eq-decl nil MPoly nil)
(RealOrder type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(MultiPolynomial type-eq-decl nil util nil)
(DegreeMono type-eq-decl nil util nil)
(Coeff type-eq-decl nil util nil)
(realorder? const-decl "bool" util nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(>= const-decl "bool" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" util nil)
(> const-decl "bool" reals nil))
nil)
(neg_mp_TCC1-1 nil 3510769138 ("" (subtype-tcc) nil nil) nil nil))
(Boxes_strategy_rec_TCC1 0
(Boxes_strategy_rec_TCC1-1 nil 3506383942 ("" (subtype-tcc) nil nil)
nil nil))
(Boxes_strategy_rec_TCC2 0
(Boxes_strategy_rec_TCC2-1 nil 3506383942
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nil application-judgement "below(m)" mod nil))
nil))
(Boxes_strategy_rec_TCC3 0
(Boxes_strategy_rec_TCC3-1 nil 3506383942
("" (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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil)
(posint_plus_nnint_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" util nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint nonempty-type-eq-decl nil integers nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
nil))
(Boxes_strategy_rec_TCC4 0
(Boxes_strategy_rec_TCC4-1 nil 3506383942 ("" (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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" util nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint nonempty-type-eq-decl nil integers nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
nil))
(Boxes_strategy_TCC1 0
(Boxes_strategy_TCC1-1 nil 3506383942 ("" (subtype-tcc) nil nil) nil
nil))
(boxes_strategy_and_TCC1 0
(boxes_strategy_and_TCC1-1 nil 3506446918
("" (termination-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(le_realorder name-judgement "RealOrder" util nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(array2list const-decl
"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}"
array2list "structures/")
(unitbox const-decl "Box(n)" boxes_def nil)
(mk_boxes const-decl "Boxes(n)" boxes_def nil)
(unpack const-decl "Boxes(n)" boxes nil)
(Boxes_strategy const-decl "Boxes(nvars)" boxes nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(boxes_strategy_and_TCC2 0
(boxes_strategy_and_TCC2-1 nil 3511092063 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(Boxes_strategy const-decl "Boxes(nvars)" boxes nil)
(volume const-decl "real" boxes_def nil)
(add_real const-decl "real" boxes nil)
(for const-decl "T" for_iterate "structures/")
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(boxes_strategy_and_TCC3 0
(boxes_strategy_and_TCC3-1 nil 3511092063 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(Boxes_strategy const-decl "Boxes(nvars)" boxes nil)
(volume const-decl "real" boxes_def nil)
(add_real const-decl "real" boxes nil)
(for const-decl "T" for_iterate "structures/")
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(boxes_strategy_and_TCC4 0
(boxes_strategy_and_TCC4-1 nil 3511092176 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(listn_0 name-judgement "listn[real](0)" boxes nil)
(listn type-eq-decl nil listn "structures/")
(MVars type-eq-decl nil MPoly nil) (Vars type-eq-decl nil util nil)
(posnat nonempty-type-eq-decl nil integers nil)
(IntervalEndpoints type-eq-decl nil util nil)
(length def-decl "nat" list_props nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(Boxes_strategy const-decl "Boxes(nvars)" boxes nil)
(volume const-decl "real" boxes_def nil)
(add_real const-decl "real" boxes nil)
(for const-decl "T" for_iterate "structures/")
(denormalize_listreal const-decl "listn[real](length(l))" util nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil)))
¤ Dauer der Verarbeitung: 0.5 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.
|
