Impressum sturmtarski.prf
Sprache: Lisp
(sturmtarskinil 3589569590"" (skeep)"" (skeep)"" (inst - "j1-2" "j1-1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3589569590"" (subtype-tcc) nil nil ) ((/= const-decl "boolean" notequal nil ))nil ))nil 3589569590"" (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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil ))nil ))nil 3589569590"" (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 )"bool" reals nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"boolean" notequal nil )"nonneg_int" nil ))nil ))nil 3619446702"" (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 )"bool" reals nil )nil integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"boolean" notequal nil )"nonneg_int" nil ))nil ))nil 3619446702"" (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 )"bool" reals nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"boolean" notequal nil )"nonneg_int" nil ))nil ))nil 3589570933"" (skeep)"" case "FORALL (i:nat): i-1>=0 AND i+1<=m AND polynomial(p(i),n(i))(x)=0 IMPLIES (polynomial(p(i-1),n(i-1))(x)=0 IFF polynomial(p(i+1),n(i+1))(x)=0)" )"1" (skeep)"1" case "FORALL (j:nat): i-j>=0 IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i-k), n(i-k))(x) = 0" )"1" case "FORALL (j:nat): i+j<=m IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i+k), n(i+k))(x) = 0" )"1" (skeep)"1" (case "j>=i" )"1" (inst - "j-i" )"1" (assert )"1" (inst - "j-i" ) (("1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil )"2" (inst -2 "i-j" )"1" (assert )"1" (inst -2 "i-j" ) (("1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (induct "j" )"1" (assert )"1" (skeep) (("1" (assert ) nil nil )) nil )) nil )"2" (assert )"2" (skosimp*)"2" (assert )"2" (case "k!1=0 OR k!1=1" )"1" (ground) nil nil )"2" (flatten)"2" (inst-cp - "k!1-1" )"2" (inst - "k!1-2" )"1" assert )"1" assert )"1" "i-1+k!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "j" )"1" (assert )"1" (skosimp*) (("1" (assert ) nil nil )) nil )) nil )"2" (skosimp*)"2" (assert )"2" (case "k!1=0" )"1" (assert ) nil nil )"2" (assert )"2" (inst-cp - "k!1-1" )"2" (case "k!1=1" )"1" (hide -2)"1" (assert )"1" "i" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (inst - "k!1-2" )"1" (assert )"1" "i-k!1+1" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (assert )"4" (skosimp*) (("4" (assert ) nil nil )) nil )) nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil )"6" (skosimp*) (("6" (assert ) nil nil )) nil )"7" (skosimp*) (("7" (assert ) nil nil )) nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (assert )"2" (expand "constructed_sturm_sequence?" )"2" (flatten)"2" (inst -11 "1+i" )"2" (assert )"2" (skeep)"2" "pd" "poly_divide(p(i - 1), n(i - 1))(p(i), n(i))(0)" )"2" (lemma "poly_divide_def" )"2" (inst?)"2" (assert )"2" replace -2)"2" assert )"2" "i" )"2" assert )"2" "i-1" "i" )"1" assert )"1" "x" )"1" assert )"1" replace -1)"1" replace -5)"1" assert )"1" case "polynomial(pd`rem, pd`rdeg)(x) = 0 IFF polynomial(-c*pd`rem, pd`rdeg)(x) = 0" )"1" replace -1 +)"1" replace "1" nil nil ))nil ))nil )"2" "2" rewrite "scal_polynomial2" )"2" "2" "c" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "NOT i = 1" )"1" (assert ) nil nil )"2" replace -1)"2" assert )"2" replace -13)"2" case "polynomial(pd`rem, pd`rdeg)(x) = 0 IFF polynomial(-c*pd`rem, pd`rdeg)(x) = 0" )"1" replace "1" "x" )"1" nil nil ))nil ))nil )"2" "2" rewrite "scal_polynomial2" )"2" "2" "c" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )"[real -> real]" polynomials "reals/" )nil sequences nil )"[T, T -> boolean]" equalities nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans 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 )"posint" nil )"int" integers nil )"nat" sturmtarski nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"posnat" sturmtarski nil )"upto(m)" sturmtarski nil )"nat" sturmtarski nil )"posint" nil )"(total_order?[real])" nil )"int" integers nil )nil naturalnumbers nil )"nonneg_int" nil )"nat" sturmtarski nil )"bool" sturmtarski nil )nil polynomial_division "Sturm/" )"real" reals nil )"nzreal" real_typesnil )"even_int" integersnil )"even_int" integersnil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"[numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil polynomials "reals/" )nil real_props nil )nil reals nil )"nnreal" nil )nil integers nil )"nat" sturmtarski nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"DivType" polynomial_division "Sturm/" )"boolean" notequal nil )nil polynomial_division "Sturm/" )"(strict_total_order?[real])" real_props nil ))nil ))nil 3617013590"" (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 )"bool" reals nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" exponentiation nil )"[real -> real]" polynomials "reals/" )"boolean" notequal nil )"real" reals nil ))nil ))nil 3617610964"" (subtype-tcc) nil nil )"boolean" notequal nil )"real" exponentiation nil )"[real -> real]" polynomials "reals/" )"real" reals nil ))nil ))nil 3617013872"" (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 )"bool" reals nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"boolean" notequal nil )"bool" sturmtarski nil )"real" exponentiation nil )"[real -> real]" polynomials "reals/" )"bool" sturmtarski nil )"nonneg_int" nil )"real" reals nil )"int" integers nil ))nil ))nil 3617123921"" (skeep)"" (label "css" -1)"" (case "g(k)=0" )"1" (expand "constructed_sturm_sequence?" )"1" (ground) nil nil )) nil )"2" "dd" "IF polynomial(g,k)(y)=0 THEN root_degree(p(0),n(0))(y) ELSE max(root_degree(p(0), n(0))(y) - 1, 0) ENDIF" )"2" case "FORALL (k,i:nat): i<=k AND k+1<m IMPLIES ((root_degree(p(i),n(i))(y)=dd OR root_degree(p(i+1),n(i+1))(y)=dd) AND (root_degree(p(i),n(i))(y)>=dd AND root_degree(p(i+1),n(i+1))(y)>=dd))" )"1" (case "root_degree(p(m-1),n(m-1))(y)=dd" )"1" (label "igz" -1)"1" (hide "igz" )"1" (assert )"1" (inst - "m-2" _)"1" (assert )"1" (lift-if)"1" (split -)"1" (flatten)"1" "root_degree_pos" )"1" "1" assert )"1" "1" expand "default_root_degree?" )"1" assert )"1" case "NOT (%1)" )"1" "1" "1" expand "constructed_sturm_sequence?" "1" "1" assert )"1" replace -4 +)"1" "root_degree_mult" )"1" "1" assert )"1" "y" )"1" assert )"1" "1" replace "1" "1" rewrite "root_degree_deriv" )"1" nil nil )"2" "0" )nil nil )"3" "root_degree_pos" )"3" "3" assert )"3" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" )"2" assert )"2" replace "2" replace "2" "2" expand "polynomial_prod" "2" expand "max" "2" expand "sigma" "2" expand "sigma" "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" "1" "1" replace -5)"1" assert )"1" "i-1" )"1" assert )"1" "1" "i" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "igz" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" assert )"2" "2" replace -1)"2" expand "default_root_degree?" )"2" case "NOT (%1)" )"1" "1" assert )"1" "1" assert )"1" case "polynomial(p(0),n(0))(y)/=0" )"1" "1" assert )"1" "root_degree_pos" )"1" "1" assert )"1" "1" "1" assert )nil nil )"2" expand "constructed_sturm_sequence?" )"2" "2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "root_degree_pos" )"2" "2" assert )"2" "root_degree_pos" )"2" "p(0)" "n(0)" "y" )"2" assert )"2" "1" expand "max" "1" assert )"1" assert )"1" "1" expand "constructed_sturm_sequence?" "1" "1" assert )"1" replace "1" replace "1" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" assert )nil nil )"2" "0" )nil nil ))nil )"2" "0" )"2" expand "poly_deriv" "2" assert )"2" "2" "n(0)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "constructed_sturm_sequence?" )"2" "2" "0" )"2" assert )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" "1" assert )"1" "1" "1" "i-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "2" "i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "igz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "constructed_sturm_sequence?" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide (3 4))"2" (inst - "m-2" "m-2" )"1" (assert )"1" (flatten)"1" (hide -2)"1" (hide -3)"1" (expand "constructed_sturm_sequence?" )"1" (flatten)"1" "m" )"1" assert )"1" "1" "pd" "poly_divide(p(m - 2), n(m - 2))(p(m - 1), n(m - 1)) ") "1" assert )"1" "poly_divide_def" )"1" "1" "m-1" )"1" assert )"1" replace -2)"1" "pr" "polynomial_prod(pd`quot,pd`qdeg,p(m-1),n(m-1))" )"1" case "NOT polynomial(pd`rem, pd`rdeg) = (LAMBDA (xyz:real): 0)" )"1" "1" "-c" )"1" "scal_polynomial2" )"1" "1" "x!1" )"1" "1" replace "1" expand "polynomial" "1" expand "sigma" "1" expand "sigma" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" assert )"2" "rd" "root_degree(p(m - 1), n(m - 1))(y)" )"2" "rd" )"2" assert )"2" "2" "2" "2" case "EXISTS (kk:nat): kk<=pd`qdeg AND pd`quot(kk)/=0 AND polynomial(pd`quot, pd`qdeg) = polynomial(pd`quot,kk)" )"1" "1" replace "1" assert )"1" "newprod" "polynomial_prod(b,n(m-1)-rd,pd`quot,kk)" )"1" "root_degree_lower_bound" )"1" "p(m-2)" "rd" "n(m-2)" "y" "n(m-1)-rd+kk" )"1" "1" "1" assert )nil nil ))nil )"2" "m-2" )"2" "m-2" )"2" "m-2" )nil nil ))nil ))nil )"3" "newprod" )"3" assert )"3" "1" expand "newprod" "1" expand "polynomial_prod" "1" expand "max" "1" expand "sigma" "1" expand "sigma" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x" )"2" replace "2" "x" )"2" replace "2" expand "newprod" "2" rewrite "polynomial_prod" )"2" rewrite "polynomial_prod_def" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "EXISTS (kk:nat): kk<=pd`qdeg AND pd`quot(kk)/=0" )"1" "1" case "EXISTS (kk:nat): kk<=pd`qdeg AND pd`quot(kk)/=0 AND FORALL (ii:nat): ii>kk AND ii<=pd`qdeg IMPLIES pd`quot(ii)=0" )"1" "1" "1" "kk" )"1" assert )"1" case "FORALL (jj:nat): kk+jj<=pd`qdeg IMPLIES polynomial(pd`quot, kk+jj) = polynomial(pd`quot, kk)" )"1" "pd`qdeg-kk" )"1" assert )nil nil ))nil )"2" "jj" )"1" assert )nil nil )"2" "2" assert )"2" "2" rewrite "polynomial_rec" "2" "1+j+kk" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "IZ" "{kk:posnat | kk<=pd`qdeg AND pd`quot(kk)/=0}" )"2" "M" "max(IZ)" )"1" "M" )"1" "M" )"1" assert )"1" "1" expand "IZ" "1" "1" assert )"1" "1" "ii!1" )"1" assert )"1" expand "IZ" "1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT nonempty?[posnat](IZ)" )"1" "1" expand "nonempty?" )"1" expand "empty?" )"1" "0" )"1" assert )"1" "IG5" "1" "IG5" )"1" "IG5" )"1" "kk" )"1" expand "member" "1" expand "IZ" "1" nil nil ))nil ))nil )"2" "IG5" )"2" "IG5" )"2" assert )"2" "2" "ii!1" )"2" expand "member" "2" expand "IZ" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "pd`qdeg+1" )"2" "2" "y!1" )"2" expand "IZ" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "poly_eq_0_le_degree" )"2" "pd`quot" "pd`qdeg" )"2" "2" "2" "1" "p(m-2)" "n(m-2)" )"1" "1" "1" "1" "n(m-2)" )"1" assert )"1" "m-2" )"1" "m-2" )"1" "m-2" )"1" "m-2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x" )"2" "x" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ii!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "constructed_sturm_sequence?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide (3 4))"2" (induct "k" )"1" (assert )"1" (skeep)"1" (assert )"1" (case "NOT i = 0" )"1" (assert ) nil nil )"2" (replaces -1)"2" (assert )"2" (lift-if)"2" "1" "1" "root_degree_pos" )"1" "1" assert )"1" "1" expand "constructed_sturm_sequence?" "1" "1" replace -3)"1" replace -4)"1" assert )"1" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" assert )nil nil )"2" "0" )nil nil )"3" "root_degree_pos" )"3" "p(0)" "n(0)" "y" )"3" assert )"3" "0" )nil nil ))nil ))nil ))nil ))nil )"2" "0" )"2" expand "poly_deriv" "2" assert )"2" "2" "n(0)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )"2" expand "max" )"2" "2" "1" "1" (assert ) nil nil ))nil )"2" "2" assert )"2" "root_degree_pos" )"2" "g" "k" "y" )"2" assert )"2" expand "constructed_sturm_sequence?" )"2" "2" replace "2" replace "2" rewrite "root_degree_mult" "1" rewrite "root_degree_deriv" )"1" assert )nil nil )"2" "0" )nil nil )"3" "root_degree_pos" )"3" "3" assert )"3" "0" )nil nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )"2" expand "poly_deriv" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "K" )"2" (flatten)"2" (assert )"2" (skeep)"2" (case "NOT i =1+K" )"1" (inst - "i" ) (("1" (assert ) nil nil ))nil )"2" (case "NOT K = i-1" )"1" (assert ) nil nil )"2" (replace -1)"2" assert )"2" "2" "i-1" )"2" assert )"2" "2" "2" expand "constructed_sturm_sequence?" "2" "2" "2" "i+1" )"2" assert )"2" "2" "pd" "poly_divide(p(i - 1), n(i - 1))(p(i), n(i))(0)" )"2" replace -1)"2" assert )"2" "root_degree_eq" )"2" "poly_divide_def" )"2" "2" assert )"2" replace "2" "1" "root_degree_division" )"1" "y" "p(i-1)" "p(i)" "pd`quot" "(1/(-c))*p(1+i)" "n(i-1)" "n(i)" "pd`qdeg" "n(1+i)" )"1" assert )"1" "1" "1" assert )"1" "1" assert )"1" case "root_degree(p(i), n(i))(y) = dd" )"1" assert )"1" expand "min" )"1" assert )"1" rewrite "root_degree_scal" )"1" assert )nil nil )"2" "css" )"2" expand "constructed_sturm_sequence?" "2" "2" "i+1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" rewrite "root_degree_scal" )"1" assert )nil nil )"2" "css" )"2" expand "constructed_sturm_sequence?" "2" "2" "1+i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" rewrite "root_degree_scal" )"1" expand "min" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil )"2" "css" )"2" expand "constructed_sturm_sequence?" "2" "2" "1+i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x" )"2" replace "2" assert )"2" "2" assert )"2" "x" )"2" assert )"2" rewrite "scal_polynomial2" )"2" rewrite "scal_polynomial2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "css" )"3" expand "constructed_sturm_sequence?" "3" expand "*" "3" "3" "1+i" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "css" )"4" expand "constructed_sturm_sequence?" "4" "4" "i-1" )"4" assert )nil nil ))nil ))nil ))nil ))nil )"5" "css" )"5" expand "constructed_sturm_sequence?" "5" "5" "i" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "css" )"2" expand "constructed_sturm_sequence?" "2" "2" "i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{m | AND AND polynomial(b, n - m)(y) /= 0 AND b(n - m) /= 0)AND AND AND m > 0) IMPLIESAND polynomial(q, n - m)(y) /= 0))))}" "reals/" )"real" polynomials "reals/" )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> real]" polynomials "reals/" )nil sequences nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )nil more_polynomial_props "reals/" )nil more_polynomial_props"reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil more_polynomial_props "reals/" )"{k: nat | k <= i AND k <= j}" nil )"[T -> real]" real_fun_ops "reals/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nzreal" nil )"odd_int" integers nil )"(total_order?[real])" nil )"posnat" sturmtarski nil )"nat" sturmtarski nil )nil min_max "reals/" )nil real_props nil )nil reals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil more_polynomial_props "reals/" )"real" reals nil )"real" sigma "reals/" )"real" polynomials "reals/" )"posint" nil )nil more_polynomial_props "reals/" )"nonneg_int" nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sturmtarski nil )nil more_polynomial_props "reals/" )nil polynomial_division "Sturm/" )"DivType" polynomial_division "Sturm/" )nil polynomial_division "Sturm/" )"[numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil polynomials "reals/" )nil defined_types nil )nil naturalnumbers nil )nil polynomials "reals/" )"odd_int" integersnil )"real" reals nil )"nat" sturmtarski nil )"bool" sets nil )"nat" sturmtarski nil )"bool" sets nil )"[posnat -> boolean]" sturmtarski nil )"nat" sturmtarski nil )max const-decl"{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}" "ints/" )"bool" sets nil )set type-eq-decl nil sets nil )nil polynomials "reals/" )nil more_polynomial_props"reals/" )"real" reals nil )nil polynomials "reals/" )"[nat -> real]" sturmtarski nil )"nzreal" real_typesnil )nil integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"posint" nil )"int" integers nil )"bool" sturmtarski nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities 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 )nil 3617013924"" (skeep)"" (case "g(k)=0" )"1" (expand "constructed_sturm_sequence?" )"1" (ground) nil nil )) nil )"2" "dd" "IF polynomial(g,k)(y)=0 THEN root_degree(p(0),n(0))(y) ELSE max(root_degree(p(0), n(0))(y) - 1, 0) ENDIF" )"2" case "FORALL (k,i:nat): i<=k AND k+1<m IMPLIES ((root_degree(p(i),n(i))(y)=dd OR root_degree(p(i+1),n(i+1))(y)=dd) AND (root_degree(p(i),n(i))(y)>=dd AND root_degree(p(i+1),n(i+1))(y)>=dd))" )"1" (assert )"1" (inst - "m-2" _)"1" (assert )"1" (lift-if)"1" (split -)"1" (flatten)"1" (lemma "root_degree_pos" )"1" (inst?)"1" (assert )"1" (hide 3)"1" expand "default_root_degree?" )"1" assert )"1" case "NOT (%1)" ) (! 2 1))"1" "1" "1" expand "constructed_sturm_sequence?" "1" "1" assert )"1" replace -4 +)"1" "root_degree_mult" )"1" "1" assert )"1" "y" )"1" assert )"1" "1" replace "1" "1" rewrite "root_degree_deriv" )"1" nil nil )"2" "0" )nil nil )"3" "root_degree_pos" )"3" "3" assert )"3" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" )"2" assert )"2" replace "2" replace "2" "2" expand "polynomial_prod" "2" expand "max" "2" expand "sigma" "2" expand "sigma" "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" "2" replace -4)"2" assert )"2" "i-1" )"2" assert )"2" "2" "i" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide 3)"2" (replace -1)"2" (expand "default_root_degree?" )"2" case "NOT (%1)" ) (! 3 1))"1" "1" assert )"1" "1" assert )"1" case "polynomial(p(0),n(0))(y)/=0" )"1" "1" assert )"1" "root_degree_pos" )"1" "1" assert )"1" "1" "1" assert )nil nil )"2" expand "constructed_sturm_sequence?" )"2" "2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "root_degree_pos" )"2" "2" assert )"2" "root_degree_pos" )"2" "p(0)" "n(0)" "y" )"2" assert )"2" "1" expand "max" "1" assert )"1" assert )"1" "1" expand "constructed_sturm_sequence?" "1" "1" assert )"1" replace "1" replace "1" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" assert )nil nil )"2" "0" )nil nil ))nil )"2" "0" )"2" expand "poly_deriv" "2" assert )"2" "2" "n(0)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "constructed_sturm_sequence?" )"2" "2" "0" )"2" assert )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" "2" "2" assert )"2" "1" "1" "i-1" )"1" (assert ) nil nil )"2" assert )nil nil ))nil ))nil )"2" "2" "i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "constructed_sturm_sequence?" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide (3 4))"2" (induct "k" )"1" (assert )"1" (skeep)"1" (assert )"1" (case "NOT i = 0" )"1" (assert ) nil nil )"2" (replaces -1)"2" (assert )"2" (lift-if)"2" (split -3)"1" "1" "root_degree_pos" )"1" "1" assert )"1" "1" expand "constructed_sturm_sequence?" "1" "1" replace -3)"1" replace -4)"1" assert )"1" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" assert )nil nil )"2" "0" )nil nil )"3" "root_degree_pos" )"3" "p(0)" "n(0)" "y" )"3" assert )"3" "0" )nil nil ))nil ))nil ))nil ))nil )"2" "0" )"2" expand "poly_deriv" "2" assert )"2" "2" "n(0)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )"2" expand "max" )"2" "2" "1" "1" (assert ) nil nil ))nil )"2" "2" assert )"2" "root_degree_pos" )"2" "g" "k" "y" )"2" assert )"2" expand "constructed_sturm_sequence?" )"2" "2" replace -7)"2" replace "2" rewrite "root_degree_mult" "1" rewrite "root_degree_deriv" )"1" assert )nil nil )"2" "0" )nil nil )"3" "root_degree_pos" )"3" "3" assert )"3" "0" )nil nil ))nil ))nil ))nil ))nil )"2" "0" )"2" assert )"2" expand "poly_deriv" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "K" )"2" (flatten)"2" (assert )"2" (skeep)"2" (case "NOT i =1+K" )"1" (inst - "i" ) (("1" (assert ) nil nil ))nil )"2" (case "NOT K = i-1" )"1" (assert ) nil nil )"2" (replace -1)"2" (assert )"2" "2" "i-1" )"2" assert )"2" "2" "2" expand "constructed_sturm_sequence?" "2" "2" "2" "i+1" )"2" assert )"2" "2" "pd" "poly_divide(p(i - 1), n(i - 1))(p(i), n(i))(0)" )"2" replace -1)"2" assert )"2" "root_degree_eq" )"2" "poly_divide_def" )"2" "2" assert )"2" replace "2" "1" "root_degree_division" )"1" "y" "p(i-1)" "p(i)" "pd`quot" "(1/(-c))*p(1+i)" "n(i-1)" "n(i)" "pd`qdeg" "n(1+i)" )"1" assert )"1" "1" "1" assert )"1" "1" assert )"1" case "root_degree(p(i), n(i))(y) = dd" )"1" assert )"1" expand "min" )"1" assert )"1" rewrite "root_degree_scal" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" nil nil )"5" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3617953557 ("" (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 )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" exponentiation nil )"[real -> real]" polynomials "reals/" )"real" reals nil )"int" integers nil ))nil ))nil 3617953558"" (skeep)"" (lemma "constructed_sturm_seq_root_degrees" )"" (inst?)"" (assert )"" (expand "default_root_deg" ) (("" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )nil sturmtarskinil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"int" integers nil )"nat" sturmtarski nil )nil integers nil )"bool" reals nil )nil integers 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 3618047247"" case "FORALL (g: [nat -> real], k: nat, m: posnat, n: [nat -> nat], AND dd<m IMPLIES") "1" (skeep)"1" (inst?)"1" (inst - "m-1" )"1" (assert )"1" (skeep)"1" (inst - "i" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "dd" )"1" (skeep)"1" (skeep)"1" (case "NOT i = 0" )"1" (assert ) nil nil )"2" (replace -1)"2" (assert )"2" (expand "default_root_deg" 1)"2" (expand "max" )"2" (lift-if) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (skeep)"2" (case "NOT i = j+1" )"1" (inst - "g" "k" "m" "n" "p" "y" )"1" (assert )"1" (inst - "i" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide -5)"2" (replace -1)"2" (assert )"2" (case "j = 0" )"1" (replace -1)"1" (assert )"1" (expand "default_root_deg" 1)"1" "1" expand "max" )"1" "1" "1" expand "constructed_sturm_sequence?" "1" "1" replace -4)"1" replace -5)"1" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" "root_degree_pos" )"1" "1" assert )nil nil ))nil ))nil )"2" "0" )nil nil )"3" "root_degree_pos" )"3" "p(0)" "n(0)" "y" )"3" assert )"3" "0" )nil nil ))nil ))nil ))nil ))nil )"2" expand "poly_deriv" "2" "0" )"2" assert )"2" "2" "n(0)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "constructed_sturm_sequence?" "2" "2" "0" )"2" "1" )"2" assert )"2" "2" replace -2 2)"2" replace -3 2)"2" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" assert )nil nil )"2" "root_degree_pos" )"2" "p(0)" "n(0)" "y" )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "poly_deriv" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (copy -3)"2" (label "igz" -1)"2" case "NOT (p(1+j)(n(1+j))/=0 AND p(j)(n(j))/=0 AND p(j-1)(n(j-1))/=0)" )"1" expand "constructed_sturm_sequence?" "1" "1" "1+j" )"1" "j" )"1" "j-1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "constructed_sturm_sequence?" "2" "2" "2" "igz" )"2" "j+1" )"2" assert )"2" "2" "pd" "poly_divide(p(j - 1), n(j - 1))(p(j), n(j))(0)" )"2" replace -1)"2" case "NOT polynomial((-1/c)*p(1 + j), n(1 + j)) = polynomial(pd`rem, pd`rdeg)" )"1" "1" rewrite "scal_polynomial2" )"1" "1" "x!1" )"1" rewrite "scal_polynomial2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_divide_def" )"2" "2" assert )"2" replace "2" replace "2" "root_degree_division" )"2" "y" "p(j - 1)" "p(j)" "pd`quot" "(-1/c)*p(1+j)" "n(j-1)" "n(j)" "pd`qdeg" "n(1+j)" )"2" assert )"2" replace "2" "1" "1" "1" assert )"1" "1" "j-1" )"1" "j" )"1" assert )"1" expand "min" )"1" "1" "1" "1" "1" rewrite "root_degree_scal" )"1" assert )nil nil ))nil ))nil )"2" "2" rewrite "root_degree_scal" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "*" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nat" sturmtarski nil )nil polynomial_division "Sturm/" )"DivType" polynomial_division "Sturm/" )"nzreal" nil )"[T -> real]" real_fun_ops "reals/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )nil polynomials "reals/" )"odd_int" integers nil )"nzreal" real_typesnil )nil more_polynomial_props"reals/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil more_polynomial_props "reals/" )"{k: nat | k <= i AND k <= j}" nil )nil polynomial_division "Sturm/" )"real" reals nil )nil real_props nil )nil reals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil more_polynomial_props "reals/" )"(strict_total_order?[real])" real_props nil )nil more_polynomial_props "reals/" )nil naturalnumbers nil )"int" integers nil )"nonneg_int" nil )nil more_polynomial_props "reals/" )"odd_int" integers nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" 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 naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sturmtarski nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil sequences nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"[real -> real]" polynomials "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"real" polynomials "reals/" )"{m | AND AND polynomial(b, n - m)(y) /= 0 AND b(n - m) /= 0)AND AND AND m > 0) IMPLIESAND polynomial(q, n - m)(y) /= 0))))}" "reals/" )"nat" sturmtarski nil ))nil 3617696203"" (skeep)"" (label "css" -1)"" (label "igz" -2)"" case "FORALL (xy,xr:real): x<=xy AND xy<=xr AND xr<=y IMPLIES sign_ext(polynomial(g,k)(xy)) = sign_ext(polynomial(g,k)(xr))" )"1" (inst-cp - "x" "z" )"1" (inst - "z" "y" )"1" (assert )"1" (case "x<=z AND z<=y" )"1" (flatten)"1" (assert )"1" (hide (-1 -2))"1" (case "m>=2" )"1" (inst-cp - "0" )"1" (inst - "1" )"1" assert )"1" expand "only_root_between?" )"1" "1" "1" assert )"1" "x" )"1" "y" )"1" assert )"1" "x" )"1" "y" )"1" assert )"1" "1" expand "number_sign_changes" )"1" expand "number_sign_changes" )"1" assert )"1" "1" assert )"1" "1" assert )"1" "1" assert )"1" case "sign_ext(polynomial(poly_deriv(p(0)), n(0)-1)(x)) = ") "1" case "sign_ext(polynomial(p(0),n(0))(x)) = -sign_ext(polynomial(g,k)(x))*sign_ext(polynomial(p(1),n(1))(x))" )"1" "1" assert )"1" "root_degree_pos" )"1" "root_degree_pos" )"1" "p(0)" "n(0)" "z" )"1" assert )"1" "g" "k" "z" )"1" assert )"1" case "NOT (p(0)(n(0))/=0 AND g(k)/=0)" )"1" expand "constructed_sturm_sequence?" )"1" "1" "0" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "dd" "root_degree(p(0),n(0))(z)" )"2" replace "2" case "root_degree(p(1),n(1))(z) = dd-1" )"1" assert )"1" "even_or_odd" )"1" "dd" )"1" "dd-1" )"1" "odd_iff_even_succ" )"1" "dd-1" )"1" assert )"1" "root_degree_even" )"1" "p(0)" "n(0)" "x" "y" "z" )"1" assert )"1" "p(1)" "n(1)" "x" "y" "z" )"1" assert )"1" case "p(1)(n(1))=0" )"1" expand "constructed_sturm_sequence?" )"1" "1" "1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "1" expand "sign_ext" )"1" "1" assert )"1" "1" assert )"1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" )"2" "2" assert )"2" "2" assert )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "sign_ext" )"3" "3" assert )"3" "3" assert )"3" "3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" expand "sign_ext" )"4" "4" assert )"4" "4" assert )"4" "4" assert )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" expand "sign_ext" )"5" "5" assert )"5" "5" assert )"5" "5" assert )"5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" expand "sign_ext" )"6" "6" assert )"6" "6" assert )"6" "6" assert )"6" 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 "constructed_sturm_sequence?" "2" "2" replace "2" replace "2" assert )"2" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" assert )nil nil ))nil )"2" expand "poly_deriv" "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" "2" "2" expand "constructed_sturm_sequence?" "2" "2" replace "2" replace "2" assert )"2" rewrite "polynomial_prod_def" "2" rewrite "sign_ext_mult" )"2" expand "sign_ext" "2" expand "sign_ext" "2" "2" assert )"2" "2" replace "2" replace "2" rewrite "polynomial_prod_def" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "polynomial(poly_deriv(p(0)), n(0) - 1)(x)=0" )"1" "1" expand "constructed_sturm_sequence?" "1" "1" assert )"1" replace "1" replace "1" rewrite "polynomial_prod_def" "1" rewrite "polynomial_prod_def" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" "2" "2" assert )"2" "2" assert )"2" "2" assert )"2" "1" "poly_decreasing" )"1" "p(0)" "n(0)" "x" "z" )"1" assert )"1" case "n(0)>0" )"1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "poly_deriv(p(0))" "0" "n(0)-1" "x" "c!1" )"1" assert )"1" "1" "igz" )"1" "1" "igz" )"1" "cc!1" )"1" assert )"1" "1" "css" )"1" expand "constructed_sturm_sequence?" "1" "1" replace "1" replace "1" rewrite "polynomial_prod_def" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "css" )"2" expand "constructed_sturm_sequence?" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_increasing" )"2" "p(0)" "n(0)" "x" "z" )"2" assert )"2" case "n(0)>0" )"1" assert )"1" "1" "poly_intermediate_value_dec" )"1" "poly_deriv(p(0))" "0" "n(0)-1" "x" "c" )"1" assert )"1" "1" "igz" )"1" "1" "igz" )"1" "cc" )"1" assert )"1" "1" "css" )"1" expand "constructed_sturm_sequence?" "1" "1" replace "1" replace "1" rewrite "polynomial_prod_def" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "constructed_sturm_sequence?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "constructed_sturm_sequence?" )"3" "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 ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (expand "constructed_sturm_sequence?" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst - "0" )"2" (expand "only_root_between?" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" case "FORALL (rr:real): x<=rr AND rr<=y IMPLIES polynomial(g,k)(rr)/=0" )"1" (inst-cp - "xy" )"1" (inst-cp - "xr" )"1" (assert )"1" (flatten)"1" (expand "sign_ext" 3)"1" (lift-if)"1" (assert )"1" (lift-if)"1" assert )"1" "1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "g" "0" "k" "xy" "xr" )"1" assert )"1" "1" "cc!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "g" "0" "k" "xy" "xr" )"2" assert )"2" "2" "cc" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (inst - "1" )"1" (expand "only_root_between?" )"1" (flatten)"1" (assert )"1" (inst - "rr" )"1" (assert )"1" (flatten)"1" "css" )"1" expand "constructed_sturm_sequence?" "1" "1" replace -4 3)"1" replace -5 3)"1" rewrite "polynomial_prod_def" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "constructed_sturm_sequence?" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[real -> real]" polynomials "reals/" )nil sequences nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" sturmtarski nil )"bool" more_polynomial_props"reals/" )"real" reals nil )"real" polynomials "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sign "reals/" )nil polynomials "reals/" )nil more_polynomial_props "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"boolean" notequal nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" sturmtarski nil )nil more_polynomial_props "reals/" )"nonneg_int" nil )nil more_polynomial_props "reals/" )nil naturalnumbers nil )"odd_int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )nil more_polynomial_props "reals/" )nil naturalnumbers nil )"{m | AND AND polynomial(b, n - m)(y) /= 0 AND b(n - m) /= 0)AND AND AND m > 0) IMPLIESAND polynomial(q, n - m)(y) /= 0))))}" "reals/" )"real" exponentiation nil )"real" reals nil )nil polynomials "reals/" )nil polynomials "reals/" )nil polynomials "reals/" )nil polynomials "reals/" )"NSC" number_sign_changes "Sturm/" )"(total_order?[real])" nil )"bool" reals nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil ))nil )nil 3617696022"" (skeep)"" (label "igz" -2)"" case "FORALL (xy,xr:real): x<=xy AND xy<=xr AND xr<=y IMPLIES sign_ext(polynomial(g,k)(xy)) = sign_ext(polynomial(g,k)(xr))" )"1" (inst-cp - "x" "z" )"1" (inst - "z" "y" )"1" (assert )"1" (case "x<=z AND z<=y" )"1" (flatten)"1" (assert )"1" (hide (-1 -2))"1" (case "m>=2" )"1" (inst-cp - "0" )"1" (inst - "1" )"1" (assert )"1" expand "only_root_between?" )"1" "1" "1" assert )"1" "x" )"1" "y" )"1" assert )"1" "x" )"1" "y" )"1" assert )"1" "1" expand "number_sign_changes" )"1" expand "number_sign_changes" )"1" assert )"1" "1" assert )"1" "1" assert )"1" "1" assert )"1" case "sign_ext(polynomial(poly_deriv(p(0)), n(0)-1)(x)) = ") "1" case "sign_ext(polynomial(p(0),n(0))(x)) = -sign_ext(polynomial(g,k)(x))*sign_ext(polynomial(p(1),n(1))(x))" )"1" "1" assert )"1" "root_degree_pos" )"1" "root_degree_pos" )"1" "p(0)" "n(0)" "z" )"1" assert )"1" "g" "k" "z" )"1" assert )"1" case "NOT (p(0)(n(0))/=0 AND g(k)/=0)" )"1" expand "constructed_sturm_sequence?" )"1" "1" "0" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "dd" "root_degree(p(0),n(0))(z)" )"2" replace "2" case "root_degree(p(1),n(1))(z) = dd-1" )"1" assert )"1" "even_or_odd" )"1" "dd" )"1" "dd-1" )"1" "odd_iff_even_succ" )"1" "dd-1" )"1" assert )"1" "root_degree_even" )"1" "p(0)" "n(0)" "x" "y" "z" )"1" assert )"1" "p(1)" "n(1)" "x" "y" "z" )"1" assert )"1" case "p(1)(n(1))=0" )"1" expand "constructed_sturm_sequence?" )"1" "1" "1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "1" expand "sign_ext" )"1" "1" assert )"1" "1" assert )"1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" )"2" "2" assert )"2" "2" assert )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "sign_ext" )"3" "3" assert )"3" "3" assert )"3" "3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" expand "sign_ext" )"4" "4" assert )"4" "4" assert )"4" "4" assert )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" expand "sign_ext" )"5" "5" assert )"5" "5" assert )"5" "5" assert )"5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" expand "sign_ext" )"6" "6" assert )"6" "6" assert )"6" "6" assert )"6" 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 "constructed_sturm_sequence?" "2" "2" replace "2" replace "2" assert )"2" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" assert )nil nil ))nil )"2" expand "poly_deriv" "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" "2" "2" expand "constructed_sturm_sequence?" "2" "2" replace "2" replace "2" assert )"2" rewrite "polynomial_prod_def" "2" rewrite "sign_ext_mult" )"2" expand "sign_ext" "2" expand "sign_ext" "2" "2" assert )"2" "2" replace "2" replace "2" rewrite "polynomial_prod_def" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "polynomial(poly_deriv(p(0)), n(0) - 1)(x)=0" )"1" "1" expand "constructed_sturm_sequence?" "1" "1" assert )"1" replace "1" replace "1" rewrite "polynomial_prod_def" "1" rewrite "polynomial_prod_def" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" "2" "2" assert )"2" "2" assert )"2" "2" assert )"2" "1" "poly_decreasing" )"1" "p(0)" "n(0)" "x" "z" )"1" assert )"1" case "n(0)>0" )"1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "poly_deriv(p(0))" "0" "n(0)-1" "x" "c!1" )"1" assert )"1" "1" "igz" )"1" "1" "igz" )"1" "cc!1" )"1" assert )"1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"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 )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil )nil nil )nil 3617644038"" (skeep)"" case "FORALL (xy,xr:real): x<=xy AND xy<=xr AND xr<=y IMPLIES sign_ext(polynomial(g,k)(xy)) = sign_ext(polynomial(g,k)(xr))" )"1" (inst-cp - "x" "z" )"1" (inst - "z" "y" )"1" (assert )"1" (case "x<=z AND z<=y" )"1" (flatten)"1" (assert )"1" (hide (-1 -2))"1" (case "m>=2" )"1" (inst-cp - "0" )"1" (inst - "1" )"1" (assert )"1" (expand "only_root_between?" )"1" "1" "1" assert )"1" "x" )"1" "y" )"1" assert )"1" "x" )"1" "y" )"1" assert )"1" "1" expand "number_sign_changes" )"1" expand "number_sign_changes" )"1" assert )"1" "1" assert )"1" "1" assert )"1" "1" assert )"1" case "sign_ext(polynomial(poly_deriv(p(0)), n(0)-1)(x)) = ") "1" case "sign_ext(polynomial(p(0),n(0))(x)) = -sign_ext(polynomial(g,k)(x))*sign_ext(polynomial(p(1),n(1))(x))" )"1" "1" assert )"1" "root_degree_pos" )"1" "root_degree_pos" )"1" "p(0)" "n(0)" "z" )"1" assert )"1" "g" "k" "z" )"1" assert )"1" case "NOT (p(0)(n(0))/=0 AND g(k)/=0)" )"1" expand "constructed_sturm_sequence?" )"1" "1" "0" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "dd" "root_degree(p(0),n(0))(z)" )"2" replace "2" case "root_degree(p(1),n(1))(z) = dd-1" )"1" assert )"1" "even_or_odd" )"1" "dd" )"1" "dd-1" )"1" "odd_iff_even_succ" )"1" "dd-1" )"1" assert )"1" "root_degree_even" )"1" "p(0)" "n(0)" "x" "y" "z" )"1" assert )"1" "p(1)" "n(1)" "x" "y" "z" )"1" assert )"1" case "p(1)(n(1))=0" )"1" expand "constructed_sturm_sequence?" )"1" "1" "1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "1" expand "sign_ext" )"1" "1" assert )"1" "1" assert )"1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" )"2" "2" assert )"2" "2" assert )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "sign_ext" )"3" "3" assert )"3" "3" assert )"3" "3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" expand "sign_ext" )"4" "4" assert )"4" "4" assert )"4" "4" assert )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" expand "sign_ext" )"5" "5" assert )"5" "5" assert )"5" "5" assert )"5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" expand "sign_ext" )"6" "6" assert )"6" "6" assert )"6" "6" assert )"6" 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 "constructed_sturm_sequence?" "2" "2" replace "2" replace "2" assert )"2" rewrite "root_degree_mult" )"1" rewrite "root_degree_deriv" )"1" assert )nil nil ))nil )"2" expand "poly_deriv" "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" "2" "2" expand "constructed_sturm_sequence?" "2" "2" replace "2" replace "2" assert )"2" rewrite "polynomial_prod_def" "2" rewrite "sign_ext_mult" )"2" expand "sign_ext" "2" expand "sign_ext" "2" "2" assert )"2" "2" replace "2" replace "2" rewrite "polynomial_prod_def" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "polynomial(poly_deriv(p(0)), n(0) - 1)(x)=0" )"1" "1" expand "constructed_sturm_sequence?" "1" "1" assert )"1" replace "1" replace "1" rewrite "polynomial_prod_def" "1" rewrite "polynomial_prod_def" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" "2" "2" assert )"2" "2" assert )"2" "2" assert )"2" "1" "poly_decreasing" )"1" "p(0)" "n(0)" "x" "z" )"1" assert )"1" case "n(0)>0" )"1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "poly_deriv(p(0))" "0" "n(0)-1" "x" "c!1" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"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 )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )nil nil )nil 3617643010"" (skeep)"" case "FORALL (xy,xr:real): x<=xy AND xy<=xr AND xr<=y IMPLIES sign_ext(polynomial(g,k)(xy)) = sign_ext(polynomial(g,k)(xr))" )"1" (inst-cp - "x" "z" )"1" (inst - "z" "y" )"1" (assert )"1" (case "x<=z AND z<=y" )"1" (flatten)"1" (assert )"1" (hide (-1 -2))"1" (case "m>=2" )"1" (inst-cp - "0" )"1" (inst - "1" )"1" (assert )"1" (expand "only_root_between?" )"1" "1" "1" assert )"1" "x" )"1" "y" )"1" assert )"1" "x" )"1" "y" )"1" assert )"1" "1" expand "number_sign_changes" )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.705Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
