SSL query_coeff.prf
Interaktion und
(query_coeffnil 3621165054 ("" (subtype-tcc) nil nil )"posint" nil ))nil ))nil 3621165054 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621165054"" (skeep)"" (typepred (f))"" (typepred (i))"" (skeep)"" (inst -2 "k" )"" (typepred (k)) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )nil integers nil )"bool" reals nil ) (> const-decl "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 )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil ))nil ))nil 3621165054 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3621165054"" (skeep)"" (typepred (i))"" (split-ineq -1)"" (typepred (f))"" (inst -1 "i" ) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"posint" nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posint" nil ))nil ))nil 3621165054"" (skeep)"" (skeep)"" (typepred " v(j, f, i + 1)" )"1" (typepred (k))"1" (inst -2 "k" ) (("1" (ground) nil nil )) nil )) nil )"2" (typepred (i))"2" (case "i<1+j" )"1" (ground) nil nil )"2" (case "i=1+j" )"1" (ground)"1" (typepred (f))"1" (inst -1 "i" ) (("1" (ground) nil nil )) nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )"posint" 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 number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil integers nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))nil ))nil 3621672198 ("" (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 ) (< const-decl "bool" reals nil )nil integers nil )nil naturalnumbers nil )nil naturalnumbers nil )"[list -> boolean]" list_adt nil )"nat" list_props nil )"boolean" notequal nil ))nil ))nil 3621672198"" (skeep)"" (split 1)"1" (ground) (("1" (grind) nil nil )) nil )"2" (skeep) (("2" (grind) nil nil )) nil ))nil ))nil )"posint" nil )"nat" list_props nil )"int" integers nil )"T" list_props nil ))nil ))nil 3621672198"" (skeep)"" (grind)"" (typepred (L))"" (grind) (("" (typepred (n)) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"nat" list_props 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 ) (< const-decl "bool" reals nil )nil integers nil )nil naturalnumbers nil )nil naturalnumbers nil )"[list -> boolean]" list_adt nil ))nil ))nil 3621672198"" (skeep) (("" (typepred (n)) (("" (grind) nil nil )) nil )) nil )"[list -> boolean]" list_adt nil )"nat" list_props nil )nil naturalnumbers 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 )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621672198"" (termination-tcc) nil nil ) nil nil ))nil 3621672198"" (skeep)"" (split 2)"1" (grind) nil nil )"2" (skeep)"2" (typepred "v(cdr[below(3)](L), n-1, new)" )"1" (inst -3 "i-1" )"1" (grind)"1" (expand "nth" 2 1)"1" (lift-if 2)"1" (split 2)"1" (flatten) (("1" (ground) nil nil )) nil )"2" (flatten) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (grind)"2" (typepred (L))"2" (typepred (i)) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (typepred (n)) (("2" (grind) nil nil )) nil )"3" (typepred (n)) (("3" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"int" integers nil )"posint" nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[(cons?) -> list]" list_adt nil )"T" list_props nil )nil nat_types nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[list -> boolean]" list_adt nil )nil naturalnumbers nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil ) (>= const-decl "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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"below(length(L))" query_coeff nil )"{ll: list[below(3)] | cons?[below(3)](ll)}" nil )"posint" nil ))nil ))nil 3621678714 ("" (existence-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 ) (< const-decl "bool" reals nil )nil integers nil )nil naturalnumbers nil )nil naturalnumbers nil )"[list -> boolean]" list_adt nil )"nat" list_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621678727"" case " FORALL (nn:posnat, L: list[below(3)], n: below(length(L)), new: below(3), ") "1" (skeep)"1" (inst?) (("1" (inst -1 "length(L)" ) nil nil )) nil )) nil )"2" (hide 2)"2" (induct "nn" )"1" (ground) nil nil ) ("2" (ground) nil nil )"3" (skeep)"3" (skeep)"3" (case-replace "j=0" )"1" (expand "switch_one_entry" )"1" (hide -2)"1" (typepred (n))"1" (ground)"1" (replace -4 :dir rl)"1" (case-replace "n=0" )"1" (grind)"1" (case "cdr(L) = null" )"1" (ground) nil nil )"2" "2" expand "length" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "n=0" )"1" (expand "switch_one_entry" 2)"1" (ground)"1" (expand "array2list" 2)"1" (expand "array2list_it" )"1" "cdr(L) = array2list_it(f WITH [n := new], length(L), 1)" )"1" (hide 3)"1" "list_extensionality[below(3)]" )"1" "cdr(L)" " array2list_it(f WITH [n := new], length(L), 1)" )"1" "1" "1" "1" (propax) nil nil )"2" "array2list_it(f WITH [n := new], length(L), 1)" )"2" replace -2)"2" "2" "cdr(L)" )"2" expand "length" 1 2)"2" "2" "2" "2" expand "length" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "array2list_it(f WITH [n := new], length(L), 1)" )"3" "3" "n_1+1" )"1" replace -6)"1" "1" replace "1" "1" "nth(cdr(L), n_1) = nth(L, n_1+1)" )"1" replace "1" "1" "array2list[below(3)](length(L))(f)" )"1" "n_1+1" )"1" nil nil )"2" "2" expand "length" "2" "2" "1" "1" expand "length" )"1" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nth" "2" nil nil ))nil )"3" expand "length" "3" "3" "1" "1" expand "length" )"1" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "length" 1)"2" "2" "1" "1" expand "length" )"1" 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 ))nil ))nil )"2" (expand "switch_one_entry" 3)"2" (ground)"2" (expand "array2list" 3)"2" (expand "array2list_it" )"2" (typepred (f))"2" (case-replace "f(0) = car(L)" )"1" "switch_one_entry(cdr(L), n - 1, new) = array2list_it(f WITH [n := new], length(L), 1)" )"1" "1" "list_extensionality[below(3)]" )"1" "1" "1" "1" "1" "1" (propax) nil nil )"2" "array2list_it(f WITH [n:=new], length(L), 1)" )"2" replace -2)"2" "2" expand "length" "2" "2" "1" "1" "1" expand "length" )"1" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "array2list_it(f WITH [n := new], length(L), 1)" )"3" "3" "n_1+1" )"1" replace "1" "switch_one_entry(cdr(L), n - 1, new)" )"1" "n_1" )"1" "1" case "n_1/=n-1" )"1" "1" replace "1" "1" "nth(cdr(L), n_1) = nth(L, n_1+1)" )"1" "1" "array2list[below(3)](length(L))(f)" )"1" "n_1+1" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" expand "nth" "2" nil nil ))nil )"3" expand "length" "3" "3" "1" "1" expand "length" )"1" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" case "FORALL (mm:posnat, ll:{lll:list[below(3)]|cons?(lll) AND length(lll) =mm}, m:below(mm)): ") "1" "length(cdr(L))" "cdr(L)" "n-1" )nil nil )"2" "2" "mm" )"1" nil nil )"2" nil nil )"3" "3" "3" case "j!1=0" )"1" "m=0" )"1" expand "switch_one_entry" )"1" expand "nth" )"1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" case "m=0" )"1" replace "1" expand "switch_one_entry" )"1" expand "nth" )"1" nil nil ))nil ))nil ))nil )"2" expand "switch_one_entry" "2" "2" expand "nth" "2" "cdr(ll)" "m-1" )"2" "2" expand "length" "2" "2" expand "length" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" "switch_one_entry(ll, m, new)" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "3" "mm" )"3" "3" "switch_one_entry(ll, m, new)" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "length" )"2" "2" "1" "1" nil nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 4)"2" "array2list[below(3)](length(L))(f)" )"2" "0" )"2" "2" replace -4)"2" expand "nth" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (skeep) (("4" (skeep) (("4" (grind) nil nil )) nil )) nil ))nil ))nil )"3" (skeep) (("3" (ground) (("3" (grind) nil nil )) nil )) nil ))nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"odd_int" integers nil )"[(cons?) -> list]" list_adt nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integers nil )"posint" nil )"int" integers nil )"{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" "structures/" )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"below(length(L))" query_coeff nil )"below(3)" query_coeff nil )"below(length(switch_one_entry(cdr(L), n - 1, new)))" query_coeffnil )"{lll: list[below(3)] | cons?(lll) AND length(lll) = 1 + j!1}" nil )"nat" query_coeff nil )"[(cons?) -> T]" list_adt nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil more_list_props"structures/" )"odd_int" integersnil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"list[below(3)]" query_coeff nil )"below(length(cdr(L)))" query_coeff nil )nil naturalnumbers nil )nil defined_types nil )"(strict_total_order?[real])" real_props 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 integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )"nat" list_props nil )"[T, T -> boolean]" equalities nil )nil listn "structures/" )nil nat_types nil )"T" list_props nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"boolean" notequal nil )"{ll: list[below(3)] | AND " query_coeff nil)) nil 3621672198 ("" (subtype-tcc) nil nil )"posint" nil ))nil ))nil 3621672198"" (skeep)"" (typepred (j))"" (lemma "expt_ge1" )"" (inst -1 "3" "j+1" )"" (ground)"" (skeep)"" (grind)"" (typepred (L)) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )nil integers 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 )"posint" nil )nil integers nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil listn "structures/" )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )"posrat" nil )"posnat" exponentiation nil )"real" exponentiation nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"posint" exponentiation nil )"(total_order?[real])" nil )nil exponentiation nil ))nil ))nil 3621672198"" (skeep)"" (skeep)"" (typepred (j))"" (typepred (L)) (("" (ground) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )nil listn "structures/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nat" list_props nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil naturalnumbers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil list_adt nil )nil defined_types nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"posint" 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 )"bool" reals nil )nil integers nil )nil integers nil ))nil ))nil 3621672198 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil listn "structures/" )"bool" reals nil )nil naturalnumbers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3621672198 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil listn "structures/" )"bool" reals nil )nil naturalnumbers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621672198 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil listn "structures/" )"bool" reals nil )nil naturalnumbers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3621672198 ("" (subtype-tcc) nil nil )"posint" nil ))nil ))nil 3621672198"" (skeep)"" (skeep)"" (typepred "v(j, L, i + 1)" )"1" (ground) (("1" (grind) nil nil )) nil )"2" (typepred (L)) (("2" (ground) nil nil )) nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )"posint" 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 ) (< const-decl "bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil listn "structures/" )"bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))nil ))nil 3621672198"" (skeep)"" (skeep)"" (typepred "v(j, L, i + 1)" )"1" (grind) nil nil )"2" (typepred (L)) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"posint" nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" 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 ) (< const-decl "bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil listn "structures/" )"bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))nil ))nil 3621672198 ("" (subtype-tcc) nil nil )"int" integers 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 )"bool" reals nil )nil integers nil )nil integers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil listn "structures/" )"bool" reals nil )nil naturalnumbers nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621672198 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil listn "structures/" )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621242035"" (skolem 1 ("j" "_" "_" "_" ))"" case "FORALL (n:nat, ") "1" (skeep)"1" (inst?)"1" (inst -1 "j+1-i" )"1" (split -1)"1" (propax) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skeep)"1" (typepred (f))"1" (inst -1 "i" )"1" (expand "bump_one_ind" )"1" (lift-if 1)"1" (split 1)"1" (flatten)"1" (split 1)"1" (flatten) (("1" (ground) nil nil )) nil )"2" (propax) nil nil ))nil ))nil )"2" (flatten) (("2" (ground) nil nil )) nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil )"2" (skeep)"2" (simplify)"2" (skeep)"2" (expand "bump_one_ind" 1)"2" (lift-if 1)"2" (split 1)"1" (flatten) (("1" (ground) nil nil )) nil )"2" (flatten)"2" (split 2)"1" (flatten) (("1" (ground) nil nil )) nil )"2" (flatten)"2" (inst -1 "f" "i+1" "k" )"1" "1" (ground) nil nil )"2" (ground) nil nil )"3" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{ff: [nat -> below(3)] | FORALL (k: above(j + 1)): ff(k) = 0}" nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" 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 )"int" integers nil )"(total_order?[real])" nil )"posint" nil )nil defined_types nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"upto(1 + j)" query_coeff nil )"posnat" query_coeff nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"upto(1 + j)" query_coeff nil )"int" integers nil ))nil 3621174807"" (skeep)"" (lift-if 1)"" (split 1)"1" (expand "base_n_to_nat" )"1" (lemma "sigma_with" )"1" (expand "bump_one_ind" )"1" (flatten)"1" "(LAMBDA (s: nat): IF f(i) < 2 THEN f WITH [i := 1 + f(i)](s)LAMBDA (s: nat): 3 ^ s * f(s)) WITH [i:= 3^i*(1+f(i))]") "1" "(LAMBDA (s: nat): 3 ^ s * f(s)) WITH [i := 3 ^ i * (1 + f(i))]" "LAMBDA (s: nat): 3 ^ s * f(s)" "3 ^ i * (1 + f(i))" "1+j" "i" "0" )"1" (split -2)"1" (ground) nil nil ) ("2" (ground) nil nil )"3" (ground) nil nil ))nil ))nil )"2" (hide 2)"2" (decompose-equality 1)"2" (ground)"2" (case "i=x!1" )"1" (ground) nil nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "base_n_to_nat" )"2" (expand "bump_one_ind" 2 1)"2" (lemma "sigma_with" )"2" "LAMBDA (s: nat): IF f(i) < 2 THEN f WITH [i := 1 + f(i)](s)" " LAMBDA (s: nat): 3 ^ s * bump_one_ind(j, f, 1 + i)(s)" "0" "j+1" "i" "0" )"1" (split -1)"1" (ground)"1" (case "i+1<=j+1" )"1" (ground)"1" (replace -2)"1" "bump_one_ind(j, f, 1 + i)(i) = f(i)" )"1" (ground) nil nil )"2" "bump_one_below" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 3))"2" (typepred (f))"2" (typepred (i))"2" case "i<1+j" )"1" (ground) nil nil )"2" case "i=1+j" )"1" "i" )"1" (ground) nil nil )"2" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ) ("3" (ground) nil nil )"4" (hide 3)"4" (decompose-equality 1)"1" (case "x!1 = i" )"1" (ground) nil nil )"2" (ground) nil nil ))nil )"2" (typepred (f))"2" (typepred (i))"2" (case "i<1+j" )"1" (ground) nil nil )"2" case "i=1+j" )"1" "i" )"1" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil )"3" (typepred (f))"3" (typepred (i))"3" (case "i<1+j" )"1" (ground) nil nil )"2" case "i=1+j" )"1" "i" )"1" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred (f))"2" (typepred (i))"2" (case "i<1+j" )"1" (ground) nil nil )"2" (case "i=1+j" )"1" (inst -3 "i" )"1" (ground) nil nil )"2" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil )"3" (flatten)"3" (typepred (f))"3" (typepred (i))"3" (case "i<1+j" )"1" (ground) nil nil )"2" (case "i=1+j" )"1" (inst -3 "i" )"1" (ground) nil nil )"2" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil query_coeff nil )"posint" nil )"posint" exponentiation nil )"nnreal" sigma_nat "reals/" )"nat" sigma_nat "reals/" )"nat" base_repr "reals/" )"{ff: [nat -> below(3)] | FORALL (k: above(j + 1)): ff(k) = 0}" nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )nil integers nil )nil integers nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"int" integers nil )"int" integers nil )nil sigma "reals/" )nil sigma "reals/" )"nonneg_int" nil )"real" reals nil )"posnat" query_coeff nil )"{f | FORALL (k: above(j)): f(k) = 0}" nil )"upto(1 + j)" query_coeff nil )nil sigma "reals/" )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 ))nil 3621258320 ("" (subtype-tcc) nil nil )nil nil ))nil 3621258320"" (skeep)"" (typepred (i))"" (case "i=j+1" )"1" (typepred (f))"1" (inst -1 "i" )"1" (inst -4 "i" ) (("1" (ground) nil nil )) nil )"2" (ground) nil nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields 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 )"posint" nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"(total_order?[real])" nil )"upto(1 + j)" query_coeff nil )"posnat" query_coeff nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"posint" nil ))nil ))nil 3621258320 ("" (subtype-tcc) nil nil )nil nil ))nil 3621258372"" (skolem 1 ("j" "_" "_" ))"" case "FORALL (n:nat, (f: [nat -> below(3)] | FORALL (k: above(j)): f(k) = 0), LAMBDA (s: nat): 2 * 3 ^ s)") "1" (skeep)"1" (inst?)"1" (inst -1 "i" )"1" (split -1)"1" (propax) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skeep)"1" (replace -1 :dir rl)"1" (simplify)"1" (rewrite "sigma_eq_arg" )"1" (expand "bump_one_ind" 1 1)"1" (inst -2 "0" )"1" (split -2)"1" (ground)"1" (expand "base_n_to_nat" )"1" (lemma "sigma_with" )"1" "LAMBDA (s: nat): " "LAMBDA (s: nat): 3 ^ s * bump_one_ind(j, f, 1)(s)" "0" "j+1" "0" "0" )"1" "1" rewrite "bump_one_below" )"1" "1" replace -2)"1" "1" expand "*" )"1" "1" "(LAMBDA (s: nat): LAMBDA (x: nat): 3 ^ s * bump_one_ind(j, f, 1)(x))LAMBDA (s: nat):") "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil )"3" (ground) nil nil )"4" "4" "4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (inst -1 "f" "i-1" )"1" (split -1)"1" (simplify -1)"1" (lemma "bump_one_ind_lem" )"1" (inst -1 "j" "f" "i" )"1" (lift-if -1)"1" (inst-cp -4 "i" )"1" (split -5)"1" "1" replace -3)"1" replace -1)"1" "1" "*" "-1" 2)"1" "1" replace -2)"1" expand "sigma" 2 2)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (inst -3 "m" ) (("2" (ground) nil nil )) nil ))nil )"3" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil )"3" (skeep)"3" (hide 2)"3" (typepred (f))"3" (typepred (i))"3" (inst -3 "i" )"3" (inst -2 "i" )"1" (ground) nil nil ) ("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep)"3" (typepred (f))"3" (typepred (j))"3" (typepred (i))"3" (inst -4 "i" )"3" (inst -3 "i" )"1" (ground) nil nil ) ("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" exponentiation nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"{ff: [nat -> below(3)] | FORALL (k: above(j + 1)): ff(k) = 0}" nil )"nat" base_repr "reals/" )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" 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 )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"posint" nil )"posint" nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posnat" query_coeff nil )nil defined_types nil )nil naturalnumbers nil )"posint" exponentiation nil )"nnreal" sigma_nat "reals/" )"nat" sigma_nat "reals/" )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )"int" integers nil )"even_int" integersnil )"posnat" exponentiation nil )"real" exponentiation nil )nil query_coeff nil )"posrat" nil )"[T -> real]" real_fun_ops "reals/" )"nonneg_int" nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"odd_int" integers nil )nil query_coeff nil )nil real_props nil )"bool" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"upto(1 + j)" query_coeff nil )"(strict_total_order?[real])" real_props nil )"upto(1 + j)" query_coeff nil )"upto(1 + j)" query_coeff nil ))nil 3621333123 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"posnat" query_coeff nil )"{f | FORALL (k: above(j!1)): f(k) = 0}" nil )"{ii: upto(1 + j!1) | f!1(ii) < 2}" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"bool" sets nil )"bool" sets nil ))nil ))nil 3621333123 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"{ii: upto(1 + j!1) | f!1(ii) < 2}" nil )"{f | FORALL (k: above(j!1)): f(k) = 0}" nil )"posnat" query_coeff nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621333584"" (skolem 1 ("j" "f" "_" ))"" case "FORALL (n:nat, i: {ii: upto(1 + j) | f(ii) < 2}): LET M = low2(j, f, i) INAND (FORALL (m: nat): m < M IMPLIES f(m) = 2))") "1" (skeep) (("1" (inst -1 "i" "i" ) nil nil )) nil )"2" (hide 2)"2" (induct "n" 1 "NAT_induction" )"1" (ground) nil nil )"2" (skeep)"2" (ground)"2" (skeep)"2" (expand "low2" 1)"2" (lift-if 1)"2" (split 1)"1" (flatten)"1" "choose({m: nat | m < i AND f(m) < 2}) " )"1" (split -2)"1" "choose({m: nat | m < i AND f(m) < 2}) " )"1" (ground) nil nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "2" "m" )"2" "2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" "2" "m" )"2" "2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (typepred (i))"2" (ground)"2" case "nonempty?({m:nat| m<i AND f(m)<2})" )"1" expand "nonempty?" )"1" expand "empty?" )"1" "1" expand "member" )"1" (inst 2 "x" ) nil nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" "2" expand "empty?" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{ii: upto(j + 1) | f(ii) < 2}" query_coeff nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" 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 )"posint" nil )nil defined_types nil )nil naturalnumbers nil )"{ii: upto(1 + j) | f(ii) < 2}" query_coeffnil )"{f | FORALL (k: above(j)): f(k) = 0}" nil )"posnat" query_coeff nil )"bool" sets nil )set type-eq-decl nil sets nil ) (choose const-decl "(p)" sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3621256133 ("" (subtype-tcc) nil nil ) nil nil ))nil 3621256149"" case "FORALL (j: posnat, AND (FORALL (m:nat):m<nn IMPLIES f(m) = 2 )}):") "1" (skeep)"1" case "EXISTS (nn:upto(j+1)): f(nn) < 2 AND ") "1" (skeep)"1" (inst? -3)"1" (inst -3 "nn" ) (("1" (ground) nil nil )) nil )) nil ))nil )"2" (hide (-1 2))"2" (typepred (f))"2" (ground)"2" (inst 1 " low2(j, f, j+1)" )"1" (lemma "low2_lem" )"1" (inst -1 "j" "f" "j+1" )"1" (ground) nil nil )"2" (inst -1 "j+1" ) (("2" (ground) nil nil ))nil ))nil ))nil )"2" (inst -1 "j+1" ) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (typepred (n))"2" (lemma "bump_one_ind_lem2" )"2" (inst?)"2" (case-replace "n=0" )"1" (typepred (j))"1" (lemma "bump_one_ind_lem" )"1" (inst -1 "j" "f" "0" )"1" (ground)"1" (expand "^" )"1" (expand "expt" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (inst -1 "n-1" )"1" (split -1)"1" (simplify -1)"1" (lemma "bump_one_ind_lem" )"1" (inst -1 "j" "f" "n" )"1" (ground)"1" (replace -1)"1" replace -2)"1" "1" rewrite "sigma_scal" )"1" "sigma_geometric" )"1" "n-1" "0" "3" )"1" "1" replace -1)"1" "1" "1" "2 * ((3 ^ 0 - 3 ^ n) / (-2)) = - (3^0-3^n)" )"1" "1" case "forall(a,b:real): a - (-b) = a+b" )"1" "3^n" "(3 ^ 0 - 3 ^ n)" )"1" "1" replace "1" expand "^" )"1" expand "expt" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil )"3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground)"2" (skeep)"2" (inst?) (("2" (ground) nil nil )) nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"odd_int" integersnil )"nat" sigma_nat "reals/" )"nnreal" sigma_nat "reals/" )"posint" exponentiation nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"posnat" query_coeff nil )"{f: [nat -> below(3)] | FORALL (k: above(j)): f(k) = 0}" nil )"{nn: upto(1 + j) | f(nn) < 2 AND (FORALL (m: nat): m < nn IMPLIES f(m) = 2)}" nil )"int" integers nil )"odd_int" integers nil )nil sigma_nat "reals/" )"rat" rationals nil )"rat" rationals nil )"rat" rationals nil )"nnrat" exponentiation nil )"even_int" integersnil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"even_int" integers nil )"nzint" integers nil )"int" integers nil )"real" reals nil )"real" reals nil )"real" reals nil )nil reals nil )nil real_props nil )"nonneg_int" nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil sigma "reals/" )nil sigma "reals/" )"posnat" exponentiation nil )"real" exponentiation nil )"real" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )nil query_coeff nil )nil query_coeff nil )nil query_coeff nil )"(strict_total_order?[real])" real_props nil )"{ii: upto(j + 1) | f(ii) < 2}" query_coeff nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"posnat" query_coeff nil )"{f | FORALL (k: above(j)): f(k) = 0}" nil )"upto(1 + j)" query_coeff nil )"posint" nil )"posint" 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 integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"nat" base_repr "reals/" )"{ff: [nat -> below(3)] | FORALL (k: above(j + 1)): ff(k) = 0}" nil ))nil 3621264743"" (skeep)"" (skeep)"" (typepred (f))"" (typepred (k_1))"" (lemma "upper_is_bound" )"" (inst?)"" (inst -1 "k_1" ) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )"nat" base_repr "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(strict_total_order?[real])" real_props nil )"posint" nil )nil base_repr "reals/" )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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" base_repr "reals/" ))nil ))nil 3621264743 ("" (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 )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" base_repr "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"posint" nil ))nil ))nil 3621264745"" (skeep)"" (lemma "bump_one_prep" )"" (inst?)"" (lemma "base_n_unique" )"" (typepred (f))"" (replace -1)"" (lemma "base_n_is_n_alt" )"" (inst -1 "3" "k" "upper_index(3, k) +2" )"" (split -1)"1" (replace -1 :dir rl)"1" "upper_index(3,k)+2 " "3" "bump_one_ind(upper_index(3, k) + 1, base_n(3, k), 0)" )"1" (expand "base_n_to_nat" -4)"1" (ground)"1" (decompose-equality 1)"1" "bump_one_ind(1 + upper_index(3, k), base_n(3, k), 0)" )"1" case "x!1>2+upper_index(3,k)" )"1" "x!1" )"1" "upper_is_bound" )"1" "3" "k+1" "x!1" )"1" "1" (ground) nil nil )"2" "2" "2" expand "upper_index" )"2" "2" "1" "1" "log_nat_incr" )"1" replace -2)"1" expand "log_nat" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "log_nat_incr" )"2" expand "log_nat" "2" "2" "1" "1" nil nil ))nil )"2" "2" "2" expand "log_nat" "2" "2" "1" "1" nil nil ))nil )"2" "2" "2" "3" "(1 + k) / 3 / 3" "k" )"2" "1" nil nil )"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 )"2" "x!1" )"2" "1" (ground) nil nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil )"2" "2" (rewrite "base_n_lt_n" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "upper_index" )"2" (lift-if 1)"2" (split 1)"1" (grind) nil nil )"2" (flatten)"2" "log_nat_bounds" )"2" "3" "k" )"2" "2" "2" expand "^" )"2" expand "expt" 2)"2" expand "expt" 2)"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil query_coeff nil )nil base_repr "reals/" )nil log_nat "reals/" )"odd_int" integers nil )"posnat" exponentiation nil )"posint" nil )"real" exponentiation nil )"real" exponentiation nil )"nat" exponentiation nil )"int" integers nil )"posint" nil )"nat" base_repr "reals/" )"nat" query_coeff nil )nil base_repr "reals/" )"(total_order?[real])" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"posrat" nil )"odd_int" integers nil )"posrat" nil )"even_int" integersnil )"[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat"reals/" )nil log_nat "reals/" )"nat" query_coeff nil )"(strict_total_order?[real])" real_props nil )nil base_repr "reals/" )"posint" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"nat" sigma_nat "reals/" )"nnreal" sigma_nat "reals/" )"bool" reals nil )nil naturalnumbers nil )"{ff: [nat -> below(3)] | FORALL (k: above(j + 1)): ff(k) = 0}" nil )nil base_repr "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"nat" base_repr "reals/" )"[T, T -> boolean]" equalities nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )"nat" base_repr "reals/" )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil integers nil )"bool" reals nil )nil integers 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 )"posint" nil ))nil 3621165054"" (lemma "bump_one_prep2" ) (("" (ground) nil nil )) nil )nil query_coeff nil )) nil ))nil 3621677401"" case "FORALL (nn:nat, j: posnat, L: listn[below(3)](j + 1), ") "1" (skeep)"1" (inst?)"1" (inst -1 "j+1-i" ) (("1" (ground) nil nil )) nil )) nil ))nil )"2" (hide 2)"2" (induct "nn" )"1" (skeep)"1" (both-sides "+" "i" -1)"1" (simplify)"1" (expand "bump_one_ind_list" )"1" (lift-if 1)"1" (ground)"1" (lemma "bump_one_below" )"1" (lemma "list_extensionality[below(3)]" )"1" (inst?)"1" (flatten)"1" (hide -1)"1" "array2list[below(3)](1 + j)(bump_one_ind(j, f, i))" )"1" replace -2)"1" "1" (propax) nil nil )"2" "2" (propax) nil nil ))nil )"3" "3" "n" )"3" replace -3 :dir rl)"3" "j" "f" "i" "n" )"3" "3" "3" replace -1)"3" "3" "3" replace "3" "3" "array2list[below(3)](1 + j)(f)" )"3" "n" )"3" 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 )"2" (ground) nil nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (case "nth(L,i) = f(i)" )"1" (case "f(i)<2" )"1" (expand "bump_one_ind_list" )"1" (expand "bump_one_ind" )"1" (hide -3)"1" (ground)"1" (lemma "switch_is_with" )"1" (inst -1 "L" "i" "1+f(i)" "f" )"1" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bump_one_ind" 2)"2" (expand "bump_one_ind_list" 2)"2" (ground)"2" (lemma "switch_is_with" )"2" "bump_one_ind_list(j, L, 1 + i)" "i" "0" "bump_one_ind(j, f, 1 + i)" )"1" (ground) nil nil )"2" (hide 3)"2" (inst -2 "j" "L" "f" "i+1" )"2" "1" (ground) nil nil )"2" (propax) nil nil )"3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -3 :dir rl)"2" (typepred "array2list[below(3)](j + 1)(f)" )"2" (inst -3 "i" )"1" (ground) nil nil ) ("2" (ground) nil nil ))nil ))nil ))nil )"3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"posnat" query_coeff nil )"listn[below(3)](1 + j)" query_coeff nil )"upto(1 + j)" query_coeff nil )"{f: [nat -> below(3)] | FORALL (k: above(j)): f(k) = 0}" nil )nil query_coeff nil )"[list -> boolean]" list_adt nil )"posint" nil )nil query_coeff nil )"(strict_total_order?[real])" real_props nil )nil more_list_props"structures/" )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"nonneg_int" nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"int" integers nil )"posint" 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 )nil integers nil )"bool" reals nil )nil integers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil listn "structures/" )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )"T" list_props nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"listn[below(3)](j + 1)" query_coeffnil )"{ff: [nat -> below(3)] | FORALL (k: above(j + 1)): ff(k) = 0}" nil ))nil 3621696480 ("" (subtype-tcc) nil nil ) nil nil ))nil 3621696480"" (skeep)"" (lemma "switch_to_array" )"" (inst -1 "j" "L" "base_n(3,k)" "0" )"1" (typepred (L))"1" (split -4)"1" (replace -1)"1" (expand "base_list" )"1" "bump_one_ind(j, base_n(3, k), 0) = base_n(3, 1 + k)" )"1" (hide -)"1" (hide 2)"1" (lemma "bump_one_prep" )"1" (inst -1 "j" " base_n(3, k)" )"1" (lemma "base_n_is_n_alt" )"1" (inst -1 "3" "k" "j+1" )"1" "1" "1" replace -1 :dir rl)"1" "base_n_to_nat_unique" )"1" "3" "k" "j+1" "bump_one_ind(j, base_n(3, k), 0)" " base_n(3, k+1)" )"1" "1" "1" "bump_one_ind(j, base_n(3, k), 0)" )"1" case "x!1 >1+j" )"1" "x!1" )"1" "base_n_0" )"1" "3 " "1+k" "x!1" )"1" "1" nil nil )"2" "2" case "k=0" )"1" replace "1" "both_sides_expt_gt1_gt" )"1" "3" "x!1" "1+j" )"1" "1" case "forall (a,b:nat): a<b IMPLIES a+1<=b" )"1" "0" "3^(1+j)" )"1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "k+1<=3^(1+j)" )"1" "both_sides_expt_gt1_gt" )"1" "3" "x!1" "1+j" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" case "forall (a,b:nat): a<b IMPLIES a+1<=b" )"1" "k" "3^(1+j)" )"1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" nil nil ))nil ))nil ))nil )"2" "2" rewrite "base_n_lt_n" )nil nil ))nil ))nil )"2" "2" rewrite "base_n_lt_n" )"2" "bump_one_ind(j, base_n(3, k), 0)" )"2" nil nil ))nil ))nil ))nil )"3" replace -3)"3" "base_n_is_n_alt" )"3" "3" "k+1" "j+1" )"3" "1" nil nil )"2" case "forall (a,b:nat): a<b IMPLIES a+1<=b" )"1" "k" "3^(1+j)" )"1" "1" "both_sides_expt_gt1_gt" )"1" "3" "j+2" "j+1" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" )"2" expand "expt" 1)"2" case "1<3" )"1" "1" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "base_list" ) (("2" (ground) nil nil )) nil ))nil ))nil )"2" (split 1)"1" (skeep) (("1" (rewrite "base_n_lt_n" ) nil nil )) nil )"2" (skeep)"2" (typepred (k_1))"2" (typepred (k))"2" (lemma "base_n_0" )"2" (inst -1 "3" "k" "k_1" )"2" (case "k_1>=j+1" )"1" (lemma "both_sides_expt_gt1_ge" )"1" (inst -1 "3" "k_1" "j+1" )"1" (flatten)"1" (hide -1) (("1" (ground) nil nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil query_coeff nil )"(total_order?[real])" nil )nil exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"{ff: [nat -> below(3)] | FORALL (k: above(j + 1)): ff(k) = 0}" nil )"posint" nil )nil base_repr "reals/" )nil base_repr "reals/" )"(strict_total_order?[real])" real_props nil )"nat" query_coeff nil )nil real_types nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"odd_int" integers nil )"(total_order?[real])" nil )"odd_int" integers nil )nil exponentiation nil )nil base_repr "reals/" )"(strict_total_order?[real])" real_props nil )"posint" exponentiation nil )"posint" nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"posnat" exponentiation nil )nil extra_real_props nil )nil base_repr "reals/" )nil query_coeff nil )nil naturalnumbers nil )"bool" reals nil )"listn[below(n)](digits)" base_repr "reals/" )nil listn "structures/" )"nat" list_props nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, 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 )"bool" reals nil ) (> const-decl "bool" reals nil )"nat" base_repr "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil integers nil )"posnat" query_coeff nil )nil naturalnumbers nil )"below(3 ^ (1 + j))" query_coeff nil )nil integers nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3621592121 ("" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil ))nil 3621758096 ("" (subtype-tcc) nil nil )nil nil ))nil 3621758096 ("" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )"nat" list_props nil )nil listn "structures/" )"listn[below(n)](digits)" base_repr "reals/" )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"int" integers nil )"(total_order?[real])" nil )"posint" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" exponentiation nil )"posnat" exponentiation nil ))nil ))nil 3621758096"" (skeep)"" (skeep)"" (ground)"" (typepred (i))"" (ground)"" (case "forall (a, b:nat): a<b IMPLIES a+1<=b" )"1" (inst -1 "i" "3^n" ) (("1" (ground) nil nil )) nil )"2" (skeep) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans 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 )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"posint" nil )"(total_order?[real])" nil )"real" reals nil )"posint" exponentiation nil ))nil ))nil 3621758096 ("" (subtype-tcc) nil nil )"real" exponentiation nil )) nil ))nil 3621758096 ("" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )"nat" list_props nil )nil listn "structures/" )"listn[below(n)](digits)" base_repr "reals/" )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"(strict_total_order?[real])" real_props nil )"posnat" exponentiation nil )"(total_order?[real])" nil )"posint" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" exponentiation nil ))nil ))nil 3621758096 ("" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )"nat" list_props nil )nil listn "structures/" )"posnat" exponentiation nil )"(total_order?[real])" nil )"posint" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" exponentiation nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"listn[below(n)](digits)" base_repr"reals/" ))nil ))nil 3621758096"" (termination-tcc) nil nil )"posnat" exponentiation nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )"{x: real | x = F(l) * G(l)}" query_coeffnil )"real" exponentiation nil )"real" exponentiation nil ))nil ))nil 3621758096 ("" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )"nat" list_props nil )nil listn "structures/" )"listn[below(n)](digits)" base_repr "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" exponentiation nil )"(total_order?[real])" nil )"posnat" exponentiation nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"real" exponentiation nil ))nil ))nil 3621592759 ("" (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 )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil naturalnumbers nil )nil defined_types nil )nil list_adt nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil integers nil )nil integers nil )"nat" list_props nil )nil listn "structures/" )"listn[below(n)](digits)" base_repr "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posint" exponentiation nil )"(total_order?[real])" nil )"int" integers nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"real" exponentiation nil )"posnat" exponentiation nil ))nil ))nil 3621592773"" case "FORALL (nn:nat, n: {x:nat|x>1}, LAMBDA (j: nat):") "1" (skeep) (("1" (inst?) (("1" (inst -1 "3^n-i" ) nil nil )) nil ))nil )"2" (hide 2)"2" (skolem 1 ("_" "n" "F" "G" "_" "_" "_" ))"2" (induct "nn" )"1" (skeep)"1" (both-sides "+" "i" -1)"1" (simplify -1)"1" (replace -1)"1" (expand "dot_tail_sum2plus" )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (expand "dot_tail_sum2plus" 1)"2" (lift-if 1)"2" (split 1)"1" (flatten) (("1" (ground) nil nil )) nil )"2" (flatten)"2" "is_nonzero(n, L, F, G) + a" "i+1" "bump_one_list(n - 1, i, L)" )"1" (split -1)"1" (replace -1)"1" (swap-rel 2)"1" rewrite "sigma_first" (2 2))"1" "1" "is_nonzero(n, L, F, G)" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep) (("3" (ground) nil nil )) nil ))nil ))nil ))nil )"3" (skeep) (("3" (ground) nil nil )) nil ))nil )"(strict_total_order?[real])" real_props nil )"{x: nat | x > 1}" query_coeff nil )nil defined_types nil )nil naturalnumbers nil )"nonneg_int" nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"posint" nil )"{x: real | x = F(l) * G(l)}" query_coeffnil )"{ll: listn[below(3)](j + 1) | ll = base_list(3, k + 1, j + 1)}" nil )"upto(3 ^ n)" query_coeff nil )"posint" nil )"(total_order?[real])" nil )"posint" exponentiation nil )"int" integers nil )"real" reals nil )"real" reals 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 )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil naturalnumbers nil )nil integers nil )nil integers nil )nil listn "structures/" )"listn[below(n)](digits)" base_repr "reals/" )"[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" query_coeff nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3621595927 ("" (subtype-tcc) nil nil )"real" reals nil ))nil ))nil 3621595927"" (skeep)"" (skeep)"" (typepred (i))"" (ground)"" (case "forall (k, l:nat): k<l IMPLIES k+1<=l" )"1" (inst -1 "i" "3^n" ) (("1" (ground) nil nil )) nil )"2" (hide-all-but 1)"2" (skeep) (("2" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans 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 )"int" integers nil )"(total_order?[real])" nil )"posint" exponentiation nil )"(total_order?[real])" nil ))nil ))nil 3621595927"" (skeep)"" (skeep)"" (typepred (i))"" (case "forall (a, b:nat): a<b IMPLIES a+1<=b" )"1" (inst -1 "i" "3^n" ) (("1" (ground) nil nil )) nil )"2" (skeep) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"posint" nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" exponentiation 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 )"bool" reals nil )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil ))nil ))nil 3621758128 ("" (termination-tcc) nil nil )"posnat" exponentiation nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )"{x: real | x = F(f) * G(f)}" query_coeff nil )"real" exponentiation nil )"real" exponentiation nil ))nil ))nil 3621595927"" (skeep)"" (skeep) (("" (rewrite "base_n_lt_n" ) nil nil )) nil )) nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (> const-decl "bool" 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 base_repr "reals/" ))nil ))nil 3621595927"" (skeep) (("" (inst 2 "3^n" ) (("" (ground) nil nil )) nil )) nil )"posint" exponentiation 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 )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil integers nil )"bool" reals nil )nil integers nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3621758128"" (skeep)"" (skeep) (("" (rewrite "base_n_lt_n" ) nil nil )) nil )) nil )"bool" 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 base_repr "reals/" ))nil ))nil 3621596460"" (skolem 1 ("n" "F" "G" "_" "_" ))"" case "FORALL (nn:nat, a: real, i: upto(3 ^ n)): nn=3^n-i IMPLIES LAMBDA (j: nat): F(base_n(3, j)) * G(base_n(3, j))) ") "1" (skeep)"1" (inst?) (("1" (inst -1 "3^n-i" ) nil nil )) nil )) nil )"2" (hide 2)"2" (induct "nn" )"1" (skeep)"1" (both-sides "+" "i" -1)"1" (simplify -1)"1" (replace -1)"1" (expand "dot_tail_sum2" )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (expand "dot_tail_sum2" 1)"2" (lift-if 1)"2" (split 1)"1" (flatten) (("1" (ground) nil nil )) nil )"2" (flatten)"2" "is_nz(n, base_n(3, i), F, G) + a " "1 + i" )"2" (split -1)"1" (typepred "bump_one(i, base_n(3, i))" )"1" (replace -1)"1" replace -2)"1" "1" rewrite "sigma_first" 2)"1" "is_nz(n, base_n(3, i), F, G)" )"1" (ground) nil nil ))nil )"2" "2" "2" rewrite "base_n_lt_n" )nil nil ))nil ))nil ))nil )"2" "2" "2" rewrite "base_n_lt_n" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (skeep)"3" (skeep)"3" (skeep) (("3" (rewrite "base_n_lt_n" ) nil nil ))nil ))nil ))nil ))nil )"4" (skeep) (("4" (ground) nil nil )) nil )"5" (skeep)"5" (skeep)"5" (skeep) (("5" (rewrite "base_n_lt_n" ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skeep)"3" (skeep)"3" (skeep)"3" (skeep) (("3" (rewrite "base_n_lt_n" ) nil nil )) nil ))nil ))nil ))nil )"4" (skeep) (("4" (ground) nil nil )) nil )"5" (skeep)"5" (skeep)"5" (skeep) (("5" (rewrite "base_n_lt_n" ) nil nil )) nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" query_coeff nil )"nat" base_repr "reals/" )nil naturalnumbers nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" 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 )"real" reals nil )"real" reals nil )"int" integers nil )"posint" exponentiation nil )"(total_order?[real])" nil )"posnat" query_coeff nil )nil defined_types nil )nil naturalnumbers nil )"nonneg_int" nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )nil base_repr "reals/" )nil sigma "reals/" )"{ff: [nat -> below(3)] | ff = base_n(3, k + 1)}" query_coeff nil )"{x: real | x = F(f) * G(f)}" query_coeff nil )"posint" nil )"posint" nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.205 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
