Quelle poly_systems.prf
Sprache: Lisp
(poly_systemsnil 3618845198"" (skeep)"" (case "FORALL (i): i<=k IMPLIES n(i)=0" )"1" case "FORALL (i,x): i<=k IMPLIES polynomial(p(i),n(i))(x)/=0" )"1" (inst + "0" "LAMBDA (j:below(0)): 0" )"1" (split)"1" (skosimp*) nil nil ) ("2" (skosimp*) nil nil )"3" (skosimp*)"3" (inst - "j!1" "b!1" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (inst - "i" )"2" (inst - "i" )"2" (assert )"2" (replace -3)"2" (expand "polynomial" )"2" (expand "sigma" )"2" (expand "sigma" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "IGGY" "LAMBDA (b:real): ((EXISTS (j:nat): j<=k AND polynomial(p(j), n(j))(b) = 0))" )"2" (case "is_finite[real](IGGY)" )"1" (copy -1)"1" (lemma "card_bij_inv[real]" )"1" (name "K" "card(IGGY)" )"1" (inst - "K" "IGGY" )"1" (assert )"1" (label "fbij" -2)"1" (skeep)"1" (skeep -2)"1" "newenum" "sort_array[K,real,<=].sort(f)" )"1" (inst + "K" "newenum" )"1" case "NOT (FORALL (i, j: below(K)): i < j IMPLIES newenum(i) < newenum(j))" )"1" "1" "1" case "NOT newenum(i!1) = newenum(j)" )"1" assert )"1" "newenum" )"1" expand "sorted?" )"1" "i!1" "j" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "newenum" )"2" expand "permutation_of?" )"2" "2" expand "bijective?" -1)"2" "2" expand "surjective?" )"2" "j" )"2" "i!1" )"2" "2" "x!1" )"2" "x!2" )"2" replace "2" replace "2" "fbij" )"2" expand "bijective?" "2" "2" expand "injective?" "2" "x!1" "x!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 )"2" replace -1)"2" assert )"2" "1" "1" "newenum" )"1" expand "permutation_of?" )"1" "1" expand "bijective?" )"1" "1" expand "surjective?" "1" "i!1" )"1" "j!1" )"1" "j!1" )"1" assert )"1" "f(j!1)" )"1" replace "1" replace "1" expand "IGGY" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "newenum" )"2" expand "permutation_of?" )"2" "2" expand "bijective?" )"2" "2" expand "surjective?" "2" "b" )"1" "ii" )"1" "ii" )"1" "f!1(ii)" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "IGGY" "2" assert )"2" "j" )"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 )"2" (propax) nil nil ))nil ))nil ))nil )"2" (hide 3)"2" "IGGYk" "LAMBDA (kp:nat): (LAMBDA (b: real):(EXISTS (j: nat): AND polynomial(p(j), n(j))(b) = 0))") "2" case "FORALL (kp:nat): kp<=k IMPLIES is_finite[real](IGGYk(kp))" )"1" (inst - "k" )"1" (assert )"1" (case "IGGYk(k) = IGGY" )"1" (assert ) nil nil )"2" (decompose-equality 1)"2" (expand "IGGYk" 1)"2" (expand "IGGY" 1)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" "IGGYthis" "LAMBDA (kp:nat): LAMBDA (b:real): polynomial(p(kp),n(kp))(b)=0" )"2" case "FORALL (kp:nat): kp<=k IMPLIES is_finite[real](IGGYthis(kp))" )"1" (induct "kp" )"1" (assert )"1" (inst - "0" )"1" (assert )"1" (case "IGGYthis(0)=IGGYk(0)" )"1" (assert ) nil nil )"2" "2" expand "IGGYthis" 1)"2" expand "IGGYk" 1)"2" "2" "1" "0" )"1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (assert )"2" case "IGGYk(1+j) = union(IGGYk(j),IGGYthis(1+j))" )"1" (lemma "finite_union[real]" )"1" "IGGYk(j)" "IGGYthis(1+j)" )"1" (assert ) nil nil )"2" "1+j" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (decompose-equality 1)"2" expand "union" 1)"2" expand "member" )"2" expand "IGGYk" 1)"2" expand "IGGYthis" 1)"2" "2" "1" "1" case "j!1 = 1+j" )"1" (assert ) nil nil )"2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" (assert ) nil nil ))nil ))nil )"3" "1+j" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (kk:nat,a:[nat->real]): (EXISTS (i:nat):i<=kk AND a(i)/=0) IMPLIES is_finite[real](LAMBDA (b:real): polynomial(a,kk)(b)=0)" )"1" (skeep)"1" (inst - "n(kp)" "p(kp)" )"1" (split -)"1" (assert )"1" expand "IGGYthis" 1)"1" (propax) nil nil ))nil ))nil )"2" (inst + "n(kp)" )"2" assert )"2" "kp" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (induct "kk" )"1" (skeep)"1" (skeep -1)"1" case "i = 0" )"1" "1" "1" assert )"1" "finite_emptyset[real]" )"1" case "%1 = %2" )"1" (assert ) nil nil )"2" "2" "2" expand "polynomial" )"2" expand "sigma" )"2" expand "sigma" )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" case "EXISTS (z:real): polynomial(a,j+1)(z)=0" )"1" "1" "polynomial_zero_factor" )"1" "1" replace -2)"1" "1" "IP" "%1" )"1" replace -1)"1" "g!1" )"1" "1" "IG" "%1" )"1" replace -1)"1" case "IP = union(IG,singleton(z))" )"1" "finite_union[real]" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "2" "2" expand "IP" "2" expand "IG" "2" expand "union" "2" expand "singleton" "2" expand "member" "2" "1" "x!1" )"1" replace "1" assert )nil nil ))nil ))nil )"2" "x!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "polynomial_eq_coeff" )"2" "a" "LAMBDA (i:nat): 0" "j+1" )"2" "2" "2" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil )"2" "2" case "polynomial(LAMBDA (i: nat): 0, 1 + j)(x!1) = 0" )"1" "1" assert )"1" "x!1" )"1" case "polynomial(g!1, j)(x!1) = 0" )"1" assert )nil nil )"2" expand "polynomial" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "i!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "polynomial" "2" rewrite "sigma_restrict_eq_0" )"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 )"2" "finite_emptyset[real]" )"2" case "%1 = %2" )"1" (assert ) nil nil )"2" "2" "2" expand "emptyset" 1)"2" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"[bool, bool -> bool]" booleans 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" sigma "reals/" )"bool" booleans nil )nil naturalnumbers nil )"bool" reals nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"boolean" notequal nil )nil sequences nil )"[real -> real]" polynomials "reals/" )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"[real -> boolean]" poly_systems nil )"real" poly_systems nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"bool" functions nil )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )nil nat_types nil )"{a | permutation_of?(A, a) AND sorted?(a)}" "structures/" )"bool" sort_array "structures/" )"bool" permutations "structures/" )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )nil finite_sets nil )"set" sets nil )"finite_set" finite_sets nil )nil finite_sets nil )nil integers nil )"bool" reals nil )nil integers nil )"[real -> boolean]" poly_systems nil )"real" reals nil )"[real -> boolean]" poly_systems nil )"(singleton?)" sets nil )"bool" sets nil )"(nonempty?)" sets nil )"non_empty_finite_set" finite_sets nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil integers nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )nil sigma "reals/" )nil sigma "reals/" )"nat" poly_systems nil )"nat" poly_systems nil )nil naturalnumbers nil )nil polynomials "reals/" )"real" reals nil )nil polynomials "reals/" )nil defined_types nil )nil naturalnumbers nil )"[nat -> [real -> boolean]]" nil )"posint" nil )"bool" sets nil )nil finite_sets nil )"nat" poly_systems nil )"set" sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"[nat -> [real -> boolean]]" poly_systemsnil )AND const-decl "[bool, bool -> bool]" booleans nil ))nil ))nil 3618843949"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" ))nil ))nil 3621242993"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"nat" sigma_nat "reals/" )"nnreal" sigma_nat "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" ))nil ))nil 3618918694"" (lemma "system_roots_enum" )"" (skeep)"" (inst - "k" "n" "p" )"" (assert )"" (replace -2)"" (skeep)"" (label "fmz" -1)"" (label "skz" -3)"" "Q" "prod_polynomials LAMBDA (i: nat): 1), k)") "" (replace -1)"" (name "Qdeg" "sigma(0, k, n)" )"" (replace -1)"" case "NOT FORALL (x): polynomial(Q,Qdeg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i))" )"1" (hide 2)"1" "1" "Q" )"1" case "NOT n * (LAMBDA (i: nat): 1) = n" )"1" "1" expand "*" 1)"1" (propax) nil nil ))nil ))nil )"2" replace -1)"2" "x" )"2" replace -5)"2" replace -2)"2" "1" "product_eq_0[nat]" )"1" "1" assert )"1" "1" expand "^" -1)"1" expand "expt" "1" expand "expt" "1" "skz" "x" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" assert )"2" "product_eq_zero[nat]" )"2" "2" assert )"2" "i!1" )"2" "2" "j!1" )"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 )"2" (assert )"2" "1" "1" "1" case "K = 0" )"1" "1" "i" )"1" assert )"1" "poly_sign_near_infinity" )"1" "p(i)" "n(i)" )"1" assert )"1" "i" )"1" assert )"1" assert )"1" "1" "1" expand "sign_ext" "1" expand "sign_ext" "1" assert )"1" "x" )"1" assert )"1" "M" )"1" assert )"1" "1" "1" "poly_intermediate_value_dec" )"1" "p(i)" "0" "n(i)" "x" "M" )"1" assert )"1" "1" "cc!1" "i" )"1" assert )"1" 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 )"2" case "x > enum(K-1)" )"1" "poly_sign_near_infinity" )"1" case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): AND ") "1" "k" )"1" assert )"1" "1" "1" "1" case "NOT FORALL (x: real): ") "1" "1" "x!1" "i" )"1" assert )"1" expand "sign_ext" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "MM" "max(M,x+1)" )"2" "MM" )"2" "i" )"2" assert )"2" "poly_intermediate_value_dec" )"2" "p(i)" "0" "n(i)" "x" "MM" )"2" assert )"2" "2" "cc!1" "i" )"2" assert )"2" "2" "i!2" "K-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M,M!1)" )"1" "1" case "j = 1+j!1" )"1" "x!1" )"1" assert )nil nil ))nil )"2" "x!1" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "x < enum(0)" )"1" "1" "1" "poly_sign_near_negative_infinity" )"1" case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): AND IF odd?(n(j)) THEN -1 ELSE 1 ENDIF) *p(j)(n(j))))") "1" "k" )"1" assert )"1" "1" "1" "MM" "min(-M,x-1)" )"1" case "NOT EXISTS (cc:real): MM<=cc AND cc<=x AND polynomial(p(i),n(i))(cc)=0" )"1" "i" )"1" assert )"1" "MM" "i" )"1" assert )"1" case "NOT sign_ext((IF odd?(n(i)) THEN -1 ELSE 1 ENDIF) * p(i)(n(i))) = -1" )"1" "i" )"1" assert )"1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "sign_ext" "2" "2" "2" "poly_intermediate_value_inc" )"2" "p(i)" "0" "n(i)" "MM" "x" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cc" "i" )"2" assert )"2" "2" "0" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "x!1" )"1" assert )"1" "even_or_odd" )"1" "n(0)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M,M!1)" )"1" "1" case "j = 1+j!1" )"1" "x!1" )"1" assert )"1" "even_or_odd" )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT EXISTS (i:nat): i+1<K AND enum(i)<x AND x<enum(i+1)" )"1" "Nset" "{nm:nat | nm+1<K aNd enum(nm)<x}" )"1" "lub_nat" )"1" "Nset" "K+1" )"1" assert )"1" "1" "i" )"1" "i" )"1" "i" )"1" expand "Nset" "1" "1" assert )"1" case "enum(1+i)=x" )"1" "1+i" )"1" "1" assert )"1" "j" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" "2" "1+i" )"1" assert )nil nil )"2" expand "extend" "2" expand "Nset" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "upper_bound?" "2" "2" "s!1" )"2" expand "extend" "2" "1" "1" expand "Nset" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" "2" "0" )"2" assert )"2" case "NOT K>1" )"1" case "NOT x = enum(0)" )"1" assert )nil nil )"2" "0" )"2" "2" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "x = enum(0)" )"1" "0" )"1" "1" "j" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" expand "empty?" )"2" "0" )"2" expand "member" )"2" expand "Nset" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" "poly_Rolle" )"2" "Q" "Qdeg" "enum(i)" "enum(i+1)" )"2" assert )"2" assert )"2" case "NOT Qdeg > 0" )"1" assert )"1" "1" "Q" )"1" case "FORALL (j): j<=k IMPLIES n(j)=0" )"1" "1" "i!1" )"1" "i!1" )"1" assert )"1" replace "1" expand "polynomial" "1" expand "sigma" "1" expand "sigma" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (pz:nat): pz<=k AND sigma[nat](0, pz, LAMBDA (j): n(j)) = 0 IMPLIES FORALL (j): j <= pz IMPLIES n(j) = 0" )"1" "k" )"1" assert )"1" replace "1" case "NOT n = n*(LAMBDA (i:nat): 1)" )"1" "1" expand "*" )"1" nil nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" assert )"2" "sigma_tolambda" )"2" "n" "k" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "pz" )"1" assert )"1" "1" "1" expand "sigma" "1" expand "sigma" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "izp" "2" assert )"2" "1" "1" case "NOT j = j!1+1" )"1" "j" )"1" assert )nil nil ))nil )"2" replace "2" assert )"2" expand "sigma" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sigma" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "1" "1" "c!1" )"1" assert )"1" "iii" )"1" "1" "iii" )"1" assert )"1" case "x < c!1" )"1" "poly_intermediate_value_dec" )"1" "p(iii)" "0" "n(iii)" "x" "c!1" )"1" assert )"1" "1" "skz" )"1" "cc!1" "iii" )"1" assert )"1" "1" "fmz" )"1" "i!3" "i" )"1" "1+i" "i!3" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_inc" )"2" "p(iii)" "0" "n(iii)" "c!1" "x" )"2" assert )"2" "2" "skz" )"2" "cc!1" "iii" )"2" assert )"2" "2" "fmz" )"2" "i!3" "i" )"2" "1+i" "i!3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "enum(i)" )"2" "enum(1+i)" )"2" assert )"2" "2" "2" "2" "1" "1" assert )nil nil )"2" "i" )nil nil ))nil )"2" "1+i" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil )"3" (assert ) nil nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" "poly_sign_near_infinity" )"1" case "FORALL (j): j<=k IMPLIES EXISTS (M:posnat): FORALL (i): i<=j IMPLIES FORALL (x:real):x >= M IMPLIES sign_ext(polynomial(p(i), n(i))(x)) = sign_ext(p(i)(n(i)))" )"1" "k" )"1" assert )"1" "1" "M" )"1" "1" "i" )"1" assert )"1" "M" )"1" assert )"1" "i" )"1" assert )"1" expand "sign_ext" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "j" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "1" "x" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" "1" "1" "max(M!1,M)" )"1" "1" case "i = 1+j!1" )"1" "1" "x" )"1" assert )nil nil ))nil ))nil )"2" "i" )"2" assert )"2" "2" "x" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" )"2" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (j): j<=k IMPLIES EXISTS (M:posnat): FORALL (i): i<=j IMPLIES FORALL (x:real):x <= -M IMPLIES sign_ext(polynomial(p(i), n(i))(x)) = sign_ext((IF even?(n(i)) THEN 1 ELSE -1 ENDIF)*p(i)(n(i)))" )"1" "k" )"1" assert )"1" "1" "-M" )"1" "1" "i" )"1" assert )"1" "-M" )"1" assert )"1" "i" )"1" "even_or_odd" )"1" "n(i)" )"1" "1" expand "sign_ext" )"1" "1" assert )"1" "1" assert )"1" "1" assert )"1" "1" "1" assert )"1" "1" assert )"1" 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" "j" )"1" assert )"1" "poly_sign_near_negative_infinity" )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "1" "x" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "poly_sign_near_negative_infinity" )"2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M!1,M!2)" )"1" "1" case " i = 1+j!1" )"1" "1" "x" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "i" )"2" assert )"2" "2" "x" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (inst + "x" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nat" sigma_nat "reals/" )"nnreal" sigma_nat "reals/" )"bool" integers nil )nil more_polynomial_props"reals/" )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" "reals/" )"odd_int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )nil polynomials "reals/" )nil integers nil )nil integers nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"nzint" integers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" integers nil )"real" reals nil )nil polynomials "reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" reals nil )nil naturalnumbers nil )"int" integers nil )nil "reals/" )"[nat -> nat]" poly_systems nil )nil sigma_nat "reals/" )"nonneg_int" nil )nil polynomials "reals/" )set type-eq-decl nil sets nil )"bool" sets nil )"[nat -> boolean]" poly_systems nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"(Nset)" poly_systems nil )"R" extend nil )"bool" booleans nil )"bool" sets nil )"bool" sets nil )"odd_int" integers nil )nil integer_props nil )nil defined_types nil )nil naturalnumbers nil )"posint" nil )"posint" nil )"{s: posrat | s >= q AND s >= r}" nil )"{k: posint | i <= k AND j <= k}" nil )"real" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" integers nil )"real" exponentiation nil )nil product "reals/" )"nat" poly_systems nil )"nat" poly_systems nil )nil product "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )nil naturalnumbers nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )nil sequences nil )"[real -> real]" polynomials "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[T -> real]" real_fun_ops "reals/" )nil product "reals/" )nil product "reals/" )"real" product "reals/" )"boolean" notequal nil )"real" exponentiation nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"{a | LAMBDA (j): polynomial(GF(j), KF(j))(x) ^ GP(j)))AND AND GP(i) /= 0 IMPLIES GF(i)(KF(i)) /= 0)AND (FORALL (i): i > sigma(0, k, KF * GP) IMPLIES a(i) = 0)}" 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 poly_systems nil ))nil )nil 3618918595"" (lemma "system_roots_enum" )"" (skeep)"" (inst - "k" "n" "p" )"" (assert )"" (replace -2)"" (skeep)"" (label "skz" -3)"" (name "Q" "prod_upto(p, n, k)" )"" (replace -1)"" case "NOT FORALL (x): polynomial(Q`poly,Q`deg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i))" )"1" (hide 2)"1" (skeep)"1" (typepred "Q" )"1" (inst - "x" )"1" replace -2)"1" "1" "product_eq_0[nat]" )"1" "1" assert )"1" "1" "x" "n!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" "product_eq_zero[nat]" )"1" "1" assert )"1" "1" "i!1" )"1" "1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (split 1)"1" (flatten)"1" (skeep -1)"1" (case "K = 0" )"1" "1" "i" )"1" assert )"1" "poly_sign_near_infinity" )"1" "p(i)" "n(i)" )"1" assert )"1" "i" )"1" assert )"1" assert )"1" "1" "1" expand "sign_ext" "1" expand "sign_ext" "1" assert )"1" "x" )"1" assert )"1" "M" )"1" assert )"1" "1" "1" "poly_intermediate_value_dec" )"1" "p(i)" "0" "n(i)" "x" "M" )"1" assert )"1" "1" "cc!1" "i" )"1" assert )"1" 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 )"2" case "x > enum(K-1)" )"1" "poly_sign_near_infinity" )"1" case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): AND ") "1" "k" )"1" assert )"1" "1" "1" "1" case "NOT FORALL (x: real): ") "1" "1" "x!1" "i" )"1" assert )"1" expand "sign_ext" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "MM" "max(M,x+1)" )"2" "MM" )"2" "i" )"2" assert )"2" "poly_intermediate_value_dec" )"2" "p(i)" "0" "n(i)" "x" "MM" )"2" assert )"2" "2" "cc!1" "i" )"2" assert )"2" "2" "i!2" "K-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M,M!1)" )"1" "1" case "j = 1+j!1" )"1" "x!1" )"1" assert )nil nil ))nil )"2" "x!1" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "x < enum(0)" )"1" "1" "1" "poly_sign_near_negative_infinity" )"1" case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): AND IF odd?(n(j)) THEN -1 ELSE 1 ENDIF) *p(j)(n(j))))") "1" "k" )"1" assert )"1" "1" "1" "MM" "min(-M,x-1)" )"1" case "NOT EXISTS (cc:real): MM<=cc AND cc<=x AND polynomial(p(i),n(i))(cc)=0" )"1" "i" )"1" assert )"1" "MM" "i" )"1" assert )"1" case "NOT sign_ext((IF odd?(n(i)) THEN -1 ELSE 1 ENDIF) * p(i)(n(i))) = -1" )"1" "i" )"1" assert )"1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "sign_ext" "2" "2" "2" "poly_intermediate_value_inc" )"2" "p(i)" "0" "n(i)" "MM" "x" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cc" "i" )"2" assert )"2" "2" "0" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "x!1" )"1" assert )"1" "even_or_odd" )"1" "n(0)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M,M!1)" )"1" "1" case "j = 1+j!1" )"1" "x!1" )"1" assert )"1" "even_or_odd" )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT EXISTS (i:nat): i+1<K AND enum(i)<x AND x<enum(i+1)" )"1" "Nset" "{nm:nat | nm+1<K aNd enum(nm)<x}" )"1" "lub_nat" )"1" "Nset" "K+1" )"1" assert )"1" "1" "i" )"1" "i" )"1" "i" )"1" expand "Nset" "1" "1" assert )"1" case "enum(1+i)=x" )"1" "1+i" )"1" "1" assert )"1" "j" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" "2" "1+i" )"1" assert )nil nil )"2" expand "extend" "2" expand "Nset" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "upper_bound?" "2" "2" "s!1" )"2" expand "extend" "2" "1" "1" expand "Nset" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" 1)"2" "0" )"2" assert )"2" case "NOT K>1" )"1" case "NOT x = enum(0)" )"1" assert )nil nil )"2" "0" )"2" "2" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "x = enum(0)" )"1" "0" )"1" "1" "j" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" expand "empty?" )"2" "0" )"2" expand "member" )"2" expand "Nset" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" "2" "poly_Rolle" )"2" "Q`poly" "Q`deg" "enum(i)" "enum(i+1)" )"2" assert )"2" assert )"2" case "NOT Q`deg > 0" )"1" assert )"1" "1" "Q" )"1" case "FORALL (j): j<=k IMPLIES n(j)=0" )"1" "1" "i!1" )"1" "i!1" )"1" assert )"1" replace "1" expand "polynomial" "1" expand "sigma" "1" expand "sigma" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (pz:nat): pz<=k AND sigma[nat](0, pz, LAMBDA (j): n(j)) = 0 IMPLIES FORALL (j): j <= pz IMPLIES n(j) = 0" )"1" "k" )"1" assert )nil nil ))nil )"2" "pz" )"1" assert )"1" "1" "1" expand "sigma" "1" expand "sigma" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "izp" "2" assert )"2" "1" "1" case "NOT j = j!1+1" )"1" "j" )"1" assert )nil nil ))nil )"2" replace "2" assert )"2" expand "sigma" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sigma" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "1" "1" "c!1" )"1" assert )"1" "iii" )"1" "1" "iii" )"1" assert )"1" case "x < c!1" )"1" "poly_intermediate_value_dec" )"1" "p(iii)" "0" "n(iii)" "x" "c!1" )"1" assert )"1" "1" "skz" )"1" "cc!1" "iii" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (postpone) nil nil ))nil )"3" (postpone) nil nil ))nil )"3" (postpone) nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3618918536"" (lemma "system_roots_enum" )"" (skeep)"" (inst - "k" "n" "p" )"" (assert )"" (replace -2)"" (skeep)"" (label "skz" -4)"" (name "Q" "prod_upto(p, n, k)" )"" (replace -1)"" case "NOT FORALL (x): polynomial(Q`poly,Q`deg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i))" )"1" (hide 2)"1" (skeep)"1" (typepred "Q" )"1" (inst - "x" )"1" replace -2)"1" "1" "product_eq_0[nat]" )"1" "1" assert )"1" "1" "x" "n!1" )"1" (assert ) nil )))))))))"2" "2" (assert ) nil )))))"2" "product_eq_zero[nat]" )"1" "1" assert )"1" "1" "i!1" )"1" "1" "j!1" )"1" assert )nil )))))))))))))"2" "2" assert )nil )))))))))))))))))"2" (split 1)"1" (flatten)"1" (skeep -1)"1" (case "K = 0" )"1" "1" "i" )"1" assert )"1" "poly_sign_near_infinity" )"1" "p(i)" "n(i)" )"1" assert )"1" "i" )"1" assert )"1" assert )"1" "1" "1" expand "sign_ext" "1" expand "sign_ext" "1" assert )"1" "x" )"1" assert )"1" "M" )"1" assert )"1" "1" "1" "poly_intermediate_value_dec" )"1" "p(i)" "0" "n(i)" "x" "M" )"1" assert )"1" "1" "cc!1" "i" )"1" assert )"1" nil )))))))))))))))))))))))))))))))))))))))))))))))))))))"2" case "x > enum(K-1)" )"1" "poly_sign_near_infinity" )"1" case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): AND ") "1" "k" )"1" assert )"1" "1" "1" "1" case "NOT FORALL (x: real): ") "1" "1" "x!1" "i" )"1" assert )"1" expand "sign_ext" "1" "1" nil )))))))))))"2" "MM" "max(M,x+1)" )"2" "MM" )"2" "i" )"2" assert )"2" "poly_intermediate_value_dec" )"2" "p(i)" "0" "n(i)" "x" "MM" )"2" assert )"2" "2" "cc!1" "i" )"2" assert )"2" "2" "i!2" "K-1" )"2" assert )nil )))))))))))))))))))))))))))))))))))))"2" "jp" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "x!1" )"1" assert )nil )))))))))"2" "0" )"2" assert )nil )))))))))))"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M,M!1)" )"1" "1" case "j = 1+j!1" )"1" "x!1" )"1" assert )nil )))"2" "x!1" "j" )"2" assert )nil )))))))))))"2" "1+j!1" )"2" assert )nil )))))))))))))))))))))"2" case "x < enum(0)" )"1" "1" "1" "poly_sign_near_negative_infinity" )"1" case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): AND IF odd?(n(j)) THEN -1 ELSE 1 ENDIF) *p(j)(n(j))))") "1" "k" )"1" assert )"1" "1" "1" "MM" "min(-M,x-1)" )"1" case "NOT EXISTS (cc:real): MM<=cc AND cc<=x AND polynomial(p(i),n(i))(cc)=0" )"1" "i" )"1" assert )"1" "MM" "i" )"1" assert )"1" case "NOT sign_ext((IF odd?(n(i)) THEN -1 ELSE 1 ENDIF) * p(i)(n(i))) = -1" )"1" "i" )"1" assert )"1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" nil )))))))))))))))))"2" replace "2" expand "sign_ext" "2" "2" "2" "poly_intermediate_value_inc" )"2" "p(i)" "0" "n(i)" "MM" "x" )"2" assert )nil )))))))))))))))))))))))"2" "2" "cc" "i" )"2" assert )"2" "2" "0" "i!1" )"2" assert )nil )))))))))))))))))))))))"2" "jp" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "x!1" )"1" assert )"1" "even_or_odd" )"1" "n(0)" )"1" "1" nil )))))))))))))))))"2" "0" )"2" assert )nil )))))))))))"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M,M!1)" )"1" "1" case "j = 1+j!1" )"1" "x!1" )"1" assert )"1" "even_or_odd" )"1" "1" "1" nil )))))))))))"2" "x!1" "j" )"2" assert )nil )))))))))))"2" "1+j!1" )"2" assert )nil )))))))))))))))))))))))))"2" case "NOT EXISTS (i:nat): i+1<K AND enum(i)<x AND x<enum(i+1)" )"1" "Nset" "{nm:nat | nm+1<K aNd enum(nm)<x}" )"1" "lub_nat" )"1" "Nset" "K+1" )"1" assert )"1" "1" "i" )"1" "i" )"1" "i" )"1" expand "Nset" "1" "1" assert )"1" case "enum(1+i)=x" )"1" "1+i" )"1" "1" assert )"1" "j" )"1" assert )nil )))))))))"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" "2" "1+i" )"1" assert )nil )"2" expand "extend" "2" expand "Nset" "2" assert )nil )))))))))))))))))))))))))))"2" expand "upper_bound?" "2" "2" "s!1" )"2" expand "extend" "2" "1" "1" expand "Nset" "1" "1" assert )nil )))))))"2" nil )))))))))))))))"2" expand "nonempty?" 1)"2" "0" )"2" assert )"2" case "NOT K>1" )"1" case "NOT x = enum(0)" )"1" (assert ) nil )"2" "0" )"2" "2" "j" )"2" assert )nil )))))))))"2" assert )"2" case "x = enum(0)" )"1" "0" )"1" "1" "j" )"1" assert )nil )))))))"2" assert )"2" assert )"2" expand "empty?" )"2" "0" )"2" expand "member" )"2" expand "Nset" "2" nil )))))))))))))))))))))))))))))"2" "2" (assert ) nil )))))"2" "2" "poly_Rolle" )"2" "Q`poly" "Q`deg" "enum(i)" "enum(i+1)" )"2" assert )"2" assert )"2" case "NOT Q`deg > 0" )"1" assert )"1" "1" "Q" )"1" case "FORALL (j): j<=k IMPLIES n(j)=0" )"1" "1" "i!1" )"1" "i!1" )"1" assert )"1" replace "1" expand "polynomial" "1" expand "sigma" "1" expand "sigma" "1" nil )))))))))))))))))"2" case "FORALL (pz:nat): pz<=k AND sigma[nat](0, pz, LAMBDA (j): n(j)) = 0 IMPLIES FORALL (j): j <= pz IMPLIES n(j) = 0" )"1" "k" )"1" assert )nil )))"2" "pz" )"1" assert )"1" "1" "1" expand "sigma" "1" expand "sigma" "1" assert )nil )))))))))))"2" "2" "izp" "2" assert )"2" "1" "1" case "NOT j = j!1+1" )"1" "j" )"1" assert )nil )))"2" replace "2" assert )"2" expand "sigma" "2" assert )nil )))))))))))"2" expand "sigma" "2" assert )nil )))))))))))))))))))))))"2" assert )"2" "1" "1" "c!1" )"1" assert )"1" "iii" )"1" "1" "iii" )"1" assert )"1" case "x < c!1" )"1" "poly_intermediate_value_dec" )"1" "p(iii)" "0" "n(iii)" "x" "c!1" )"1" assert )"1" "1" nil )))))))))"2" nil )))))))))))))))))"2" nil )))))))))))))))))"3" (postpone) nil )))"3" (postpone) nil )))"3" (postpone) nil )))))))))"2" (postpone) nil ))))))))))))))))))))))nil )nil nil )nil 3618842027"" (lemma "system_roots_enum" )"" (skeep)"" (inst - "k" "n" "p" )"" (assert )"" (replace -2)"" (skeep)"" (name "Q" "prod_upto(p, n, k)" )"" (replace -1)"" case "NOT FORALL (x): polynomial(Q`poly,Q`deg)(x)=0 IFF (EXISTS (i:below(K)): x = enum(i))" )"1" (hide 2)"1" (skeep)"1" (typepred "Q" )"1" (inst - "x" )"1" (replace -2)"1" "1" "product_eq_0[nat]" )"1" "1" assert )"1" "1" "x" "n!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" "product_eq_zero[nat]" )"1" "1" assert )"1" "1" "i!1" )"1" "1" "j!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (split 1)"1" (flatten)"1" (skeep -1)"1" (case "K = 0" )"1" (skeep 1)"1" "i" )"1" assert )"1" "poly_sign_near_infinity" )"1" "p(i)" "n(i)" )"1" assert )"1" "i" )"1" assert )"1" assert )"1" "1" "1" expand "sign_ext" "1" expand "sign_ext" "1" assert )"1" "x" )"1" assert )"1" "M" )"1" assert )"1" "1" "1" "poly_intermediate_value_dec" )"1" "p(i)" "0" "n(i)" "x" "M" )"1" assert )"1" "1" "cc!1" "i" )"1" assert )"1" 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 )"2" (case "x > enum(K-1)" )"1" "poly_sign_near_infinity" )"1" case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): AND ") "1" "k" )"1" assert )"1" "1" "1" "1" case "NOT FORALL (x: real): ") "1" "1" "x!1" "i" )"1" assert )"1" expand "sign_ext" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "MM" "max(M,x+1)" )"2" "MM" )"2" "i" )"2" assert )"2" "poly_intermediate_value_dec" )"2" "p(i)" "0" "n(i)" "x" "MM" )"2" assert )"2" "2" "cc!1" "i" )"2" assert )"2" "2" "i!2" "K-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M,M!1)" )"1" "1" case "j = 1+j!1" )"1" "x!1" )"1" assert )nil nil ))nil )"2" "x!1" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "x < enum(0)" )"1" "1" "1" "poly_sign_near_negative_infinity" )"1" case "FORALL (jp:nat): jp<=k IMPLIES (EXISTS (M: posnat): AND IF odd?(n(j)) THEN -1 ELSE 1 ENDIF) *p(j)(n(j))))") "1" "k" )"1" assert )"1" "1" "1" "MM" "min(-M,x-1)" )"1" case "NOT EXISTS (cc:real): MM<=cc AND cc<=x AND polynomial(p(i),n(i))(cc)=0" )"1" "i" )"1" assert )"1" "MM" "i" )"1" assert )"1" case "NOT sign_ext((IF odd?(n(i)) THEN -1 ELSE 1 ENDIF) * p(i)(n(i))) = -1" )"1" "i" )"1" assert )"1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" expand "sign_ext" "2" "2" "2" "poly_intermediate_value_inc" )"2" "p(i)" "0" "n(i)" "MM" "x" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "cc" "i" )"2" assert )"2" "2" "0" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "jp" )"1" assert )"1" "p(0)" "n(0)" )"1" assert )"1" "1" "1" "M" )"1" "1" "x!1" )"1" assert )"1" "even_or_odd" )"1" "n(0)" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "p(1+j!1)" "n(1+j!1)" )"2" assert )"2" "1" "1" "max(M,M!1)" )"1" "1" case "j = 1+j!1" )"1" "x!1" )"1" assert )"1" "even_or_odd" )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT EXISTS (i:nat): i+1<K AND enum(i)<x AND x<enum(i+1)" )"1" "Nset" "{nm:nat | nm+1<K aNd enum(nm)<x}" )"1" "lub_nat" )"1" "Nset" "K+1" )"1" assert )"1" "1" "i" )"1" "i" )"1" "i" )"1" expand "Nset" -1)"1" "1" assert )"1" case "enum(1+i)=x" )"1" "1+i" )"1" "1" assert )"1" "j" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" "2" "1+i" )"1" assert )nil nil )"2" expand "extend" "2" expand "Nset" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "upper_bound?" 1)"2" "2" "s!1" )"2" expand "extend" "2" "1" "1" expand "Nset" "1" "1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" 1)"2" "0" )"2" assert )"2" case "NOT K>1" )"1" case "NOT x = enum(0)" )"1" assert )nil nil )"2" "0" )"2" "2" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "x = enum(0)" )"1" "0" )"1" "1" "j" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" expand "empty?" )"2" "0" )"2" expand "member" )"2" expand "Nset" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" "2" "poly_Rolle" )"2" "Q`poly" "Q`deg" "enum(i)" "enum(i+1)" )"2" assert )"2" assert )"2" case "NOT Q`deg > 0" )"1" assert )"1" "1" "Q" )"1" case "FORALL (j): j<=k IMPLIES n(j)=0" )"1" "1" "i!1" )"1" "i!1" )"1" assert )"1" replace "1" expand "polynomial" "1" expand "sigma" "1" expand "sigma" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (pz:nat): pz<=k AND sigma[nat](0, pz, LAMBDA (j): n(j)) = 0 IMPLIES FORALL (j): j <= pz IMPLIES n(j) = 0" )"1" "k" )"1" assert )nil nil ))nil )"2" "pz" )"1" assert )"1" "1" "1" expand "sigma" "1" expand "sigma" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "izp" "2" assert )"2" "1" "1" case "NOT j = j!1+1" )"1" "j" )"1" assert )nil nil ))nil )"2" replace "2" assert )"2" expand "sigma" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sigma" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "1" "1" "c!1" )"1" assert )"1" "iii" )"1" "1" "iii" )"1" assert )"1" case "x < c!1" )"1" "poly_intermediate_value_dec" )"1" "p(iii)" "0" "n(iii)" "x" "c!1" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (postpone) nil nil ))nil )"3" (postpone) nil nil ))nil )"3" (postpone) nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3621258003"" (skeep)"" (rewrite "length_row" ) (("" (assert ) nil nil )) nil )) nil )nil matrix_props "matrices/" )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 matrices "matrices/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices "matrices/" )"bool" reals nil )"nat" matrices "matrices/" )"bool" reals nil )"{c: nat | AND AND c = 0 OR " "matrices/" )nil matrices "matrices/" )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" nil )nil integers nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621258003"" (skeep)"" (assert )"" (typepred "vect2matrix(row(A63)(RelF6(0)))" )"" (assert )"" (replace -6)"" (rewrite "length_row" 1)"" (assert )"" (replace -7)"" (expand "^" + 1)"" (expand "expt" )"" (expand "expt" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )nil matrix_props "matrices/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"real" exponentiation nil )"real" exponentiation nil )"posint" exponentiation nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers 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 matrices "matrices/" )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 )"nat" list_props nil )nil matrices "matrices/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"bool" reals nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices "matrices/" )"nat" matrices "matrices/" )"bool" reals nil )"{c: nat | AND AND c = 0 OR " "matrices/" )nil matrices "matrices/" )"{PFM | rows(PFM) = 1 AND columns(PFM) = length(v)}" matrices"matrices/" )"Vector" matrices "matrices/" )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" nil )nil integers nil ))nil ))nil 3621258003"" (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 )"int" integers nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" ))nil ))nil 3621258003"" (skeep) (("" (assert ) nil nil )) nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" ))nil ))nil 3621258003"" (skeep)"" (rewrite "length_row" ) (("" (assert ) nil nil )) nil )) nil )nil matrix_props "matrices/" )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 matrices "matrices/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices "matrices/" )"bool" reals nil )"nat" matrices "matrices/" )"bool" reals nil )"{c: nat | AND AND c = 0 OR " "matrices/" )nil matrices "matrices/" )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" nil )nil integers nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3621258003"" (skeep)"" (rewrite "tensor_rows" )"" (assert )"" (expand "tensor_prod" )"" (lemma "columns_form_matrix" )"" (inst?)"" (assert )"" (replaces -1)"" (expand "vect2matrix" )"" (lemma "columns_form_matrix" )"" (inst?)"" (assert )"" (replaces -1)"" (rewrite "length_row" )"" assert )"" "v(m - 1)(LAMBDA (d): RelF6(1 + d))" )"" "" "" expand "^" )"" expand "expt" + 2)"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"posint" nil )"int" integers nil )nil tensor_product "matrices/" )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 matrices "matrices/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices "matrices/" )"bool" reals nil )"nat" matrices "matrices/" )"bool" reals nil )"{c: nat | AND AND c = 0 OR " "matrices/" )nil matrices "matrices/" )nil integers nil )nil integers nil )nil integers nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil matrices "matrices/" )"{PFM | rows(PFM) = 1 AND columns(PFM) = length(v)}" matrices"matrices/" )"Vector" matrices "matrices/" )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"PosFullMatrix" tensor_product "matrices/" )"posint" nil )"[[nat, nat] -> real]" tensor_product"matrices/" )"[numfield, numfield -> numfield]" number_fields nil )nil matrix_props "matrices/" )NOT const-decl "[bool -> bool]" booleans nil )"real" exponentiation nil )"posnat" exponentiation nil )"posint" nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" matrices "matrices/" )"FullMatrix" matrices"matrices/" )"posint" exponentiation nil )nil matrices "matrices/" ))nil ))nil 3621269302"" (skeep)"" (rewrite "length_row" )"" (lift-if)"" (ground)"" (lemma "tensor_power_rows_alt" )"" (inst?)"" (assert )"" (lemma "base_n_to_nat_lt" )"" (inst?)"" (split -)"1" (assert ) nil nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )nil matrix_props "matrices/" )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 matrices "matrices/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil reals nil )"[list -> boolean]" list_adt nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )"nat" list_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil nat_types nil )"T" list_props nil )nil matrices "matrices/" )"bool" reals nil )"nat" matrices "matrices/" )"bool" reals nil )"{c: nat | AND AND c = 0 OR " "matrices/" )nil matrices "matrices/" )nil integers nil )nil integers nil )"PosFullMatrix" tensor_product"matrices/" )"{M: PosFullMatrix | rows(M) = 6 AND columns(M) = 3}" nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )nil base_repr "reals/" )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"posint" exponentiation nil )"posint" nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )nil integers nil )"nat" exponentiation nil )nil tensor_product"matrices/" ))nil ))nil 3621269303"" (induct "k" )"1" (assert ) nil nil )"2" (skeep)"2" (rewrite "full_matrix_eq" )"2" (split)"1" (expand "vect2matrix" )"1" (rewrite "rows_form_matrix" ) (("1" (assert ) nil nil ))nil ))nil )"2" (expand "vect2matrix" )"2" (lemma "columns_form_matrix" )"2" (inst?)"2" (assert )"2" (replaces -1)"2" (rewrite "length_row" )"2" (lift-if)"2" (assert )"2" (ground)"1" (lemma "tensor_power_rows_alt" )"1" "1" assert )"1" rewrite "expt_x1" )"1" "base_n_to_nat_lt" )"1" "1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "tensor_power_columns_alt" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (assert )"3" (expand "A63_tensor_power_mat_row" )"3" (expand "vect2matrix" )"3" (rewrite "entry_form_matrix" )"3" (rewrite "entry_form_matrix" )"3" (assert )"3" (lift-if)"3" (lift-if)"3" (lift-if)"3" "1" rewrite "access_row" )"1" rewrite "access_row" )"1" expand "tensor_power_alt" )"1" expand "base_n_to_nat" )"1" expand "sigma" )"1" expand "sigma" )"1" rewrite "expt_x0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "length_row" )"2" rewrite "length_row" )"2" assert )"2" "2" "1" expand "base_n_to_nat" )"1" expand "sigma" )"1" expand "sigma" )"1" rewrite "expt_x0" )"1" "tensor_power_rows_alt" )"1" "1" assert )"1" rewrite "expt_x1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "tensor_power_columns_alt" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "length_row" )"3" "3" "3" rewrite "length_row" )"3" "tensor_power_columns_alt" )"3" "3" assert )"3" rewrite "expt_x1" )"3" 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 )"3" (skolem 1 "k" )"3" (flatten)"3" (skeep)"3" (assert )"3" (rewrite "full_matrix_eq" +)"3" (split)"1" (expand "vect2matrix" +)"1" (lemma "columns_form_matrix" )"1" (inst?)"1" (assert )"1" (replaces -1)"1" (rewrite "length_row" )"1" (lift-if)"1" "1" "base_n_to_nat_lt" )"1" "1" assert )"1" "1" "tensor_power_rows_alt" )"1" "1" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "tensor_power_columns_alt" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (case "NOT i = 0" )"1" (typepred "i" ) (("1" (assert ) nil nil )) nil )"2" (replace -1)"2" (assert )"2" (case "NOT j < 3^(2+k)" )"1" (assert ) nil nil )"2" (expand "vect2matrix" +)"2" (rewrite "entry_form_matrix" )"2" "2" "1" rewrite "access_row" )"1" expand "A63_tensor_power_mat_row" "1" expand "tensor_prod" )"1" rewrite "entry_form_matrix" )"1" "1" assert )"1" "1" expand "tensor_fun" )"1" "1" replace -5 +)"1" expand "vect2matrix" "1" rewrite "entry_form_matrix" )"1" "1" "1" rewrite "access_row" )"1" expand "vect2matrix" "1" "columns_form_matrix" )"1" "1" "1" assert )nil nil )"2" "2" expand "vect2matrix" "2" "columns_form_matrix" )"2" "2" assert )"2" "2" assert )"2" expand "vect2matrix" "2" rewrite "entry_form_matrix" )"1" "1" "1" rewrite "access_row" )"1" expand "vect2matrix" "1" "columns_form_matrix" )"1" "1" "1" assert )nil nil )"2" "2" assert )"2" rewrite "length_row" )"2" case "NOT columns(A63)=3" )"1" assert )nil nil )"2" replace "2" assert )"2" expand "tensor_power_alt" "2" expand "tensor_prod" "2" rewrite "entry_form_matrix" "2" "2" "1" expand "tensor_fun" "1" assert )"1" case "NOT rows(A63)=6" )"1" assert )nil nil )"2" replace "2" assert )"2" case "base_n_to_nat(6, LAMBDA (d): RelF6(1 + d), k) = (base_n_to_nat(6, RelF6, 1 + k) - ") "1" replace "1" case "mod(base_n_to_nat(6, RelF6, 1 + k), 6) = RelF6(0)" )"1" assert )nil nil )"2" "2" case "FORALL (dd:nat): mod(base_n_to_nat(6, RelF6, dd), 6) = RelF6(0)" )"1" nil nil )"2" "dd" )"1" expand "base_n_to_nat" "1" expand "sigma" )"1" expand "sigma" )"1" rewrite "expt_x0" )"1" assert )"1" expand "mod" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "dd" )"2" "2" assert )"2" expand "base_n_to_nat" "2" expand "sigma" "2" case "6^(1+dd) = 6*6^dd" )"1" replace "1" assert )"1" "mod_sum" )"1" "sigma(0, dd, LAMBDA (s: nat): 6 ^ s * RelF6(s))" "6" "(RelF6(1 + dd) * 6 ^ dd)" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" )"2" expand "expt" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" case "FORALL (dd:nat): mod(base_n_to_nat(6, RelF6, dd), 6) = RelF6(0)" )"1" "1+k" )"1" replace "1" assert )"1" expand "base_n_to_nat" "1" "sigma_split" )"1" "1+k" "1" "0" )"1" "1" assert )"1" "1" expand "sigma" "1" expand "sigma" "1" rewrite "expt_x0" )"1" assert )"1" "1" rewrite "sigma_scal" "1" "sigma_shift_to_zero" )"1" "1+k" "1" )"1" "1" assert )"1" "1" rewrite "sigma_eq" "1" "1" "1" expand "^" "1" expand "expt" "1" 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 )"2" "2" "dd" )"1" expand "base_n_to_nat" )"1" expand "sigma" )"1" expand "sigma" )"1" rewrite "expt_x0" )"1" assert )"1" expand "mod" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "dd" )"2" "2" expand "base_n_to_nat" "2" expand "sigma" "2" case "6^(1+dd) = 6*6^dd" )"1" "1" "mod_sum" )"1" "sigma(0, dd, LAMBDA (s: nat): 6 ^ s * RelF6(s))" "6" "(RelF6(1 + dd) * 6 ^ dd)" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "^" "2" expand "expt" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "base_n_to_nat_lt" )"2" "2" "1" "tensor_power_rows_alt" )"1" "1" assert )"1" "1" expand "^" )"1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "tensor_power_columns_alt" )"3" "3" assert )"3" "j" )"3" replace "3" case "3^(2+k) = 3^(1+k)* 3" )"1" assert )nil nil )"2" expand "^" "2" expand "expt" "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 )"2" "2" expand "vect2matrix" "2" "columns_form_matrix" )"2" "2" assert )"2" "mod_pos" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "length_row" )"2" expand "vect2matrix" "2" "columns_form_matrix" )"2" "2" "1" assert )nil nil )"2" "2"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.821 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
