|
(multi_polylist
(maxnum_TCC1 0
(maxnum_TCC1-1 nil 3603213169 ("" (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))
nil))
(maxnum_TCC2 0
(maxnum_TCC2-1 nil 3603213169 ("" (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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil))
nil))
(max_TCC1 0
(max_TCC1-1 nil 3603199783 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_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)
(length def-decl "nat" list_props nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil))
nil))
(max_TCC2 0
(max_TCC2-1 nil 3603207043 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(length def-decl "nat" list_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil))
nil))
(max_TCC3 0
(max_TCC3-1 nil 3603207043 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_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)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(max_TCC4 0
(max_TCC4-1 nil 3603207043 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_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)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(max_TCC5 0
(max_TCC5-1 nil 3603207043 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(length def-decl "nat" list_props nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil))
nil))
(max_TCC6 0
(max_TCC6-1 nil 3603207043 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil))
nil))
(max_TCC7 0
(max_TCC7-1 nil 3603207043 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil))
nil))
(max_TCC8 0
(max_TCC8-1 nil 3603210536 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil))
nil))
(max_TCC9 0
(max_TCC9-1 nil 3603210536 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(length def-decl "nat" list_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil))
nil))
(max_TCC10 0
(max_TCC10-1 nil 3603210536
("" (skeep)
(("" (split)
(("1" (expand "length" + 1)
(("1" (assert)
(("1" (expand "length" + 2)
(("1" (expand "length" + 3)
(("1" (typepred "v(cdr[nat](ml1), cdr[nat](ml2))")
(("1" (replaces -2)
(("1" (expand "maxnum" +)
(("1" (lift-if) (("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (expand "nth" + 1)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (assert)
(("2" (ground)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil)
("4" (expand "length" -2)
(("4"
(typepred "v(cdr[nat](ml1), cdr[nat](ml2))")
(("4" (inst - "i-1")
(("4" (assert)
(("4" (lift-if)
(("4"
(ground)
(("1" (grind) nil nil)
("2" (grind) nil nil)
("3" (grind) nil nil)
("4" (grind) nil nil)
("5" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (expand "length" -2)
(("5"
(typepred "v(cdr[nat](ml1), cdr[nat](ml2))")
(("5" (inst - "i-1")
(("5" (assert)
(("5" (lift-if) (("5" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("6" (expand "length" -1)
(("6"
(typepred "v(cdr[nat](ml1), cdr[nat](ml2))")
(("6" (inst - "i-1")
(("6" (assert) (("6" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util 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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(length def-decl "nat" list_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_realorder name-judgement "RealOrder" util nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(max_id 0
(max_id-1 nil 3603440469
("" (induct "ml")
(("1" (grind) nil nil)
("2" (skolem 1 ("rr" "ll"))
(("2" (flatten)
(("2" (expand "max" +)
(("2" (expand "maxnum") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((list_induction formula-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)
(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)
(max def-decl "{ml |
length[nat](ml) = maxnum(length[nat](ml1), length[nat](ml2)) AND
(FORALL (i: nat):
i < length(ml) IMPLIES
nth(ml, i) =
IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)
ELSIF null?(ml2) OR i >= length(ml2) THEN nth(ml1, i)
ELSE maxnum(nth(ml1, i), nth(ml2, i))
ENDIF)}" multi_polylist nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(length def-decl "nat" list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(MonoList type-eq-decl nil multi_polylist nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil))
shostak))
(max_cdr_TCC1 0
(max_cdr_TCC1-1 nil 3603447297 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil)
(max def-decl "{ml |
length[nat](ml) = maxnum(length[nat](ml1), length[nat](ml2)) AND
(FORALL (i: nat):
i < length(ml) IMPLIES
nth(ml, i) =
IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)
ELSIF null?(ml2) OR i >= length(ml2) THEN nth(ml1, i)
ELSE maxnum(nth(ml1, i), nth(ml2, i))
ENDIF)}" multi_polylist nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil))
nil))
(max_cdr 0
(max_cdr-1 nil 3603447298
(""
(case "FORALL (ml1, ml2: MonoList,r1,r2:real):
cdr(max(cons(r1,ml1), cons(r2,ml2))) = max(cdr(cons(r1,ml1)), cdr(cons(r2,ml2)))")
(("1" (skeep)
(("1" (inst - "cdr(ml1)" "cdr(ml2)" "car(ml1)" "car(ml2)")
(("1" (assert)
(("1"
(case "FORALL (l:list[nat]): (NOT null?(l)) IMPLIES l = cons(car(l),cdr(l))")
(("1" (rewrite -1 :dir rl)
(("1" (rewrite -1 :dir rl) nil nil)) nil)
("2" (hide-all-but 1)
(("2" (skeep) (("2" (decompose-equality 2) nil nil))
nil))
nil)
("3" (assert)
(("3" (hide-all-but 1) (("3" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (assert)
(("2" (expand "max" + 1) (("2" (propax) nil nil)) nil)) nil))
nil)
("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (grind) nil nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(list_cons_extensionality formula-decl nil list_adt nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(car adt-accessor-decl "[(cons?) -> T]" list_adt nil)
(number nonempty-type-decl nil numbers nil)
(list type-decl nil list_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(length def-decl "nat" list_props nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(max def-decl "{ml |
length[nat](ml) = maxnum(length[nat](ml1), length[nat](ml2)) AND
(FORALL (i: nat):
i < length(ml) IMPLIES
nth(ml, i) =
IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)
ELSIF null?(ml2) OR i >= length(ml2) THEN nth(ml1, i)
ELSE maxnum(nth(ml1, i), nth(ml2, i))
ENDIF)}" multi_polylist nil)
(cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil))
shostak))
(max_sym 0
(max_sym-1 nil 3603445515
("" (induct "ml1")
(("1" (grind)
(("1" (expand "max" +)
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (skolem 1 ("r" "l"))
(("2" (flatten)
(("2" (skeep)
(("2" (expand "max" +)
(("2" (lift-if)
(("2" (ground)
(("2" (case "maxnum(r,car(ml2)) = maxnum(car(ml2),r)")
(("1" (replace -1)
(("1" (inst - "cdr(ml2)") (("1" (assert) nil nil))
nil))
nil)
("2" (expand "maxnum" 1)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if) (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(car adt-accessor-decl "[(cons?) -> T]" list_adt nil)
(cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(list_induction formula-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)
(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)
(max def-decl "{ml |
length[nat](ml) = maxnum(length[nat](ml1), length[nat](ml2)) AND
(FORALL (i: nat):
i < length(ml) IMPLIES
nth(ml, i) =
IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)
ELSIF null?(ml2) OR i >= length(ml2) THEN nth(ml1, i)
ELSE maxnum(nth(ml1, i), nth(ml2, i))
ENDIF)}" multi_polylist nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(length def-decl "nat" list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(MonoList type-eq-decl nil multi_polylist nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil))
shostak))
(max_assoc 0
(max_assoc-1 nil 3603446582
("" (induct "ml")
(("1" (grind) nil nil)
("2" (skolem 1 ("r" "l"))
(("2" (flatten)
(("2" (skeep)
(("2" (expand "max" + 4)
(("2" (lift-if)
(("2" (ground)
(("1" (expand "max" + 2) (("1" (propax) nil nil)) nil)
("2" (expand "max" + 1)
(("2" (assert)
(("2" (lift-if)
(("2" (ground)
(("1" (grind) nil nil)
("2" (expand "max" 2 1)
(("2" (assert)
(("2" (lift-if)
(("2"
(split)
(("1" (grind) nil nil)
("2"
(flatten)
(("2"
(expand "max" + 3)
(("2"
(lift-if)
(("2"
(assert)
(("2"
(lemma "max_cdr")
(("2"
(inst - "ml1" "ml2")
(("2"
(assert)
(("2"
(replaces -1)
(("2"
(inst
-
"cdr(ml1)"
"cdr(ml2)")
(("2"
(replace -1)
(("2"
(expand "maxnum")
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(lift-if)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((max_cdr formula-decl nil multi_polylist nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(ml2 skolem-const-decl "MonoList" multi_polylist nil)
(cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(list_induction formula-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)
(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)
(max def-decl "{ml |
length[nat](ml) = maxnum(length[nat](ml1), length[nat](ml2)) AND
(FORALL (i: nat):
i < length(ml) IMPLIES
nth(ml, i) =
IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)
ELSIF null?(ml2) OR i >= length(ml2) THEN nth(ml1, i)
ELSE maxnum(nth(ml1, i), nth(ml2, i))
ENDIF)}" multi_polylist nil)
(null? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(maxnum const-decl
"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylist
nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(length def-decl "nat" list_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(MonoList type-eq-decl nil multi_polylist nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil))
shostak))
(varmono_TCC1 0
(varmono_TCC1-1 nil 3603021513 ("" (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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil))
nil))
(varmono_TCC2 0
(varmono_TCC2-1 nil 3603021513 ("" (termination-tcc) nil nil) nil
nil))
(monolist_eval_rec_TCC1 0
(monolist_eval_rec_TCC1-1 nil 3604179743 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil))
nil))
(monolist_eval_rec_TCC2 0
(monolist_eval_rec_TCC2-1 nil 3604179743 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(MonoList type-eq-decl nil multi_polylist nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_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))
nil))
(monolist_eval_rec_TCC3 0
(monolist_eval_rec_TCC3-1 nil 3604179743
("" (skeep)
(("" (case-replace "length(ml) = 0")
(("1" (grind) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(list type-decl nil list_adt nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(length def-decl "nat" list_props nil)
(MonoList type-eq-decl nil multi_polylist nil)
(real_times_real_is_real application-judgement "real" reals nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(gt_realorder name-judgement "RealOrder" util nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(product def-decl "real" product "reals/"))
nil))
(monolist_eval_rec_TCC4 0
(monolist_eval_rec_TCC4-1 nil 3604179743 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil))
nil))
(monolist_eval_rec_TCC5 0
(monolist_eval_rec_TCC5-1 nil 3604179743 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(/= const-decl "boolean" notequal nil))
nil))
(monolist_eval_rec_TCC6 0
(monolist_eval_rec_TCC6-1 nil 3604179743
("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil))
nil))
(monolist_eval_rec_TCC7 0
(monolist_eval_rec_TCC7-1 nil 3604179743
("" (skeep)
((""
(typepred
"v(cdr[nat](ml), c * xvar(i) ^ car[nat](ml), i + 1)(xvar)")
(("" (case "0 < length[nat](ml)")
(("1" (rewrite "product_first" 2)
(("1" (assert)
(("1" (expand "nth" 2 1)
(("1"
(case "product(0, length(cdr[nat](ml)) - 1,
LAMBDA (k: nat):
IF k < length(cdr[nat](ml))
THEN xvar(1 + k + i) ^ nth(cdr[nat](ml), k)
ELSE 1
ENDIF) = product(1, length[nat](ml) - 1,
LAMBDA (k: nat):
IF k < length[nat](ml)
THEN xvar(k + i) ^ nth[nat](ml, k)
ELSE 1
ENDIF)")
(("1" (assert) nil nil)
("2" (hide-all-but (-1 1 2))
(("2" (expand "length" 1 3)
(("2" (expand "length" 1 4)
(("2" (lemma "product_shift_T[nat]")
(("2"
(inst -1 _ "length(cdr[nat](ml)) - 1" "0"
"1")
(("2" (assert)
(("2" (inst?)
(("1"
(expand "nth" -1 2)
(("1"
(case-replace
"(LAMBDA (i_1: nat):
IF 1 + i_1 < 1 + length[nat](cdr(ml))
THEN xvar(1 + i_1 + i) ^ nth(cdr(ml), i_1)
ELSE 1
ENDIF) = (LAMBDA (k: nat):
IF k < length(cdr[nat](ml))
THEN xvar(1 + k + i) ^ nth(cdr[nat](ml), k)
ELSE 1
ENDIF)")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2"
(decompose-equality)
(("1" (grind) nil nil)
("2" (grind) nil nil)
("3" (grind) nil nil)
("4" (grind) nil nil))
nil))
nil)
("3"
(hide-all-but 1)
(("3" (grind) nil nil))
nil)
("4"
(hide-all-but 1)
(("4" (grind) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2" (grind) nil nil))
nil)
("3"
(hide-all-but 1)
(("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide-all-but 1) (("3" (grind) nil nil)) nil)
("4" (hide-all-but 1) (("4" (grind) nil nil)) nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
nil)
("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
((car adt-accessor-decl "[(cons?) -> T]" list_adt nil)
(cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(nth def-decl "T" list_props nil)
(below type-eq-decl nil nat_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(< const-decl "bool" reals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(length def-decl "nat" list_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(product def-decl "real" product "reals/")
(T_high type-eq-decl nil product "reals/")
(T_low type-eq-decl nil product "reals/")
(<= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<< adt-def-decl "(strict_well_founded?[list])" list_adt nil)
(strict_well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(MonoList type-eq-decl nil multi_polylist nil)
(>= const-decl "bool" reals 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(every adt-def-decl "boolean" list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(= 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(product_first formula-decl nil product "reals/")
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(lt_realorder name-judgement "RealOrder" util nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(le_realorder name-judgement "RealOrder" util nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ge_realorder name-judgement "RealOrder" util nil)
(ml skolem-const-decl "MonoList" multi_polylist nil)
(xvar skolem-const-decl "[nat -> real]" multi_polylist nil)
(i skolem-const-decl "nat" multi_polylist nil)
(expt def-decl "real" exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(product_shift_T formula-decl nil product "reals/")
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(monolist_eval_prod_TCC1 0
(monolist_eval_prod_TCC1-1 nil 3603468314 ("" (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)
(PRED type-eq-decl nil defined_types nil)
(list type-decl nil list_adt nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lt_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)
(/= const-decl "boolean" notequal nil))
nil))
(monolist_eval_prod 0
(monolist_eval_prod-1 nil 3603468325
("" (skeep)
(("" (expand "monolist_eval")
(("" (typepred "monolist_eval_rec(ml, 1, 0)(xvar)")
(("" (assert) nil nil)) nil))
nil))
nil)
((monolist_eval const-decl "real" multi_polylist 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_times_real_is_real application-judgement "real" reals 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(list type-decl nil list_adt nil)
(PRED type-eq-decl nil defined_types nil)
(every adt-def-decl "boolean" list_adt nil)
(AND const-decl "[bool, bool -> bool]" 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)
(>= const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil product "reals/")
(T_high type-eq-decl nil product "reals/")
(product def-decl "real" product "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(length def-decl "nat" list_props nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(< const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil nat_types nil)
(nth def-decl "T" list_props nil)
(monolist_eval_rec def-decl "{r: real |
r =
c *
product(0, length(ml) - 1,
LAMBDA (k: nat):
IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)
ELSE 1
ENDIF)}" multi_polylist nil))
shostak))
(monosum_TCC1 0
(monosum_TCC1-1 nil 3603023858
("" (skeep*)
(("" (expand "monolist_eval")
(("" (expand "monolist_eval_rec" + 2) (("" (assert) nil nil))
nil))
nil))
nil)
((monolist_eval const-decl "real" multi_polylist nil)
(real_times_real_is_real application-judgement "real" reals nil)
(monolist_eval_rec def-decl "{r: real |
r =
c *
product(0, length(ml) - 1,
LAMBDA (k: nat):
IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)
ELSE 1
ENDIF)}" multi_polylist nil))
nil))
(monosum_TCC2 0
(monosum_TCC2-1 nil 3603023858
("" (skeep*)
(("" (expand "monolist_eval")
(("" (expand "monolist_eval_rec" + 3) (("" (assert) nil nil))
nil))
nil))
nil)
((monolist_eval const-decl "real" multi_polylist nil)
(real_times_real_is_real application-judgement "real" reals nil)
(monolist_eval_rec def-decl "{r: real |
r =
c *
product(0, length(ml) - 1,
LAMBDA (k: nat):
IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)
ELSE 1
ENDIF)}" multi_polylist nil))
nil))
(monosum_TCC3 0
(monosum_TCC3-3 "" 3604248507
("" (skeep*)
(("" (typepred "v(cdr[nat](ml1), cdr[nat](ml2))")
(("" (hide -1)
(("" (inst -1 "LAMBDA(i:nat):xvar(i+1)")
(("" (expand "monolist_eval")
(("" (expand "monolist_eval_rec" + 1)
((""
(typepred
"monolist_eval_rec(v(cdr[nat](ml1), cdr[nat](ml2)),
1 * xvar(0) ^ (car[nat](ml1) + car[nat](ml2)), 1)
(xvar)")
(("" (replaces -1)
(("" (expand "monolist_eval_rec" +)
(("" (assert)
((""
(typepred
"monolist_eval_rec(cdr(ml1), 1 * xvar(0) ^ car(ml1), 1)(xvar)")
(("" (replaces -1)
((""
(typepred
"monolist_eval_rec(cdr(ml2), 1 * xvar(0) ^ car(ml2), 1)(xvar)")
(("" (replaces -1)
((""
(case
"FORALL (x:real,j,k:nat): x^(j+k) = x^j*x^k")
(("1"
(inst?)
(("1"
(replaces -1)
(("1"
(typepred
"monolist_eval_rec(cdr[nat](ml1), 1, 0)(LAMBDA (i: nat): xvar(1 + i))")
(("1"
(typepred
"monolist_eval_rec(cdr[nat](ml2), 1, 0)(LAMBDA (i: nat): xvar(1 + i))")
(("1"
(replaces (-1 -2) :dir rl)
(("1"
(typepred
"monolist_eval_rec(v(cdr[nat](ml1), cdr[nat](ml2)), 1, 0)
(LAMBDA (i: nat): xvar(1 + i))")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(lemma "expt_plus")
(("2"
(case
"FORALL (j,k:nat): 0^(j+k) = 0^j*0^k")
(("1"
(skeep)
(("1"
(case "x = 0")
(("1"
(inst - "j" "k")
(("1" (assert) nil nil))
nil)
("2"
(inst - "j" "k" "x")
(("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2"
(case "k = 0")
(("1"
(replaces -1)
(("1" (grind) nil nil))
nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil)
(cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(monolist_eval const-decl "real" multi_polylist nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(length def-decl "nat" list_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(MonoList type-eq-decl nil multi_polylist nil)
(>= const-decl "bool" reals 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.76 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.
|
