Impressum multi_polylist.prf
Sprache: Lisp
(multi_polylistnil 3603213169 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil ))nil ))nil 3603213169 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))nil 3603199783 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"nat" list_props nil )nil integers nil )nil naturalnumbers nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil ))nil ))nil 3603207043 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"nat" list_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"posint" nil )"(total_order?[real])" nil )"RealOrder" util nil )nil integers nil )nil naturalnumbers nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil ))nil ))nil 3603207043 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )nil integers nil )nil naturalnumbers nil ))nil ))nil 3603207043 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )nil integers nil )nil naturalnumbers nil ))nil ))nil 3603207043 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"(total_order?[real])" nil )"RealOrder" util nil )"nat" list_props nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil ))nil ))nil 3603207043 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"posint" nil )"(total_order?[real])" nil )"RealOrder" util nil )"nat" list_props nil )nil naturalnumbers nil )nil integers nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil ))nil ))nil 3603207043 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil ))nil ))nil 3603210536 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil ))nil ))nil 3603210536 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"nat" list_props nil )"posint" nil )"posint" nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil ))nil ))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" "v(cdr[nat](ml1), cdr[nat](ml2))" )"4" (inst - "i-1" )"4" (assert )"4" (lift-if)"4" "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" "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" "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" nil )"(total_order?[real])" nil )"RealOrder" util nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )"[bool, bool -> bool]" booleans nil )nil nat_types nil )"T" list_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[list -> boolean]" list_adt nil )"[list -> boolean]" list_adt nil )"[(cons?) -> list]" list_adt nil )"nat" list_props nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"int" integers nil ))nil ))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 )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )max def-decl "{ml | AND IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)OR i >= length(ml2) THEN nth(ml1, i)" multi_polylist nil) "[list -> boolean]" list_adt nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T" list_props nil )nil nat_types nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )OR const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"[T, T -> boolean]" equalities nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ))nil 3603447297 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )max def-decl "{ml | AND IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)OR i >= length(ml2) THEN nth(ml1, i)" multi_polylist nil) "(total_order?[real])" nil )"RealOrder" util nil ))nil ))nil 3603447298"" case "FORALL (ml1, ml2: MonoList,r1,r2:real): 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 )"(total_order?[real])" nil )"RealOrder" util nil )nil list_adt nil )NOT const-decl "[bool -> bool]" booleans nil )"[(cons?) -> T]" list_adt nil )nil numbers nil )nil list_adt nil )nil booleans nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil naturalnumbers nil )"[list -> boolean]" list_adt nil )"[(cons?) -> list]" list_adt nil )"nat" list_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[list -> boolean]" list_adt nil )max def-decl "{ml | AND IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)OR i >= length(ml2) THEN nth(ml1, i)" multi_polylist nil) "[[T, list] -> (cons?)]" list_adt nil ))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 )"[list -> boolean]" list_adt nil )"[(cons?) -> T]" list_adt nil )"[(cons?) -> list]" list_adt nil )"(total_order?[real])" nil )"RealOrder" util nil )NOT const-decl "[bool -> bool]" booleans nil )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )max def-decl "{ml | AND IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)OR i >= length(ml2) THEN nth(ml1, i)" multi_polylist nil) "[list -> boolean]" list_adt nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T" list_props nil )nil nat_types nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )OR const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"[T, T -> boolean]" equalities nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ))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" "1" (grind) nil nil )"2" "2" expand "max" + 3)"2" "2" assert )"2" "max_cdr" )"2" "ml1" "ml2" )"2" assert )"2" "2" "cdr(ml1)" "cdr(ml2)" )"2" replace -1)"2" expand "maxnum" )"2" "2" "2" "2" "2" "2" "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 )nil multi_polylist nil )"(total_order?[real])" nil )"RealOrder" util nil )"[list -> boolean]" list_adt nil )"MonoList" multi_polylist nil )"[(cons?) -> list]" list_adt nil )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )max def-decl "{ml | AND IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)OR i >= length(ml2) THEN nth(ml1, i)" multi_polylist nil) "[list -> boolean]" list_adt nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T" list_props nil )nil nat_types nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )OR const-decl "[bool, bool -> bool]" booleans nil )"nat" list_props nil )"[T, T -> boolean]" equalities nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ))nil 3603021513 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))nil 3603021513 ("" (termination-tcc) nil nil ) nil nil ))nil 3604179743 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))nil 3604179743 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil multi_polylist nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))nil 3604179743"" (skeep)"" (case-replace "length(ml) = 0" )"1" (grind) nil nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"nat" list_props nil )nil multi_polylist nil )"real" reals nil )"odd_int" integersnil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"real" product "reals/" ))nil ))nil 3604179743 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil ))nil ))nil 3604179743 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"RealOrder" util nil )"boolean" notequal nil ))nil ))nil 3604179743"" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"(strict_well_founded?[list])" list_adt nil ))nil ))nil 3604179743"" (skeep)"" "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))LAMBDA (k: nat):IF k < length[nat](ml)") "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" "length(cdr[nat](ml)) - 1" "0" "1" )"2" (assert )"2" (inst?)"1" expand "nth" -1 2)"1" "(LAMBDA (i_1: nat): IF 1 + i_1 < 1 + length[nat](cdr(ml))LAMBDA (k: nat):IF k < length(cdr[nat](ml))") "1" (assert ) nil nil )"2" "2" "1" (grind) nil nil )"2" (grind) nil nil )"3" (grind) nil nil )"4" (grind) nil nil ))nil ))nil )"3" "3" (grind) nil nil ))nil )"4" "4" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "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 )"[(cons?) -> T]" list_adt nil )"[(cons?) -> list]" list_adt nil )"[list -> boolean]" list_adt nil )"T" list_props nil )nil nat_types nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"boolean" notequal nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" product "reals/" )nil product "reals/" )nil product "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(strict_well_founded?[list])" list_adt nil )"bool" orders nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )nil multi_polylist nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"[bool, bool -> bool]" booleans nil )nil product "reals/" )"int" integers nil )"nonneg_int" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"posint" nil )"odd_int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil )"MonoList" multi_polylist nil )"[nat -> real]" multi_polylist nil )"nat" multi_polylist nil )"real" exponentiation nil )"int" integers nil )nil product "reals/" )"real" reals nil ))nil ))nil 3603468314 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )nil integers nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"boolean" notequal nil ))nil ))nil 3603468325"" (skeep)"" (expand "monolist_eval" )"" (typepred "monolist_eval_rec(ml, 1, 0)(xvar)" )"" (assert ) nil nil )) nil ))nil ))nil )"real" multi_polylist nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"int" integers nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )nil integers nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product "reals/" )nil product "reals/" )"real" product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nat" list_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"boolean" notequal nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"T" list_props nil )"{r: real | LAMBDA (k: nat):IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)" multi_polylist nil)) nil 3603023858"" (skeep*)"" (expand "monolist_eval" )"" (expand "monolist_eval_rec" + 2) (("" (assert ) nil nil ))nil ))nil ))nil )"real" multi_polylist nil )"real" reals nil )"{r: real | LAMBDA (k: nat):IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)" multi_polylist nil)) nil ))nil 3603023858"" (skeep*)"" (expand "monolist_eval" )"" (expand "monolist_eval_rec" + 3) (("" (assert ) nil nil ))nil ))nil ))nil )"real" multi_polylist nil )"real" reals nil )"{r: real | LAMBDA (k: nat):IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)" multi_polylist nil)) nil ))"" 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)"" "monolist_eval_rec(v(cdr[nat](ml1), cdr[nat](ml2)), ") "" (replaces -1)"" (expand "monolist_eval_rec" +)"" (assert )"" "monolist_eval_rec(cdr(ml1), 1 * xvar(0) ^ car(ml1), 1)(xvar)" )"" (replaces -1)"" "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" "1" "1" "monolist_eval_rec(cdr[nat](ml1), 1, 0)(LAMBDA (i: nat): xvar(1 + i))" )"1" "monolist_eval_rec(cdr[nat](ml2), 1, 0)(LAMBDA (i: nat): xvar(1 + i))" )"1" "1" "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" "2" "expt_plus" )"2" case "FORALL (j,k:nat): 0^(j+k) = 0^j*0^k" )"1" "1" case "x = 0" )"1" "j" "k" )"1" (assert ) nil nil ))nil )"2" "j" "k" "x" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "2" case "k = 0" )"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 )"[(cons?) -> list]" list_adt nil )"[list -> boolean]" list_adt nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_polylist nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil naturalnumbers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil multi_polylist nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil list_adt nil )nil defined_types nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"{r: real | LAMBDA (k: nat):IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)" multi_polylist nil) "(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"int" integers nil )"nat" exponentiation nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" multi_polylist nil )nil reals nil )"int" integers nil )"even_int" integersnil )"nat" exponentiation nil )"nzrat" rationalsnil )"RealOrder" util nil )"(total_order?[real])" nil )"real" exponentiation nil )nil exponentiation nil )"posint" nil )"nonneg_int" nil )"real" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil product "reals/" )nil product "reals/" )"real" product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"boolean" notequal nil )"real" exponentiation nil )nil nat_types nil )"T" list_props nil )"[(cons?) -> T]" list_adt nil ))nil 3603036932 ("" (subtype-tcc) nil nil )nil multi_polylist nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil list_adt nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3603036932 ("" (termination-tcc) nil nil )"nat" list_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )nil multi_polylist nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil list_adt nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3603036932 ("" (subtype-tcc) nil nil ) nil nil ))nil 3603455463 ("" (subtype-tcc) nil nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))nil 3603455464"" (induct "mpl" )"1" (grind) nil nil )"2" (skolem 1 ("T" "L" ))"2" (flatten)"2" (skeep)"2" (inst - "xvar" )"2" (expand "meval" +)"2" (lemma "sigma_split" )"2" (expand "length" + 1)"2" (assert )"2" (invoke (inst - "%1" _ _ _) (! 1 2 3))"2" (inst?)"2" (inst - "0" )"2" (assert )"2" (replaces -1)"2" expand "sigma" + 1)"2" expand "sigma" + 1)"2" assert )"2" expand "length" + 1)"2" expand "nth" + 3)"2" expand "nth" + 3)"2" "2" case "FORALL (k:nat): sigma(0, k, LAMBDA (i: nat):IF i < length(L)LAMBDA (i: nat):IF i < length(cons(T, L))") "1" "length(L)-1" )"1" (assert ) nil nil )"2" assert )nil nil ))nil )"2" "2" "k" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" assert )"1" "1" "1" "1" "1" nil nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "k" )"2" "2" assert )"2" expand "sigma" "2" "2" assert )"2" "2" "2" "2" 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 )"3" (hide 2)"3" (skosimp*)"3" (inst + "10" ) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma_nat "reals/" )"int" integers nil )"list[[real, MonoList]]" multi_polylist nil )"RealOrder" util nil )"(total_order?[real])" nil )nil defined_types nil )nil naturalnumbers nil )"odd_int" integers nil )"posint" nil )"odd_int" integersnil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil sigma "reals/" )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil list_adt nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"real" multi_polylist nil )"T" list_props nil )nil nat_types nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" multi_polylist nil )"[T, T -> boolean]" equalities nil )nil multi_polylist nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )"int" integers nil )"real" reals nil ))nil 3603214067 ("" (subtype-tcc) nil nil )nil more_list_props "structures/" )) nil ))nil 3603214067"" (skeep)"" (skeep)"" (split)"1" (typepred "i" )"1" (case "NOT i = 0" )"1" (grind) nil nil )"2" (replaces -1)"2" (expand "nth" ) (("2" (rewrite "max_id" ) nil nil ))nil ))nil ))nil ))nil )"2" (typepred "i" )"2" (case "NOT i = 0" )"1" (grind) nil nil )"2" (replaces -1)"2" (expand "nth" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"RealOrder" util nil )"(total_order?[real])" nil )nil naturalnumbers nil )nil multi_polylist nil )"nat" list_props nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[(cons?) -> T]" list_adt nil )"[list -> boolean]" list_adt nil )nil multi_polylist nil )"posint" nil )"T" list_props nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3603214067"" (skeep) (("" (expand "length" + 2) (("" (assert ) nil nil )) nil ))nil )"nat" list_props nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"posint" nil ))nil ))nil 3603214067"" (skeep)"" (skeep)"" (typepred "v(cdr[[real, MonoList]](mpl))" )"1" (hide -1)"1" (assert )"1" (split)"1" (case "i = 0" )"1" (replaces -1)"1" (expand "nth" +)"1" (assert )"1" case "FORALL (l1,l2:list[nat]): max(l1,l2) = max(l1,max(l1,l2))" )"1" (inst?) nil nil )"2" (hide-all-but 1)"2" (induct "l1" )"1" (grind) nil nil )"2" (skolem 1 ("r" "l" ))"2" "2" "2" expand "max" +)"2" assert )"2" "2" "2" "2" "1" expand "maxnum" +)"1" rewrite "max_id" +)nil nil ))nil )"2" case "maxnum(r, maxnum(r, car(l2))) = maxnum(r,car(l2))" )"1" replace -1)"1" assert )"1" "cdr(l2)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (name "V" "v(cdr[[real, MonoList]](mpl))" )"2" (replace -1)"2" (inst - "i-1" )"1" (expand "nth" +)"1" (flatten)"1" (assert )"1" rewrite "max_assoc" +)"1" "max_sym" )"1" "nth(cdr(mpl), i - 1)`2" "car[[real, MonoList]](mpl)`2" )"1" replace -1)"1" rewrite "max_assoc" + :dir rl)"1" "max_sym" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (typepred "i" )"2" (expand "length" -1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "max(car[[real, MonoList]](mpl)`2, ") "2" (replace -2)"2" (assert )"2" (case "i = 0" )"1" (replaces -1)"1" (expand "nth" 1)"1" (assert ) nil nil )) nil ))nil )"2" (inst -4 "i-1" )"1" (expand "nth" 2)"1" (assert ) nil nil )) nil )"2" (assert )"2" (typepred "i" )"2" expand "length" -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "length" 1 2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"posint" nil )"posint" nil )nil multi_polylist nil )nil multi_polylist nil )"below(length(mpl))" multi_polylist nil )"MultiPolyList" multi_polylist nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )nil multi_polylist nil )"RealOrder" util nil )"(total_order?[real])" nil )nil list_adt nil )"[(cons?) -> T]" list_adt nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )nil multi_polylist nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"nat" list_props nil )"[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )nil nat_types nil )"T" list_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )max def-decl "{ml | AND IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)OR i >= length(ml2) THEN nth(ml1, i)" multi_polylist nil) "[list -> boolean]" list_adt nil )"[(cons?) -> list]" list_adt nil ))nil ))nil 3603531482"" (induct "mpl" )"1" (grind) nil nil )"2" (skolem 1 ("rp" "lmp" ))"2" (flatten)"2" (skeep)"2" (case "i = 0" )"1" (assert )"1" (replaces -1)"1" (expand "degree" -2)"1" (lift-if)"1" (expand "nth" 1)"1" (ground)"1" (hide -2)"1" (expand "max" -1)"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (expand "max" -1)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (split -1)"1" (inst - "i-1" )"1" (assert )"1" (split -1)"1" (expand "nth" +) (("1" (propax) nil nil ))nil )"2" (expand "length" -2) (("2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert )"2" (expand "degree" -1)"2" (lift-if)"2" (ground)"1" (expand "degree" 1)"1" (propax) nil nil )) nil )"2" (expand "max" -1)"2" (lift-if) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"nat" multi_polylist nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"RealOrder" util nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil list_adt nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"{ml | NOT null?(mpl)) IMPLIESmax (nth(mpl, i)`2, ml) AND " multi_polylist nil )max def-decl "{ml | AND IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)OR i >= length(ml2) THEN nth(ml1, i)" multi_polylist nil) IF const-decl "[boolean, T, T -> T]" if_def nil )"T" list_props nil )nil nat_types nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"nat" list_props nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )nil naturalnumbers nil )nil integers nil )"[bool, bool -> bool]" booleans nil )nil multi_polylist nil ))nil 3603451460 ("" (subtype-tcc) nil nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil ))nil ))nil 3603033743"" (skeep)"" (skeep)"" (expand "meval" +)"" (assert )"" (expand "meval" + 1) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"real" reals nil )"real" multi_polylist nil ))nil ))nil 3603033743"" (skeep)"" (assert )"" (flatten)"" (replaces -1)"" (replaces -3)"" (assert ) (("" (skeep) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"real" multi_polylist nil ))nil ))nil 3603033743 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil ))nil ))nil 3603033743 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" ordinals nil )"posint" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"nat" list_props nil )"ordinal" lex2 nil ))nil ))nil 3603033743"" (skeep)"" (skeep)"" (assert )"" (hide 3)"" "v(null[[real, MonoList]], cdr[[real, MonoList]](swiped), ") "" (rewrite -1)"" (hide -1)"" (expand "meval" + 3)"" (expand "meval" + 2)"" (expand "meval" + 3)"" (expand "meval" + 2) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil multi_polylist nil )nil multi_polylist nil )"real" multi_polylist nil )nil ordstruct_adt nil )"bool" ordinals nil )"bool" ordinals nil )nil ordinals nil )"ordinal" lex2 nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_polylist nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"[(cons?) -> list]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[(cons?) -> T]" list_adt nil )"real" reals nil )"real" reals nil ))nil ))nil 3603033743 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil ))nil ))nil 3603033743 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" ordinals nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"posint" nil )"boolean" notequal nil )"nat" list_props nil )"ordinal" lex2 nil ))nil ))nil 3603033743"" (skeep)"" (skeep)"" "v(null[[real, MonoList]], cdr[[real, MonoList]](swiped), ans, ") "" (rewrite -1)"" (hide -1)"" (expand "meval" + 3)"" (assert )"" (hide 3)"" (expand "meval" + 3)"" (flatten)"" (replaces -2)"" (assert )"" (expand "meval" + 2)"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil multi_polylist nil )nil multi_polylist nil )"real" multi_polylist nil )nil ordstruct_adt nil )"bool" ordinals nil )"bool" ordinals nil )nil ordinals nil )"ordinal" lex2 nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_polylist nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"[(cons?) -> list]" list_adt nil )"[(cons?) -> T]" list_adt nil )"real" reals nil )"real" reals nil ))nil ))nil 3603033743 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil ))nil ))nil 3603033743 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"posint" nil )"nonneg_int" nil )"nat" list_props nil )"bool" ordinals nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"odd_int" integers nil )"boolean" notequal nil )"ordinal" lex2 nil ))nil ))nil 3603033743"" (skeep)"" (skeep)"" "v(swiped, cdr[[real, MonoList]](toswipe), ans, mono, ") "" (rewrite -1)"" (hide -1)"" (assert )"" (hide (2 3 4))"" (assert )"" "monolist_eval(mono)(xvar) * thiscoeff" 2)"" (assert )"" case "NOT meval(toswipe)(xvar) - monolist_eval(mono)(xvar) * thiscoeff + ") "1" (assert ) nil nil )"2" (replaces -1)"2" (expand "meval" + 2)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil multi_polylist nil )nil multi_polylist nil )"real" multi_polylist nil )nil ordstruct_adt nil )"bool" ordinals nil )"bool" ordinals nil )nil ordinals nil )"ordinal" lex2 nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_polylist nil )"[list -> boolean]" list_adt nil )"[(cons?) -> list]" list_adt nil )"[(cons?) -> T]" list_adt nil )"real" reals nil )"real" reals nil ))nil ))nil 3603033743 ("" (termination-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"bool" ordinals nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"odd_int" integers nil )"odd_int" integersnil )"boolean" notequal nil )"nat" list_props nil )"ordinal" lex2 nil )"posint" nil ))nil ))nil 3603033743"" (skeep)"" (skeep)"" "v(cons[[real, MonoList]] ") "" (rewrite -1)"" (hide -1)"" (assert )"" (hide (3 4 5))"" (expand "meval" + 2)"" (expand "meval" + 2) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil multi_polylist nil )nil multi_polylist nil )"real" multi_polylist nil )nil ordstruct_adt nil )"bool" ordinals nil )"bool" ordinals nil )nil ordinals nil )"ordinal" lex2 nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_polylist nil )"[list -> boolean]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[(cons?) -> T]" list_adt nil )"[(cons?) -> list]" list_adt nil )"real" reals nil )"real" reals nil ))nil ))nil 3603028950"" (skeep)"" (assert )"" "mp_simp_rec(null[[real, MonoList]], mpl, ") "" (decompose-equality +)"" (inst - "x!1" )"" (replaces -1)"" (expand "meval" + 3) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil multi_polylist nil )nil multi_polylist nil )"real" multi_polylist nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_polylist nil )"{mpl | " multi_polylist nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"[(cons?) -> T]" list_adt nil )"real" reals nil ))nil ))nil 3603035287 ("" (grind) nil nil )"boolean" list_adt nil )) nil ))nil 3603036932"" case "FORALL (mpl1: MultiPolyList, mpl2: MultiPolyList): ") "1" (skeep)"1" (insteep -1)"1" "mp_simp(append[[real, MonoList]](mpl1, mpl2))" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "mpl1" )"1" (expand "+" )"1" (skeep)"1" (decompose-equality +)"1" (expand "append" )"1" (expand "meval" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skolem 1 ("X" "L" ))"2" (flatten)"2" (skeep)"2" (expand "append" +)"2" (expand "meval" + 1)"2" (decompose-equality +)"2" (inst - "mpl2" )"2" (decompose-equality -)"2" (inst - "x!1" )"2" (expand "+" )"2" (expand "meval" + 2)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[[T, list] -> (cons?)]" list_adt nil )"[list -> boolean]" list_adt nil )"real" multi_polylist nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil list_adt nil )"{mulist: MultiPolyList | meval(mpl) = meval(mulist)}" nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil list_adt nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )nil multi_polylist nil )nil integers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"real" multi_polylist nil )"list[T]" list_props nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3603106487 ("" (grind) nil nil )"real" reals nil )"real" multi_polylist nil ))nil ))nil 3603106487 ("" (grind) nil nil )"real" multi_polylist nil )"real" reals nil )"real" reals nil )"real" multi_polylist nil ))nil ))nil 3603106487 ("" (grind) nil nil ) nil nil ))nil 3603106487 ("" (grind) nil nil )"boolean" list_adt nil )) nil ))nil 3603106487"" (skeep)"" (skeep)"" (expand "meval" + 1)"" (expand "meval" + 1)"" (expand "meval" )"" (assert )"" "monosum(car[[real, MonoList]](mpl1)`2, ") "" (hide -1)"" (rewrite -1)"" (assert )"" (hide -1)"" (expand "meval" +) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )nil integers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"real" multi_polylist nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{pml2: MonoList | " nil )"[list -> boolean]" list_adt nil )"[(cons?) -> T]" list_adt nil )nil multi_polylist nil )"real" multi_polylist nil )"real" reals nil ))nil ))nil 3603106487 ("" (termination-tcc) nil nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"posint" nil )"nat" list_props nil ))nil ))nil 3603106487 ("" (termination-tcc) nil nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"posint" nil )"nonneg_int" nil )"nat" list_props nil ))nil ))nil 3603106487"" (skeep)"" (skeep)"" (assert )"" (expand "+" )"" "mpsum(v(mpl1, cdr[[real, MonoList]](mpl2)), ") "" (replaces -1)"" (assert )"" (expand "+" )"" (assert )"" "v(mpl1, cdr[[real, MonoList]](mpl2))" )"" (rewrite -1)"" (hide -1)"" (assert )"" "v(mpl1, (: car[[real, MonoList]](mpl2) :))" )"" rewrite -1)"" "" assert )"" expand "meval" + 4)"" assert )"" case "meval(cdr[[real, MonoList]](mpl2))(xvar) + ") "1" (assert ) nil nil )"2" "2" expand "meval" + 2)"2" expand "meval" + 2)"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 )"MultiPolyList" multi_polylist nil )"real" multi_polylist nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil multi_polylist nil )nil multi_polylist nil )"real" multi_polylist nil )"[T -> real]" real_fun_ops "reals/" )"{mpl | meval(mpl) = meval(mpl1) + meval(mpl2)}" nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[list -> boolean]" list_adt nil )"[(cons?) -> list]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[(cons?) -> T]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"real" reals nil ))nil ))nil 3603106487 ("" (termination-tcc) nil nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"posint" nil )"posint" nil )"nat" list_props nil ))nil ))nil 3603106487 ("" (termination-tcc) nil nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"posint" nil )"nonneg_int" nil )"nat" list_props nil ))nil ))nil 3603106487"" (skeep)"" (skeep)"" (expand "+" )"" "mpsum(v(cdr[[real, MonoList]](mpl1), mpl2), ") "" (replace -1)"" (hide -1)"" (expand "+" )"" (typepred "v(cdr[[real, MonoList]](mpl1), mpl2)" )"" (rewrite -1)"" (hide -1)"" "v((: car[[real, MonoList]](mpl1) :), mpl2)" )"" (rewrite -1)"" (hide -1)"" (assert )"" "" expand "meval" + 3)"" expand "meval" + 4)"" assert )"" expand "meval" + 4)"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"[(cons?) -> T]" list_adt nil )"[[T, list] -> (cons?)]" list_adt nil )"[(cons?) -> list]" list_adt nil )"[list -> boolean]" list_adt nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"{mpl | meval(mpl) = meval(mpl1) + meval(mpl2)}" nil )"[T -> real]" real_fun_ops "reals/" )"real" multi_polylist nil )nil multi_polylist nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"real" reals nil )"MultiPolyList" multi_polylist nil ))nil ))nil 3603041774"" (skeep)"" (skeep)"" (typepred "mp_simp(mpprod_rec(mpl1, mpl2))" )"" (replaces -1 :dir rl)"" (typepred "mpprod_rec(mpl1, mpl2)" )"" (rewrite -1) nil nil )) nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil multi_polylist nil )nil multi_polylist nil )"real" multi_polylist nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{mpl | " nil )"{mulist: MultiPolyList | meval(mpl) = meval(mulist)}" nil ))nil ))nil 3603108317"" (skeep) (("" (expand "length" + 2) (("" (assert ) nil nil )) nil ))nil )"nat" list_props nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"posint" nil ))nil ))nil 3603099886 ("" (grind) nil nil )"boolean" list_adt nil )) nil ))nil 3603453411 ("" (subtype-tcc) nil nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3603454251"" (skeep)"" (case "null?(mpl)" )"1" (expand "meval" + 1)"1" (assert )"1" (expand "multipoly_to_mpoly" + 4)"1" (assert )"1" (case "length(mpl)=0" )"1" (assert )"1" (expand "multipoly_to_mpoly" + 3)"1" (expand "multipoly_eval" )"1" (expand "sigma" )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (case "length(mpl)=0" )"1" (hide 2) (("1" (grind) nil nil )) nil )"2" (rewrite "meval_sigma" )"2" (expand "multipoly_eval" + 1)"2" (expand "multipoly_to_mpoly" + 1)"2" (assert )"2" (rewrite "sigma_eq" )"2" (hide 4)"2" (skolem 1 "t" )"2" case "monolist_eval(nth(mpl, t)`2)(xvar) = max (length(degree(mpl)), 1))") "1" (expand "multipoly_to_mpoly" + 1)"1" (assert ) nil nil )) nil )"2" (hide 2)"2" (rewrite "monolist_eval_prod" )"2" (expand "polyproduct_eval" )"2" expand "multipoly_to_mpoly" + 2)"2" case "length(degree(mpl))=0" )"1" case "degree(mpl) = null" )"1" replace -1)"1" assert )"1" expand "max" )"1" expand "list2array" + 1)"1" expand "multipoly_to_mpoly" "1" assert )"1" expand "product" "1" expand "product" "1" "degree_zero" )"1" "1" assert )"1" "t" )"1" assert )"1" expand "length" "1" expand "product" "1" expand "multipoly_to_poly" "1" expand "polynomial" )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "degree" )nil nil ))nil ))nil )"2" expand "max" )"2" assert )"2" case "null?(degree(mpl))" )"1" "1" "degree" )nil nil ))nil )"2" "AA" "%1" )"1" "1" "product_split[nat]" )"1" "1" expand "AA" )"1" "length(nth(mpl, t)`2) - 1" )"1" assert )"1" "1" case "FORALL (k:nat): product(length(nth(mpl, t)`2), k, LAMBDA (i: nat):") "1" "1" assert )"1" "1" assert )"1" "1" rewrite "product_eq" )"1" "1" "1" expand "multipoly_to_mpoly" )"1" expand "polynomial" )"1" "sigma_eq_one_arg" )"1" "1" "nth(nth(mpl, t)`2, n)" )"1" assert )"1" "1" "1" expand "multipoly_to_poly" )"1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "list2array_sound[nat]" )"2" "2" assert )"2" "2" "2" "1" "degree(mpl)" )"1" assert )"1" "1" "t" )"1" "1" assert )"1" "max(nth(mpl, t)`2, degree(mpl))" )"1" "n" )"1" assert )"1" "1" "1" "n" )"1" "1" "nth" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n" )"2" "degree(mpl)" )"2" assert )"2" "t" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "i!1" )"3" "3" assert )"3" "1" "1" assert )"1" expand "multipoly_to_poly" )"1" "1" "1" "n" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "multipoly_to_poly" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" expand "multipoly_to_poly" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "2" rewrite "product_1" )"2" "2" "2" "n" )"2" expand "multipoly_to_mpoly" )"2" expand "multipoly_to_poly" )"2" expand "polynomial" )"2" "sigma_eq_one_arg" )"2" "2" "0" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "degree(mpl)" )"2" "2" assert )"2" "t" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "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 multi_polylist nil )"[list -> boolean]" list_adt nil )nil multi_polylist nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil list_adt nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"real" multi_polynomial nil )"real" sigma "reals/" )"nat" list_props nil )nil naturalnumbers nil )nil integers nil )"[T, T -> boolean]" equalities nil )"MPoly" multi_polylist nil )"real" multi_polylist nil )nil multi_polylist nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )nil sigma "reals/" )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"T" list_props nil )"real" multi_polylist nil )nil util nil )nil util nil )nil util nil )nil integers nil )nil MPoly nil )nil util nil )nil util nil )nil integers nil )"bool" reals nil ) (Vars type-eq-decl nil util nil )"real" multi_polynomial nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"{z: nat | z >= x AND z >= y AND (z = x OR z = y)}" multi_polylistnil )max def-decl "{ml | AND IF null?(ml1) OR i >= length(ml1) THEN nth(ml2, i)OR i >= length(ml2) THEN nth(ml1, i)" multi_polylist nil) "{ml | NOT null?(mpl)) IMPLIESmax (nth(mpl, i)`2, ml) AND " multi_polylist nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"real" product "reals/" )nil multi_polylist nil )"[real -> real]" polynomials "reals/" )"real" multi_polylist nil )"T" array2list "structures/" )nil more_list_props "structures/" )"{k: int | i <= k AND j <= k}" nil )"(null?)" list_adt nil )"real" exponentiation nil )"boolean" notequal nil )nil product "reals/" )nil product "reals/" )nil product "reals/" )"real" multi_polylist nil )"odd_int" integersnil )nil product "reals/" )nil array2list "structures/" )"real" exponentiation nil )nil sigma "reals/" )nil product "reals/" )nil sequences nil )nil multi_polylist nil )"(total_order?[real])" nil )"RealOrder" util nil )nil integers nil )"real" reals nil )"posint" nil ))nil 3603035288 ("" (grind) nil nil )"MultiPolyList" multi_polylist nil )"{r: real | LAMBDA (k: nat):IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)" multi_polylist nil) "real" multi_polylist nil )"real" multi_polylist nil ))nil 3603035287 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))"" 3604251987"" (induct "i" )"1" (skeep)"1" (expand "mpmonom" )"1" (expand "meval" )"1" (expand "meval" )"1" (expand "varmono" )"1" (expand "monolist_eval" )"1" (expand "monolist_eval_rec" )"1" (expand "monolist_eval_rec" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep*)"2" (inst - "c" "n" "LAMBDA(i:nat):xvar(i+1)" )"2" (expand "mpmonom" )"2" (expand "varmono" +)"2" (expand "meval" +)"2" (expand "meval" + 1)"2" (expand "meval" -)"2" (expand "meval" - 1)"2" (expand "monolist_eval" +)"2" (expand "monolist_eval_rec" )"2" (expand "^" + 1)"2" (expand "expt" )"2" (expand "monolist_eval" )"2" "monolist_eval_rec(varmono(j, n), 1, 0)(LAMBDA (i: nat): xvar(1 + i))" )"2" "monolist_eval_rec(varmono(j, n), 1, 1)(xvar)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil product "reals/" )nil product "reals/" )"real" product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nat" list_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"MonoList" multi_polylist nil )"{r: real | LAMBDA (k: nat):IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)" multi_polylist nil) "real" reals nil )"real" multi_polylist nil )nil naturalnumbers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"MultiPolyList" multi_polylist nil )"real" multi_polylist nil )nil multi_polylist nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3604151425"" (skeep)"" (expand "mpvar" )"" (rewrite "multipolylist_monom" )"" (rewrite "expt_x1" ) nil nil )) nil ))nil ))nil )"MultiPolyList" multi_polylist nil )nil exponentiation nil )"real" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil multi_polylist nil ))nil 3604151480"" (skeep)"" (expand "mpvarn" )"" (rewrite "multipolylist_monom" ) (("" (assert ) nil nil ))nil ))nil ))nil )"MultiPolyList" multi_polylist nil )"real" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil multi_polylist nil ))nil 3603108095"" (skeep)"" (typepred "mpsum(mpl1,mpl2)" )"" (assert )"" (decompose-equality -)"" (inst - "xvar" )"" (expand "+" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"{mpl | meval(mpl) = meval(mpl1) + meval(mpl2)}" nil )"[T -> real]" real_fun_ops "reals/" )"real" multi_polylist nil )nil multi_polylist nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil ))nil 3603108126"" (skeep)"" (typepred "mpprod(mpl1,mpl2)" ) (("" (inst?) nil nil )) nil ))nil )"{mpl | " nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" multi_polylist nil )nil multi_polylist nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3603108154"" (induct "mpl" )"1" (grind) nil nil )"2" (skolem 1 ("X" "L" ))"2" (flatten)"2" (skeep)"2" (expand "mpscal" +)"2" (expand "meval" +)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil list_adt nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil list_adt nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"MultiPolyList" multi_polylist nil )"real" multi_polylist nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil integers nil )nil multi_polylist nil ))nil 3603099886 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3603108377"" (induct "n" )"1" (skeep) (("1" (grind) nil nil )) nil )"2" (skolem 1 "n" )"2" (flatten)"2" (assert )"2" (skeep)"2" (expand "mppow" +)"2" (lift-if)"2" (assert )"2" (ground)"1" (replaces -1)"1" (assert )"1" (expand "^" +)"1" (expand "expt" +)"1" (expand "expt" +)"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (typepred "mpprod(mpl, mppow(mpl, n))" )"2" (rewrite -1)"2" (hide -1)"2" (inst?)"2" (replaces -1)"2" expand "^" )"2" expand "expt" + 2)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{mpl | " nil )"odd_int" integers nil )"posint" nil )"real" reals nil )"real" reals nil )"RealOrder" util nil )"(total_order?[real])" nil )"real" exponentiation nil )"real" multi_polylist nil )"{r: real | LAMBDA (k: nat):IF k < length(ml) THEN xvar(k + i) ^ nth(ml, k)" multi_polylist nil) nil naturalnumbers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"MultiPolyList" multi_polylist nil )"real" multi_polylist nil )"[T, T -> boolean]" equalities nil )nil multi_polylist nil )nil multi_polylist nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3603108449"" (skeep)"" (expand "mpneg" )"" (rewrite "multipolylist_scal" ) (("" (assert ) nil nil )) nil ))nil ))nil )"MultiPolyList" multi_polylist nil )"real" reals nil )"real" reals nil )nil naturalnumbers nil )nil integers nil )nil multi_polylist nil )nil multi_polylist nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil list_adt nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil multi_polylist nil )"odd_int" integers nil ))nil 3604150775"" (skeep)"" (expand "mpminus" )"" (lemma "multipolylist_sum" )"" (inst?)"" (replaces -1)"" (lemma "multipolylist_neg" )"" (expand "mpneg" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"MultiPolyList" multi_polylist nil )"odd_int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil list_adt nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )nil multi_polylist nil )"MultiPolyList" multi_polylist nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil integers nil )nil naturalnumbers nil )nil multi_polylist nil )"real" reals nil )"real" reals nil )"real" reals nil )"MultiPolyList" multi_polylist nil )nil multi_polylist nil ))nil 3603108470"" (skeep)"" (expand "mpdiv" )"" (rewrite "multipolylist_scal" ) (("" (assert ) nil nil )) nil ))nil ))nil )"MultiPolyList" multi_polylist nil )"real" reals nil )"real" reals nil )nil naturalnumbers nil )nil integers nil )nil multi_polylist nil )nil multi_polylist nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil booleans nil )nil list_adt nil )nil reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil multi_polylist nil )"nzreal" nil ))nil 3603108525"" (skeep)"" (rewrite "multipolylist_prod" )"" (expand "sq" ) (("" (propax) nil nil )) nil )) nil ))nil )nil multi_polylist nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil list_adt nil )nil booleans nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil multi_polylist nil )nil multi_polylist nil )nil integers nil )nil naturalnumbers nil )"real" reals nil )"nonneg_real" sq "reals/" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.146Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
