|
(box
(proper_box 0
(proper_box-1 nil 3569510967
("" (skeep :preds? t)
(("" (expand "ProperBox?")
(("" (flatten)
(("" (lemma "every_nth[Interval]")
(("" (inst?) (("" (assert) (("" (inst? -1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((ProperBox? const-decl "bool" box nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(Proper? const-decl "bool" interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(ProperBox type-eq-decl nil box nil)
(below type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(every_nth formula-decl nil list_props nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil))
shostak))
(proper_append 0
(proper_append-1 nil 3577499084
("" (induct-and-simplify "pox1") nil nil)
((list type-decl nil list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(Box type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(append def-decl "list[T]" list_props nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(list_induction formula-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Proper? const-decl "bool" interval nil))
nil))
(vars_in_box_rec_TCC1 0
(vars_in_box_rec_TCC1-1 nil 3546870280 ("" (subtype-tcc) nil nil) nil
nil))
(vars_in_box_rec_TCC2 0
(vars_in_box_rec_TCC2-1 nil 3546870280 ("" (subtype-tcc) nil nil) nil
nil))
(vars_in_box_rec_TCC3 0
(vars_in_box_rec_TCC3-1 nil 3546870280 ("" (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)
(= 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(vars_in_box_rec_TCC4 0
(vars_in_box_rec_TCC4-1 nil 3546870280 ("" (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)
(= 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(|##| const-decl "bool" interval nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(vars_in_box_rec_TCC5 0
(vars_in_box_rec_TCC5-1 nil 3546870280 ("" (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)
(= 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(|##| const-decl "bool" interval nil))
nil))
(vars_in_box_rec_TCC6 0
(vars_in_box_rec_TCC6-2 nil 3546873959
("" (skosimp* :preds? t)
(("" (iff)
(("" (split)
(("1" (flatten)
(("1" (split -1)
(("1" (skosimp* :preds? t)
(("1" (hide 1) (("1" (grind) nil nil)) nil)) nil)
("2" (flatten)
(("2" (skeep :preds? t)
(("2" (case-replace "i!1=k")
(("1" (hide -5)
(("1" (assert)
(("1" (expand "nth") (("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(typepred
"v!1(cdr[Interval](box!1), n!1, i!1 + 1)(vs!1)")
(("1" (replaces -1)
(("1" (inst -4 "k")
(("1" (expand "nth" 2) (("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (hide -3 -4 3)
(("2" (expand "length" -4)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split)
(("1" (inst -1 "i!1")
(("1" (expand "nth" -1) (("1" (propax) nil nil)) nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil)
("2"
(typepred
"v!1(cdr[Interval](box!1), n!1, i!1 + 1)(vs!1)")
(("1" (replaces -1)
(("1" (skeep :preds? t)
(("1" (case-replace "i!1=k")
(("1" (assert) nil nil)
("2" (inst -3 "k")
(("2" (expand "nth" -3) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2" (expand "length" -2) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((int_plus_int_is_int application-judgement "int" integers nil)
(nth def-decl "T" list_props nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(k skolem-const-decl "subrange(i!1, n!1 - 1)" box nil)
(i!1 skolem-const-decl "{i: nat | i + length(box!1) = n!1}" box
nil)
(n!1 skolem-const-decl "nat" box nil)
(box!1 skolem-const-decl "Box" box nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(pred type-eq-decl nil defined_types nil)
(strict_well_founded? const-decl "bool" orders nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(Env type-eq-decl nil box nil)
(|##| const-decl "bool" interval nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(subrange type-eq-decl nil integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(= 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))
nil)
(vars_in_box_rec_TCC6-1 nil 3546873940 ("" (subtype-tcc) nil nil) nil
nil))
(vars_in_box 0
(vars_in_box-1 nil 3546871405
("" (skeep)
(("" (decompose-equality)
(("" (expand "vars_in_box?")
(("" (typepred "vars_in_box_rec(box, length(box), 0)(x!1)")
(("" (replaces -1) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((Interval type-eq-decl nil interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(Env type-eq-decl nil box nil)
(vars_in_box? const-decl "bool" box 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)
(length def-decl "nat" list_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(|##| const-decl "bool" interval nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(vars_in_box_rec def-decl
"{b: bool | b = (FORALL (k: subrange(i, n - 1)): vs(k) ## nth(box, k - i))}"
box nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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))
shostak))
(midvars_TCC1 0
(midvars_TCC1-1 nil 3546794101
("" (skeep)
(("" (expand "vars_in_box?")
(("" (skeep)
(("" (rewrite "midpoint_inclusion")
(("" (hide 2)
(("" (typepred "pox")
(("" (expand "ProperBox?")
(("" (flatten)
(("" (rewrite "every_nth") (("" (inst? -) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((vars_in_box? const-decl "bool" box nil)
(midpoint_inclusion formula-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(length def-decl "nat" list_props nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil) (Box type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(ProperBox type-eq-decl nil box nil)
(below type-eq-decl nil naturalnumbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil)
(every_nth formula-decl nil list_props nil))
nil))
(Lbbox_TCC1 0
(Lbbox_TCC1-1 nil 3546968069
("" (skeep) (("" (rewrite "map_length") nil nil)) nil)
((map_length formula-decl nil more_map_props 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)
([\|\|] const-decl "Interval" interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil))
nil))
(length_Lbbox 0
(length_Lbbox-1 nil 3577544620
("" (skeep)
(("" (typepred "Lbbox(pox)") (("" (propax) nil nil)) nil)) nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Lbbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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))
nil))
(Ubbox_TCC1 0
(Ubbox_TCC1-1 nil 3546968132
("" (skeep) (("" (rewrite "map_length") nil nil)) nil)
((map_length formula-decl nil more_map_props 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)
([\|\|] const-decl "Interval" interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil))
nil))
(length_Ubbox 0
(length_Ubbox-2 nil 3577621360
("" (skeep)
(("" (typepred "Ubbox(pox)") (("" (propax) nil nil)) nil)) nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Ubbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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))
nil)
(length_Ubbox-1 nil 3577544640
("" (skeep)
(("" (lemma "Ubbox_Inclusion")
(("" (insteep -)
(("" (expand "Inclusion?") (("" (flatten) nil nil)) nil)) nil))
nil))
nil)
((Interval type-eq-decl nil interval nil)) nil))
(Midbox_TCC1 0
(Midbox_TCC1-2 nil 3546993506
("" (skeep) (("" (rewrite "map_length") nil nil)) nil)
((map_length formula-decl nil more_map_props 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)
([\|\|] const-decl "Interval" interval nil)
(midpoint const-decl "real" interval nil)
(list type-decl nil list_adt nil) (Box type-eq-decl nil box nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil))
nil)
(Midbox_TCC1-1 nil 3546993450 ("" (subtype-tcc) nil nil) nil nil))
(length_Midbox 0
(length_Midbox-2 nil 3577621378
("" (skeep)
(("" (typepred "Midbox(pox)") (("" (propax) nil nil)) nil)) nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Midbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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))
nil)
(length_Midbox-1 nil 3577544690
("" (skeep)
(("" (lemma "Midbox_Inclusion")
(("" (insteep -)
(("" (expand "Inclusion?") (("" (flatten) nil nil)) nil)) nil))
nil))
nil)
((Interval type-eq-decl nil interval nil)) nil))
(Inclusion?_TCC1 0
(Inclusion?_TCC1-1 nil 3549130199 ("" (subtype-tcc) nil nil)
((below type-eq-decl nil naturalnumbers nil)
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(< const-decl "bool" reals 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))
nil))
(Inclusion_reflx 0
(Inclusion_reflx-1 nil 3549185471
("" (skeep)
(("" (expand "Inclusion?")
(("" (skeep) (("" (rewrite "Incl_reflx") nil nil)) nil)) nil))
nil)
((Inclusion? const-decl "bool" box nil)
(Incl_reflx formula-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(list type-decl nil list_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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(length def-decl "nat" list_props nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil) (Box type-eq-decl nil box nil)
(below type-eq-decl nil naturalnumbers nil))
nil))
(Inclusion_trans 0
(Inclusion_trans-1 nil 3549195103
("" (skeep)
(("" (expand "Inclusion?")
(("" (flatten)
(("" (assert)
(("" (skeep)
(("" (inst? -2)
(("" (inst? -4)
(("" (lemma "Incl_trans")
((""
(inst -1 "nth(box1,i)" "nth(box2,i)" "nth(box,i)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Inclusion? const-decl "bool" box 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(below type-eq-decl nil naturalnumbers nil)
(Incl_trans formula-decl nil interval nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil))
shostak))
(Inclusion_Proper 0
(Inclusion_Proper-1 nil 3576771283
("" (skeep)
(("" (expand "Inclusion?")
(("" (flatten)
(("" (typepred "pox")
(("" (expand "ProperBox?")
(("" (rewrite "every_nth")
(("" (rewrite "every_nth")
(("" (skeep)
(("" (insteep -3)
(("1" (insteep -)
(("1" (lemma "Incl_Proper")
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Inclusion? const-decl "bool" box 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_nth formula-decl nil list_props nil)
(PRED type-eq-decl nil defined_types nil)
(Proper? const-decl "bool" interval nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(Incl_Proper formula-decl nil interval nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pox skolem-const-decl "ProperBox" box nil)
(i skolem-const-decl "below(length[Interval](box))" box nil)
(below type-eq-decl nil naturalnumbers nil)
(box skolem-const-decl "Box" box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(< const-decl "bool" 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))
nil))
(Lbbox_Proper 0
(Lbbox_Proper-1 nil 3546968597
("" (skeep :preds? t)
(("" (typepred "Lbbox(pox)")
(("" (expand "ProperBox?")
(("" (lemma "every_nth[Interval]")
(("" (inst? :where 1)
(("" (replaces -1)
(("" (skeep 1)
(("" (expand "Lbbox" 1)
(("" (lemma "map_nth_rw[Interval,Interval]")
(("" (inst?)
(("1" (replaces -1) (("1" (grind) nil nil)) nil)
("2" (hide 2)
(("2" (typepred "i") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Lbbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(every_nth formula-decl nil list_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(pox skolem-const-decl "ProperBox" box nil)
(below type-eq-decl nil naturalnumbers nil)
(i skolem-const-decl "below(length[Interval](Lbbox(pox)))" box nil)
([\|\|] const-decl "Interval" interval nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(map_nth_rw formula-decl nil more_map_props nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil))
nil))
(Ubbox_Proper 0
(Ubbox_Proper-5 nil 3577621617
("" (skeep :preds? t)
(("" (typepred "Ubbox(pox)")
(("" (expand "ProperBox?")
(("" (lemma "every_nth[Interval]")
(("" (inst? :where 1)
(("" (replaces -1)
(("" (skeep 1)
(("" (expand "Ubbox" 1)
(("" (lemma "map_nth_rw[Interval,Interval]")
(("" (inst?)
(("1" (replaces -1) (("1" (grind) nil nil)) nil)
("2" (hide 2)
(("2" (typepred "i") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Ubbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(every_nth formula-decl nil list_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(pox skolem-const-decl "ProperBox" box nil)
(below type-eq-decl nil naturalnumbers nil)
(i skolem-const-decl "below(length[Interval](Ubbox(pox)))" box nil)
([\|\|] const-decl "Interval" interval nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(map_nth_rw formula-decl nil more_map_props nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil))
nil)
(Ubbox_Proper-4 nil 3576770592
("" (skeep :preds? t)
(("" (typepred "Ubbox(pox)")
(("" (expand "ProperBox?")
(("" (flatten)
(("" (split 1)
(("1" (lemma "list_inclusive[Interval]")
(("1" (inst?)
(("1" (split -1)
(("1" (expand "length" -2) (("1" (assert) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (lemma "every_nth[Interval]")
(("2" (inst?)
(("2" (replaces -1)
(("2" (skeep 1)
(("2" (expand "Ubbox" 1)
(("2" (lemma "map_nth_rw[Interval,Interval]")
(("2" (inst?)
(("1" (replaces -1) (("1" (grind) nil nil))
nil)
("2" (hide 2)
(("2" (typepred "i")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((listn type-eq-decl nil listn "structures/")
(Interval type-eq-decl nil interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Proper? const-decl "bool" interval nil))
nil)
(Ubbox_Proper-3 nil 3549147163
("" (skeep :preds? t)
(("" (typepred "Ubbox(box)")
(("" (expand "ProperBox?")
(("" (flatten)
(("" (split 1)
(("1" (lemma "list_inclusive[Interval]")
(("1" (inst?)
(("1" (split -1)
(("1" (expand "length" -2) (("1" (assert) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (lemma "every_nth[Interval]")
(("2" (inst?)
(("2" (replaces -1)
(("2" (skeep 1)
(("2" (expand "Ubbox" 1)
(("2" (lemma "map_nth_rw[Interval,Interval]")
(("2" (inst?)
(("1" (replaces -1) (("1" (grind) nil nil))
nil)
("2" (hide 2)
(("2" (typepred "i")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((listn type-eq-decl nil listn "structures/")
(Interval type-eq-decl nil interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Proper? const-decl "bool" interval nil))
nil)
(Ubbox_Proper-2 nil 3546968668
("" (skeep :preds? t)
(("" (typepred "Ubbox(box)") (("" (grind) nil nil)) nil)) nil)
((listn type-eq-decl nil listn "structures/")
(ProperInterval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(Interval type-eq-decl nil interval nil))
nil)
(Ubbox_Proper-1 nil 3546968597 ("" (judgement-tcc) nil nil) nil nil))
(Midbox_Proper 0
(Midbox_Proper-5 nil 3577621646
("" (skeep :preds? t)
(("" (typepred "Midbox(pox)")
(("" (expand "ProperBox?")
(("" (lemma "every_nth[Interval]")
(("" (inst? :where 1)
(("" (replaces -1)
(("" (skeep 1)
(("" (expand "Midbox" 1)
(("" (lemma "map_nth_rw[Interval,Interval]")
(("" (inst?)
(("1" (replaces -1) (("1" (grind) nil nil)) nil)
("2" (hide 2)
(("2" (typepred "i") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Midbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(every_nth formula-decl nil list_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(pox skolem-const-decl "ProperBox" box nil)
(below type-eq-decl nil naturalnumbers nil)
(i skolem-const-decl "below(length[Interval](Midbox(pox)))" box
nil)
(midpoint const-decl "real" interval nil)
([\|\|] const-decl "Interval" interval nil)
(slice const-decl "real" interval nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(map_nth_rw formula-decl nil more_map_props nil)
(Proper? const-decl "bool" interval nil)
(PRED type-eq-decl nil defined_types nil))
nil)
(Midbox_Proper-4 nil 3576770609
("" (skeep :preds? t)
(("" (typepred "Midbox(pox)")
(("" (expand "ProperBox?")
(("" (flatten)
(("" (split 1)
(("1" (lemma "list_inclusive[Interval]")
(("1" (inst?)
(("1" (split -1)
(("1" (expand "length" -2) (("1" (assert) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (lemma "every_nth[Interval]")
(("2" (inst?)
(("2" (replaces -1)
(("2" (skeep 1)
(("2" (expand "Midbox" 1)
(("2" (lemma "map_nth_rw[Interval,Interval]")
(("2" (inst?)
(("1" (replaces -1) (("1" (grind) nil nil))
nil)
("2" (hide 2)
(("2" (typepred "i")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((listn type-eq-decl nil listn "structures/")
(Interval type-eq-decl nil interval nil)
(midpoint const-decl "real" interval nil)
(slice const-decl "real" interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Proper? const-decl "bool" interval nil))
nil)
(Midbox_Proper-3 nil 3549147212
("" (skeep :preds? t)
(("" (typepred "Midbox(box)")
(("" (expand "ProperBox?")
(("" (flatten)
(("" (split 1)
(("1" (lemma "list_inclusive[Interval]")
(("1" (inst?)
(("1" (split -1)
(("1" (expand "length" -2) (("1" (assert) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil)
("2" (lemma "every_nth[Interval]")
(("2" (inst?)
(("2" (replaces -1)
(("2" (skeep 1)
(("2" (expand "Midbox" 1)
(("2" (lemma "map_nth_rw[Interval,Interval]")
(("2" (inst?)
(("1" (replaces -1) (("1" (grind) nil nil))
nil)
("2" (hide 2)
(("2" (typepred "i")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((listn type-eq-decl nil listn "structures/")
(Interval type-eq-decl nil interval nil)
(midpoint const-decl "real" interval nil)
(slice const-decl "real" interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Proper? const-decl "bool" interval nil))
nil)
(Midbox_Proper-2 nil 3546993456
("" (skeep :preds? t)
(("" (typepred "Midbox(box)") (("" (grind) nil nil)) nil)) nil)
((listn type-eq-decl nil listn "structures/")
(ProperInterval type-eq-decl nil interval nil)
(Proper? const-decl "bool" interval nil)
(Interval type-eq-decl nil interval nil)
(midpoint const-decl "real" interval nil)
(slice const-decl "real" interval nil))
nil)
(Midbox_Proper-1 nil 3546993450 ("" (judgement-tcc) nil nil) nil
nil))
(Lbbox_Inclusion 0
(Lbbox_Inclusion-2 nil 3576770662
("" (skeep :preds? t)
(("" (typepred "Lbbox(pox)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Lbbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| lb(X) |]" "pox"
"i")
(("" (replaces -1)
(("" (expand "ProperBox?")
(("" (hide -3)
(("" (lemma "every_nth[Interval]")
(("" (inst?)
(("" (assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "lb_inclusion")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Lbbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(Lbbox_Proper application-judgement "ProperBox" box nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
([\|\|] const-decl "Interval" interval nil)
(every_nth formula-decl nil list_props nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Incl_r2i formula-decl nil interval nil)
(lb_inclusion formula-decl nil interval nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(PRED type-eq-decl nil defined_types nil)
(Proper? const-decl "bool" interval nil)
(map_nth_rw formula-decl nil more_map_props nil)
(Inclusion? const-decl "bool" box nil))
nil)
(Lbbox_Inclusion-1 nil 3549130214
("" (skeep :preds? t)
(("" (typepred "Lbbox(box)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Lbbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| lb(X) |]" "box"
"i")
(("" (replaces -1)
(("" (assert)
(("" (expand "ProperBox?")
(("" (flatten)
(("" (hide -4)
(("" (lemma "every_nth[Interval]")
((""
(inst?)
((""
(assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "lb_inclusion")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((listn type-eq-decl nil listn "structures/")
(Interval type-eq-decl nil interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Incl_r2i formula-decl nil interval nil)
(lb_inclusion formula-decl nil interval nil)
(Proper? const-decl "bool" interval nil))
shostak))
(Ubbox_Inclusion 0
(Ubbox_Inclusion-5 nil 3577622015
("" (skeep :preds? t)
(("" (typepred "Ubbox(pox)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Ubbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| ub(X) |]" "pox"
"i")
(("" (replaces -1)
(("" (expand "ProperBox?")
(("" (hide -3)
(("" (lemma "every_nth[Interval]")
(("" (inst?)
(("" (assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "ub_inclusion")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Ubbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(Ubbox_Proper application-judgement "ProperBox" box nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
([\|\|] const-decl "Interval" interval nil)
(every_nth formula-decl nil list_props nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Incl_r2i formula-decl nil interval nil)
(ub_inclusion formula-decl nil interval nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(PRED type-eq-decl nil defined_types nil)
(Proper? const-decl "bool" interval nil)
(map_nth_rw formula-decl nil more_map_props nil)
(Inclusion? const-decl "bool" box nil))
nil)
(Ubbox_Inclusion-4 nil 3577621968
("" (skeep :preds? t)
(("" (typepred "Ubbox(pox)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Ubbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| lb(X) |]" "pox"
"i")
(("" (replaces -1)
(("" (expand "ProperBox?")
(("" (hide -3)
(("" (lemma "every_nth[Interval]")
(("" (inst?)
(("" (assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "ub_inclusion")
nil))))))))))))))))))))))))))))))))
nil)
nil nil)
(Ubbox_Inclusion-3 nil 3577621910
("" (skeep :preds? t)
(("" (typepred "Lbbox(pox)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Lbbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| lb(X) |]" "pox"
"i")
(("" (replaces -1)
(("" (expand "ProperBox?")
(("" (hide -3)
(("" (lemma "every_nth[Interval]")
(("" (inst?)
(("" (assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "lb_inclusion")
nil))))))))))))))))))))))))))))))))
nil)
nil nil)
(Ubbox_Inclusion-2 nil 3576770680
("" (skeep :preds? t)
(("" (typepred "Ubbox(pox)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Ubbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| ub(X) |]" "pox"
"i")
(("" (replaces -1)
(("" (assert)
(("" (expand "ProperBox?")
(("" (flatten)
(("" (hide -4)
(("" (lemma "every_nth[Interval]")
((""
(inst?)
((""
(assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "ub_inclusion")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((listn type-eq-decl nil listn "structures/")
(Interval type-eq-decl nil interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Incl_r2i formula-decl nil interval nil)
(ub_inclusion formula-decl nil interval nil)
(Proper? const-decl "bool" interval nil))
nil)
(Ubbox_Inclusion-1 nil 3549133570
("" (skeep :preds? t)
(("" (typepred "Ubbox(box)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Ubbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| ub(X) |]" "box"
"i")
(("" (replaces -1)
(("" (assert)
(("" (expand "ProperBox?")
(("" (flatten)
(("" (hide -4)
(("" (lemma "every_nth[Interval]")
((""
(inst?)
((""
(assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "ub_inclusion")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((listn type-eq-decl nil listn "structures/")
(Interval type-eq-decl nil interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Incl_r2i formula-decl nil interval nil)
(ub_inclusion formula-decl nil interval nil)
(Proper? const-decl "bool" interval nil))
nil))
(Midbox_Inclusion 0
(Midbox_Inclusion-4 nil 3577622054
("" (skeep :preds? t)
(("" (typepred "Midbox(pox)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Midbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| midpoint(X) |]"
"pox" "i")
(("" (replaces -1)
(("" (expand "ProperBox?")
(("" (hide -3)
(("" (lemma "every_nth[Interval]")
(("" (inst?)
(("" (assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "midpoint_inclusion")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ProperBox type-eq-decl nil box nil)
(ProperBox? const-decl "bool" box nil)
(Midbox const-decl "listn[Interval](length(box))" box nil)
(listn type-eq-decl nil listn "structures/")
(Box type-eq-decl nil box nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(list type-decl nil list_adt nil)
(Interval type-eq-decl nil interval nil)
(real nonempty-type-from-decl nil reals nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(Midbox_Proper application-judgement "ProperBox" box nil)
([\|\|] const-decl "Interval" interval nil)
(midpoint const-decl "real" interval nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(every_nth formula-decl nil list_props nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Incl_r2i formula-decl nil interval nil)
(midpoint_inclusion formula-decl nil interval nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(PRED type-eq-decl nil defined_types nil)
(Proper? const-decl "bool" interval nil)
(map_nth_rw formula-decl nil more_map_props nil)
(Inclusion? const-decl "bool" box nil))
nil)
(Midbox_Inclusion-3 nil 3577622028
("" (skeep :preds? t)
(("" (typepred "Ubbox(pox)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Ubbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
((""
(inst -1 "LAMBDA (X: Interval): [| ub(X) |]" "pox"
"i")
(("" (replaces -1)
(("" (expand "ProperBox?")
(("" (hide -3)
(("" (lemma "every_nth[Interval]")
(("" (inst?)
(("" (assert)
((""
(inst? -1)
((""
(hide-all-but (-1 1))
((""
(rewrite "ub_inclusion")
nil))))))))))))))))))))))))))))))))
nil)
nil nil)
(Midbox_Inclusion-2 nil 3576770697
("" (skeep :preds? t)
(("" (typepred "Midbox(pox)")
(("" (expand "Inclusion?")
(("" (assert)
(("" (skeep 1 :preds? t)
(("" (expand "Midbox")
(("" (lemma "map_nth_rw[Interval,Interval]")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.104 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.
|
