(sturmsquarefreenil 3583755671 ("" (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 )"real" exponentiation nil )"[real -> real]" polynomials "reals/" )"{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 )"real" reals nil )"(total_order?[real])" nil )"boolean" notequal nil )"int" integers nil ))nil ))nil 3583755671 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" polynomials "reals/" )"real" exponentiation nil )"[real -> real]" polynomials "reals/" )"boolean" notequal nil )"int" integers nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"real" reals nil ))nil ))nil 3588942625"" (skeep)"" (expand "sturm_sequence?" )"" (assert )"" (split +)"1" (skeep) (("1" (assert ) nil nil )) nil )"2" (skeep)"2" (case "i = 1" )"1" (replaces -1)"1" (replace -5)"1" (expand "poly_deriv" -2)"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" (skeep) (("3" (assert ) nil nil )) nil )"4" (skeep)"4" (assert )"4" (replaces -1)"4" (replace -2) (("4" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sturmsquarefree nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props 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 )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"real" polynomials "reals/" )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" "reals/" )"[real -> real]" polynomials "reals/" )"real" sigma "reals/" )"real" exponentiation nil )"real" exponentiation nil )nil min_max "reals/" )"int" integers nil ))nil 3584191381"" (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 "sturm_sequence?" )"2" (flatten)"2" (inst - "x" "i" )"2" (assert )"2" (expand "sign_ext" -7)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" assert )"2" (ground) 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 )"[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" sturmsquarefree nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"nat" sturmsquarefree nil )"upto(m)" sturmsquarefree nil )"nat" sturmsquarefree nil )"posint" nil )"(total_order?[real])" nil )"int" integers nil )nil naturalnumbers nil )"nonneg_int" nil )"nat" sturmsquarefree nil )"bool" sturmsquarefree nil )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" "reals/" )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil ))nil 3588410248"" (skeep)"" (skeep)"" case "NOT FORALL (xyzp:real): polynomial(p(m),n(m))(xyzp) = 0" )"1" (skeep)"1" (expand "sturm_sequence?" )"1" (flatten)"1" (inst -6 "xyz" "xyzp" )"1" (expand "sign_ext" -6)"1" (assert )"1" (assert )"1" (lift-if) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "polynomial_eq_coeff" )"2" (inst - "p(m)" "LAMBDA (i:nat): 0" "n(m)" )"2" (assert )"2" (flatten)"2" (hide -2)"2" (split -)"1" (inst - "n(m)" )"1" (expand "sturm_sequence?" )"1" (flatten)"1" (inst -5 "m" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (decompose-equality 1)"2" (inst - "x!1" )"2" (assert )"2" (replaces -1)"2" (expand "polynomial" +)"2" rewrite "sigma_restrict_eq_0" )"2" "2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil polynomials "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sigma "reals/" )"real" reals nil )"[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil naturalnumbers nil )"bool" reals nil )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" "reals/" )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" sturmsquarefree 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 )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"[real -> real]" polynomials "reals/" ))nil 3587370024"" (skeep)"" case "NOT (polynomial(p(0), n(0))(x) /= 0 AND ") "1" (hide 2)"1" (inst-cp - "x" )"1" (inst - "y" ) (("1" (ground) nil nil )) nil )) nil ))nil )"2" (flatten)"2" (assert )"2" (inst-cp - "b" )"2" (assert )"2" (flatten)"2" case "polynomial(poly_deriv(p(0)),max(n(0)-1,0))(b) = 0" )"1" (expand "sturm_sequence?" )"1" (flatten)"1" (inst -8 "b" )"1" (assert )"1" (expand "sign_ext" -8)"1" (assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "poly_continuous" )"2" "poly_deriv(p(0))" "max(n(0)-1,0)" "b" "abs(polynomial(poly_deriv(p(0)),n(0)-1)(b))" )"1" (skeep -)"1" case "EXISTS (deltiv:posreal): FORALL (x1:real): abs(b-x1)<deltiv IMPLIES (abs(b-x1)<delta AND x < x1 AND x1 < y)" )"1" case "sign_ext(polynomial(p(0), n(0))(x)) = max (n(0)-1,0))(b))AND max (n(0)-1,0))(b))") "1" (hide (-2 -3))"1" "1" expand "sturm_sequence?" )"1" "1" "b" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 6)"2" case "polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)>0" )"1" "1" case "FORALL (x1,x2:real): abs(x1-b)<deltiv AND abs(x2-b)<deltiv AND x1<x2 IMPLIES polynomial(p(0),n(0))(x1) < polynomial(p(0),n(0))(x2)" )"1" "b-deltiv/2" "b" )"1" "b" "b+deltiv/2" )"1" "hyplem" -1)"1" "hyplem" )"1" assert )"1" "1" expand "sign_ext" )"1" "1" assert )"1" "1" nil nil )"2" assert )"2" "2" "1" replace "1" assert )"1" "poly_intermediate_value_dec" )"1" "p(0)" "0" "n(0)" "x" "b-deltiv/2" )"1" assert )"1" "1" "1" "cc" )"1" "cc" )"1" "cc" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "b-deltiv/2" )"2" "1" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" )"2" "2" assert )"2" "1" assert )"1" "1" "1" replace "1" assert )"1" "poly_intermediate_value_dec" )"1" "p(0)" "0" "n(0)" "b+deltiv/2" "y" )"1" assert )"1" "1" "1" "cc" )"1" "cc" )"1" "cc" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "b+deltiv/2" )"2" "1" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "poly_strictly_increasing" )"2" "p(0)" "n(0)" "x1" "x2" )"2" assert )"2" case "n(0)=0" )"1" "1" expand "polynomial" )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "max" )"2" assert )"2" "c" )"2" assert )"2" "1" "c" )"1" "1" assert )"1" expand "abs" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)<0" )"1" "1" "1" case "FORALL (x1,x2:real): abs(x1-b)<deltiv AND abs(x2-b)<deltiv AND x1<x2 IMPLIES polynomial(p(0),n(0))(x1) > polynomial(p(0),n(0))(x2)" )"1" "b-deltiv/2" "b" )"1" "b" "b+deltiv/2" )"1" "hyplem" -1)"1" "hyplem" )"1" assert )"1" "1" expand "sign_ext" )"1" "1" assert )"1" "1" replace "1" assert )"1" "poly_intermediate_value_inc" )"1" "p(0)" "0" "n(0)" "x" "b-deltiv/2" )"1" assert )"1" "1" "1" "cc" )"1" "cc" )"1" "cc" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "b-deltiv/2" )"2" "1" assert )"1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"3" assert )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" )"2" "2" assert )"2" "1" nil nil )"2" assert )"2" "2" "1" replace "1" assert )"1" "poly_intermediate_value_inc" )"1" "p(0)" "0" "n(0)" "b+deltiv/2" "y" )"1" assert )"1" "1" "1" "cc" )"1" "cc" )"1" "cc" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "b+deltiv/2" )"2" "1" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "poly_strictly_decreasing" )"2" "p(0)" "n(0)" "x1" "x2" )"2" assert )"2" case "n(0)=0" )"1" "1" expand "polynomial" )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "max" )"2" assert )"2" "c" )"2" assert )"2" "1" "c" )"1" "1" assert )"1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" "2" assert )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 ))nil )"3" (assert ) nil nil ))nil )"2" (inst + "min(delta,min(b-x,y-b))" )"1" (hide-all-but (-2 -3 1))"1" (grind) nil nil )) nil )"2" (hide-all-but (-2 -3 1))"2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (expand "abs" 1)"2" (lift-if)"2" (assert )"2" (split 1)"1" (propax) nil nil )"2" "2" expand "sturm_sequence?" )"2" "2" "b" )"2" assert )"2" case "n(0) = 0" )"1" "1" expand "polynomial" "1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "max" )"2" expand "sign_ext" -7)"2" "2" "2" "2" "2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (case "n(0) = 0" )"1" (replace -1)"1" (assert )"1" expand "polynomial" (-4 3))"1" expand "sigma" )"1" expand "sigma" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[real -> real]" polynomials "reals/" )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"[T, T -> boolean]" equalities nil )"real" polynomials "reals/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"odd_int" integers nil )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" "reals/" )"bool" sturmsquarefree nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[nat -> nat]" sturmsquarefree nil )"bool" reals nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[nat -> [nat -> real]]" sturmsquarefree nil )"real" sturmsquarefree nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil polynomials "reals/" )nil polynomials "reals/" )"real" sigma "reals/" )"real" reals nil )nil min_max "reals/" )nil polynomials "reals/" )"nzreal" nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil abs_rews "ints/" )"{y: posreal | y >= x}" nil )nil polynomials "reals/" )"nzreal" real_typesnil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" sturmsquarefree nil )"real" sturmsquarefree nil )"posreal" sturmsquarefree nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )"odd_int" integersnil )nil min_max "reals/" )nil polynomials "reals/" ))nil 3587229961"" (skeep)"" (name "f" "polynomial(p(0),n(0))" )"" case "FORALL (j:nat): j<=m IMPLIES number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), j)`num = LAMBDA (i): polynomial(p(i), n(i))(y), j)`num AND sign_ext(number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), j)`lastnz) = sign_ext(number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(y), j)`lastnz)") "1" (inst - "m" )"1" (expand "sturm_sig" ) (("1" (assert ) nil nil )) nil ))nil )"2" (induct "j" )"1" (assert )"1" (split)"1" (expand "number_sign_changes" )"1" (propax) nil nil )) nil )"2" (expand "number_sign_changes" )"2" (replace -1)"2" (lemma "poly_intermediate_value_inc" )"2" (inst - "p(0)" "0" "n(0)" "x" "y" )"2" (assert )"2" (lemma "poly_intermediate_value_dec" )"2" (inst - "p(0)" "0" "n(0)" "x" "y" )"2" (assert )"2" "1" "1" "cc" "0" )"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "1" "1" "cc" "0" )"1" (assert ) nil nil ))nil ))nil )"2" replace -1)"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "1" "1" "cc" "0" )"1" (assert ) nil nil ))nil ))nil )"2" expand "sign_ext" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "jj" )"2" (hide 2)"2" (assert )"2" (flatten)"2" (assert )"2" (flatten)"2" "G" "LAMBDA (xx:real): LAMBDA (i): polynomial(p(i),n(i))(xx)" )"2" (copy -1)"2" (decompose-equality -1)"2" (inst-cp - "x" )"2" "y" )"2" "2" "2" case "NOT sign_ext(G(x)(1+jj)) = sign_ext(G(y)(1+jj))" )"1" "1" expand "G" 1)"1" "x" "1+jj" )"1" "y" "1+jj" )"1" assert )"1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"1" assert )"1" "1" "cc" "1+jj" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"2" assert )"2" "2" "cc" "1+jj" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "number_sign_changes" "2" assert )"2" "2" "2" "2" assert )"2" "1" "y" "1+jj" )"1" assert )"1" expand "G" "1" assert )nil nil ))nil ))nil ))nil )"2" expand "sign_ext" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "x" "1+jj" )"3" assert )"3" expand "G" "3" assert )nil nil ))nil ))nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" expand "sign_ext" "6" assert )"6" "6" assert )nil nil ))nil ))nil ))nil )"7" "7" assert )nil nil ))nil )"8" "8" "8" assert )"8" "1" nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" "9" "9" "9" assert )nil nil ))nil ))nil ))nil )"10" "10" assert )nil nil ))nil )"11" "11" "11" "11" assert )nil nil ))nil ))nil ))nil )"12" "12" "12" "12" 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 )"[real -> real]" polynomials "reals/" )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil defined_types nil )nil naturalnumbers nil )nil polynomials "reals/" )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(total_order?[real])" nil )nil polynomials "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> [nat -> real]]" sturmsquarefree nil )"real" reals nil )"int" integers nil )"posint" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" sturmsquarefree nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_sign_changes nil )"NSC" number_sign_changes nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" "reals/" ))nil 3587808579"" case " FORALL (b: real, dd,j, m: nat, n: [nat -> nat], AND AND x < b AND b < yAND (FORALL (c: real, i: nat):AND AND c <= y AND polynomial(p(i), n(i))(c) = 0AND (FORALL (c:real): x<=c AND c<=y AND polynomial(p(0),n(0))(c)=0 IMPLIESAND j <= m AND polynomial(p(j), n(j))(b) /= 0 AND sturm_sequence?(p, n, m)LET nsc =LAMBDA (xyz: real, pj: nat):LAMBDA AND IF polynomial(p(0), n(0))(b) = 0 THEN 1 ELSE 0 ENDIF)") "1" (skeep)"1" (inst - "b" "j" "j" "m" "n" "p" "x" "y" )"1" (assert )"1" (replace -5)"1" (replace -6) (("1" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "dd" )"1" (assert ) nil nil )"2" (skeep)"2" (assert )"2" (case "NOT j = 0" )"1" (assert ) nil nil )"2" (hide -2)"2" (replaces -1)"2" (expand "number_sign_changes" )"2" (expand "sign_ext" 2)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" assert )"2" "1" "poly_intermediate_value_inc" )"1" "p(0)" "0" "n(0)" "x" "y" )"1" assert )"1" "1" "cc" "0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(0)" "0" "n(0)" "x" "y" )"2" assert )"2" "2" "cc" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" "poly_intermediate_value_dec" )"3" "p(0)" "0" "n(0)" "x" "y" )"3" assert )"3" "3" "cc" "0" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" "x" "0" )"4" (assert ) nil nil ))nil )"5" "x" "0" )"5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "jj" )"3" (flatten)"3" (skeep)"3" (assert )"3" (case "NOT j = 1+jj" )"1" (inst - "b" "j" "m" "n" "p" "x" "y" )"1" (assert )"1" (replace -6)"1" (replace -7) (("1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (replaces -1)"2" (assert )"2" (inst-cp - "x" "jj" )"2" (assert )"2" (inst-cp - "y" "jj" )"2" (assert )"2" "x" "1+jj" )"2" assert )"2" "y" "1+jj" )"2" assert )"2" case "polynomial(p(jj),n(jj))(b)/=0" )"1" "1" "b" "jj" "m" "n" "p" "x" "y" )"1" assert )"1" replace -6)"1" replace -7)"1" "1" "1" assert )"1" expand "number_sign_changes" "1" assert )"1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"1" assert )"1" "1" "cc" "1+jj" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"2" assert )"2" "2" "cc" "1+jj" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "SQUAB" "%1" )"2" replace -1)"2" "SQUABname" "2" "SQUABname" )"2" expand "number_sign_changes" "2" expand "sign_ext" "2" assert )"2" "2" "2" "2" assert )"2" "1" expand "sign_ext" )"1" "1" "1" "poly_intermediate_value_dec" )"1" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"1" assert )"1" "1" "cc" "1+jj" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "sign_ext" )"2" "2" assert )"2" "2" "poly_intermediate_value_inc" )"2" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"2" assert )"2" "2" "cc" "1+jj" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" assert )nil nil ))nil ))nil )"4" expand "sign_ext" )"4" "4" assert )"4" "4" "poly_intermediate_value_inc" )"4" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"4" assert )"4" "4" "cc" "1+jj" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" expand "sign_ext" )"5" "5" assert )"5" "5" "poly_intermediate_value_dec" )"5" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"5" assert )"5" "5" "cc" "1+jj" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" "6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "hyplem" -2)"2" "hyplem" )"2" "2" expand "sturm_sequence?" "2" "2" "2" "b" "jj" )"2" assert )"2" case "jj = 0" )"1" "1" "1" assert )"1" "1" expand "number_sign_changes" "1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "p(1)" "0" "n(1)" "x" "y" )"1" assert )"1" "1" "cc" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(1)" "0" "n(1)" "x" "y" )"2" assert )"2" "2" "cc" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "sign_ext(polynomial(p(0),n(0))(x))/=sign_ext(polynomial(p(0),n(0))(y))" )"1" "1" expand "number_sign_changes" "1" expand "number_sign_changes" "1" "1" "1" "1" assert )"1" "1" expand "sign_ext" )"1" "1" "1" "1" assert )"1" "1" "poly_intermediate_value_dec" )"1" "p(1)" "0" "n(1)" "x" "y" )"1" assert )"1" "1" "cc" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_inc" )"2" "p(1)" "0" "n(1)" "x" "y" )"2" assert )"2" "2" "cc" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sturm_seq_first_signs_eq" )"2" "b" "m" "n" "p" "x" "y" )"2" assert )"2" "1" "1" expand "sign_ext" )"1" "1" "1" "1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "p(1)" "0" "n(1)" "x" "b" )"1" assert )"1" "1" "cc" "1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(1)" "0" "n(1)" "x" "b" )"2" assert )"2" "2" "cc" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "c" "0" )"2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sign_ext" "2" "2" "2" "2" assert )"2" "1" "square_free_max" )"1" case "n(0) = 0" )"1" "1" expand "polynomial" )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "p(0)" "min(y-b,b-x)" "b" "0" "n(0)" )"1" assert )"1" "1" "1" expand "sturm_sequence?" "1" "1" "1" "b" )"1" assert )"1" expand "max" "1" expand "sign_ext" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "x!1 = b" )"1" assert )nil nil )"2" case "x!1 < b" )"1" "poly_intermediate_value_inc" )"1" "p(0)" "0" "n(0)" "x" "x!1" )"1" assert )"1" "1" "cc" "0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(0)" "0" "n(0)" "x!1" "y" )"2" assert )"2" "2" "cc" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )"3" expand "min" "3" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "square_free_min" )"2" "p(0)" "min(y-b,b-x)" "b" "0" "n(0)" )"1" assert )"1" "1" "1" expand "sturm_sequence?" "1" "1" "1" "b" )"1" assert )"1" case "n(0) = 0" )"1" "1" expand "polynomial" )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "max" "2" assert )"2" expand "sign_ext" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "x!1 = b" )"1" assert )nil nil )"2" case "x!1 < b" )"1" "poly_intermediate_value_dec" )"1" "p(0)" "0" "n(0)" "x" "x!1" )"1" assert )"1" "1" "cc" "0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_inc" )"2" "p(0)" "0" "n(0)" "x!1" "y" )"2" assert )"2" "2" "cc" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "n(0) = 0" )"1" "1" expand "polynomial" "1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"3" expand "min" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "polynomial(p(jj - 1), n(jj - 1))(b) /= 0" )"1" case "sign_ext(polynomial(p(jj - 1), n(jj - 1))(b))=sign_ext(polynomial(p(jj - 1), n(jj - 1))(x)) AND sign_ext(polynomial(p(jj - 1), n(jj - 1))(b))=sign_ext(polynomial(p(jj - 1), n(jj - 1))(y))" )"1" "1" case "sign_ext(polynomial(p(1 + jj), n(1 + jj))(b))=sign_ext(polynomial(p(1 + jj), n(1 + jj))(x)) AND sign_ext(polynomial(p(1 + jj), n(1 + jj))(b))=sign_ext(polynomial(p(1 + jj), n(1 + jj))(y))" )"1" "1" assert )"1" "1" expand "number_sign_changes" "1" "1" assert )nil nil ))nil ))nil )"2" assert )"2" "SQUAB" "%1" )"2" "2" case "sign_ext(polynomial(p(jj), n(jj))(x)) = ") "1" case "number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), LAMBDA (i): polynomial(p(i), n(i))(y),") "1" expand "sign_ext" )"1" "1" "1" "1" assert )"1" "1" expand "number_sign_changes" "1" expand "number_sign_changes" "1" expand "sign_ext" )"1" "1" "1" "1" assert )"1" "1" "1" assert )"1" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "number_sign_changes" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )"3" "3" expand "number_sign_changes" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "number_sign_changes" "2" expand "number_sign_changes" "2" expand "sign_ext" )"2" "2" "2" "2" assert )"2" "1" "1" assert )"1" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "number_sign_changes" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )"3" "3" expand "number_sign_changes" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" expand "number_sign_changes" "4" assert )"4" "4" assert )nil nil ))nil ))nil ))nil )"5" "5" assert )"5" "1" expand "number_sign_changes" "1" assert )"1" "1" "1" nil nil )"2" "2" expand "number_sign_changes" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "number_sign_changes" "3" expand "number_sign_changes" "3" expand "sign_ext" )"3" "3" "3" "3" assert )"3" "1" "1" "1" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" expand "number_sign_changes" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" expand "number_sign_changes" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil )"4" expand "number_sign_changes" "4" assert )"4" "4" assert )nil nil ))nil ))nil ))nil )"5" "5" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "1" "1" expand "number_sign_changes" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" expand "number_sign_changes" "4" expand "number_sign_changes" "4" expand "sign_ext" )"4" "4" "4" "4" assert )"4" "1" "1" "1" nil nil )"2" "2" expand "number_sign_changes" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "number_sign_changes" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "3" "1" "1" expand "number_sign_changes" "1" assert )nil nil ))nil ))nil )"2" assert )"2" "2" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )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 )"2" "2" "hyplem" )"2" "2" "jj-1" )"2" assert )"2" replace "2" replace "2" "2" expand "SQUAB" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT sign_ext(polynomial(p(jj), n(jj))(x)) = ") "1" expand "sign_ext" "1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" case "number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), LAMBDA (i): polynomial(p(i), n(i))(y),") "1" expand "sign_ext" )"1" "1" "1" "1" assert )"1" "1" expand "number_sign_changes" "1" expand "number_sign_changes" "1" expand "sign_ext" )"1" "1" "1" "1" assert )"1" "1" "1" assert )"1" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"3" expand "number_sign_changes" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil )"4" "4" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "number_sign_changes" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "number_sign_changes" "2" expand "number_sign_changes" "2" expand "sign_ext" )"2" "2" "2" "2" assert )"2" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1" nil nil )"2" expand "number_sign_changes" "2" assert )"2" "2" expand "number_sign_changes" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"3" expand "number_sign_changes" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil )"4" "4" "1" "1" nil nil )"2" "2" expand "number_sign_changes" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" nil nil )"2" "2" expand "number_sign_changes" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "number_sign_changes" "3" expand "number_sign_changes" "3" expand "sign_ext" )"3" "3" "3" "3" assert )"3" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"3" expand "number_sign_changes" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil )"4" "4" "1" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" expand "number_sign_changes" "4" expand "number_sign_changes" "4" expand "sign_ext" )"4" "4" "4" "4" assert )"4" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "1" "1" expand "number_sign_changes" "1" assert )nil nil ))nil ))nil )"2" assert )"2" "2" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "number_sign_changes" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil )"4" "4" "1" "1" expand "number_sign_changes" "1" assert )nil nil ))nil ))nil )"2" "2" "1" expand "number_sign_changes" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "number_sign_changes" "2" assert )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" "2" "hyplem" )"2" "2" "jj-1" )"2" assert )"2" replace "2" replace "2" "2" expand "SQUAB" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (x1,x2:real): x<=x1 AND x1<x2 AND x2<=y IMPLIES sign_ext(polynomial(p(1 + jj), n(1 + jj))(x1)) = ") "1" "x" "b" )"1" "b" "y" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" "squiggy" "2" "squiggy" )"2" expand "sign_ext" "2" "2" "2" "2" "2" assert )"2" "1" "poly_intermediate_value_inc" )"1" "p(1+jj)" "0" "n(1+jj)" "x1" "x2" )"1" assert )"1" "1" "cc" "1+jj" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(1+jj)" "0" "n(1+jj)" "x1" "x2" )"2" assert )"2" "2" "cc" "1+jj" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "x2" )"3" "x2" "1+jj" )"3" assert )nil nil ))nil ))nil )"4" "x1" "1+jj" )"4" assert )nil nil ))nil )"5" "x1" "1+jj" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "squiggy" "2" "squiggy" )"2" case "FORALL (x1,x2:real): x<=x1 AND x1<x2 AND x2<=y IMPLIES sign_ext(polynomial(p(jj - 1), n(jj - 1))(x1)) = ") "1" "x" "b" )"1" "b" "y" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" expand "sign_ext" "2" "2" "2" "2" "2" assert )"2" "1" "poly_intermediate_value_inc" )"1" "p(jj-1)" "0" "n(jj-1)" "x1" "x2" )"1" assert )"1" "1" "cc" "jj-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(jj-1)" "0" "n(jj-1)" "x1" "x2" )"2" assert )"2" "2" "cc" "jj-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "x2" "jj-1" )"3" assert )nil nil ))nil )"4" "x1" "jj-1" )"4" assert )nil nil ))nil )"5" "x1" "jj-1" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "sturm_seq_repeated_root" )"2" "m" "n" "p" "b" )"2" assert )"2" "jj-1" )"2" assert )"2" "jj+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 ))nil ))nil ))nil ))nil )"posint" nil )nil naturalnumbers nil )"int" integers nil )nil sturmsquarefree nil )"real" reals nil )"naturalnumber" sturmsquarefree nil )"odd_int" integers nil )nil sturmsquarefree nil )nil more_polynomial_props "reals/" )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil more_polynomial_props "reals/" )"real" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sturmsquarefree nil )"real" sturmsquarefree nil )"real" sturmsquarefree nil )"bool" reals nil )"[nat -> nat]" sturmsquarefree nil )nil integers nil )nil integers nil )nil real_types nil )"int" integers nil )nil min_max "reals/" )nil abs_rews "ints/" )"real" reals nil )"real" sigma "reals/" )"odd_int" integers nil )nil naturalnumbers nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil polynomials "reals/" )nil polynomials "reals/" )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[T, T -> boolean]" equalities nil )nil sequences nil )"[real -> real]" polynomials "reals/" )"boolean" notequal nil )"bool" sturmsquarefree nil )nil number_sign_changes nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" "reals/" )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"NSC" number_sign_changes nil ))nil )nil 3587808541"" case " FORALL (b: real, dd,j, m: nat, n: [nat -> nat], AND AND x < b AND b < yAND (FORALL (c: real, i: nat):AND AND c <= y AND polynomial(p(i), n(i))(c) = 0AND (FORALL (c:real): x<=c AND c<=y AND polynomial(p(0),n(0))(c)=0 IMPLIESAND j + 1 <= m AND polynomial(p(j + 1), n(j + 1))(b) /= 0 AND sturm_sequence?(p, n, m)LET nsc =LAMBDA (xyz: real, pj: nat):LAMBDA AND ") "1" (skeep)"1" (inst - "b" "j" "j" "m" "n" "p" "x" "y" )"1" (assert )"1" (replace -5)"1" (replace -6) (("1" (propax) nil )))))))))))"2" (hide 2)"2" (induct "dd" )"1" (assert ) nil )"2" (skeep)"2" (assert )"2" (case "NOT j = 0" )"1" (assert ) nil )"2" (hide -2)"2" (replaces -1)"2" (expand "number_sign_changes" )"2" (expand "number_sign_changes" )"2" (assert )"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" "2" "2" assert )"2" "2" "2" assert )"2" case "NOT sign_ext(polynomial(p(1), n(1))(y)) = sign_ext(polynomial(p(1), n(1))(x))" )"1" "1" expand "sign_ext" 1)"1" "1" "1" "1" "1" assert )"1" "1" "poly_intermediate_value_dec" )"1" "p(1)" "0" "n(1)" "x" "y" )"1" assert )"1" "1" "cc" "1" )"1" assert )nil )))))))))))"2" "poly_intermediate_value_inc" )"2" "p(1)" "0" "n(1)" "x" "y" )"2" assert )"2" "2" "cc" "1" )"2" assert )nil )))))))))))"3" "poly_intermediate_value_inc" )"3" "p(1)" "0" "n(1)" "x" "y" )"3" assert )"3" "3" "cc" "1" )"3" assert )nil )))))))))))"4" "poly_intermediate_value_inc" )"4" "p(1)" "0" "n(1)" "x" "y" )"4" assert )"4" "4" "cc" "1" )"4" assert )nil )))))))))))"5" "poly_intermediate_value_dec" )"5" "p(1)" "0" "n(1)" "x" "y" )"5" assert )"5" "5" "cc" "1" )"5" assert )nil )))))))))))))))))))))))))))"2" assert )"2" case "polynomial(p(1), n(1))(x) = 0" )"1" "x" "1" )"1" (assert ) nil )))"2" case "polynomial(p(0), n(0))(x) = 0" )"1" "x" "0" )"1" assert )nil )))"2" case "polynomial(p(0), n(0))(y) = 0" )"1" "y" "0" )"1" assert )nil )))"2" case "polynomial(p(1), n(1))(y) = 0" )"1" "y" "1" )"1" assert )nil )))"2" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))"3" (skolem 1 "jj" )"3" (flatten)"3" (skeep)"3" (assert )"3" (case "NOT j = 1+jj" )"1" (inst - "b" "j" "m" "n" "p" "x" "y" )"1" (assert )"1" (replace -6)"1" (replace -7) (("1" (propax) nil )))))))))"2" (replace -1)"2" (assert )"2" (inst-cp - "x" "1+jj" )"2" (assert )"2" (inst-cp - "y" "1+jj" )"2" (assert )"2" "x" "2+jj" )"2" assert )"2" "y" "2+jj" )"2" assert )"2" case "polynomial(p(1+jj),n(1+jj))(b)/=0" )"1" "1" "b" "j-1" "m" "n" "p" "x" "y" )"1" assert )"1" replace -7)"1" replace -8)"1" "1" "1" replace -1)"1" assert )"1" expand "number_sign_changes" "1" assert )"1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "p(2+jj)" "0" "n(2+jj)" "x" "y" )"1" assert )"1" "1" "cc" "2+jj" )"1" assert )nil )))))))))))"2" "poly_intermediate_value_dec" )"2" "p(2+jj)" "0" "n(2+jj)" "x" "y" )"2" assert )"2" "2" "cc" "2+jj" )"2" assert )nil )))))))))))))))))))))))))))))))))"2" expand "number_sign_changes" "2" assert )"2" "2" "2" "2" assert )"2" "1" "number_sign_changes_lastnz_nonzero" )"1" "1" rewrite "1" "0" )"1" "1" )"1" assert )"1" "y" )"1" assert )nil )))))))))))))))"2" expand "number_sign_changes" "2" "2" assert )"2" expand "number_sign_changes" "2" "2" case "FORALL (pj:nat): pj=1+jj OR pj = 2+jj IMPLIES sign_ext(polynomial(p(pj), n(pj))(x)) = sign_ext(polynomial(p(pj), n(pj))(y))" )"1" "1+jj" )"1" "2+jj" )"1" assert )nil )))))"2" "2" "2" expand "sign_ext" "2" "2" "2" "2" "2" assert )"2" "1" "1" "1" nil )"2" "poly_intermediate_value_inc" )"2" "p(pj)" "0" "n(pj)" "x" "y" )"2" assert )"2" "2" "cc" "pj" )"2" nil )))))))))))))))"2" "2" assert )"2" "1" "1" "1" "poly_intermediate_value_dec" )"1" "p(pj)" "0" "n(pj)" "x" "y" )"1" assert )"1" "1" "cc" "pj" )"1" nil )))))))))))"2" "2" "1" nil )"2" "poly_intermediate_value_dec" )"2" "p(pj)" "0" "n(pj)" "x" "y" )"2" assert )nil )))))))))))))"2" "2" "1" nil )"2" "2" nil )))))))))))))))))))))))))))))))))))))))))))"3" "number_sign_changes_lastnz_nonzero" )"3" "3" rewrite "3" "0" )"3" "1" )"3" assert )"3" "x" )"3" assert )nil )))))))))))))))"4" expand "number_sign_changes" "4" "4" expand "number_sign_changes" "4" "4" case "FORALL (pj:nat): pj=1+jj OR pj = 2+jj IMPLIES sign_ext(polynomial(p(pj), n(pj))(x)) = sign_ext(polynomial(p(pj), n(pj))(y))" )"1" "1+jj" )"1" "2+jj" )"1" nil )))))"2" "2" "2" expand "sign_ext" "2" "2" "2" "2" "2" assert )"2" "1" "1" "1" nil )"2" "poly_intermediate_value_inc" )"2" "p(pj)" "0" "n(pj)" "x" "y" )"2" assert )"2" "2" "cc" "pj" )"2" nil )))))))))))))))"2" "2" assert )"2" "1" "1" "1" "poly_intermediate_value_dec" )"1" "p(pj)" "0" "n(pj)" "x" "y" )"1" assert )"1" "1" "cc" "pj" )"1" nil )))))))))))"2" "2" "1" nil )"2" "poly_intermediate_value_dec" )"2" "p(pj)" "0" "n(pj)" "x" "y" )"2" assert )nil )))))))))))))"2" "2" "1" nil )"2" "2" nil )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))"2" "2" "hyplem" -3)"2" "hyplem" )"2" "2" expand "sturm_sequence?" "2" "2" "2" "b" "1+jj" )"2" assert )"2" case "polynomial(p(jj), n(jj))(b) = 0" )"1" "1" expand "sign_ext" )"1" "1" assert )nil )))))))"2" "x" "jj" )"2" "y" "jj" )"2" assert )"2" case "FORALL (pj:nat,x1,x2:real): ((pj=jj OR pj = 2+jj) AND (x<=x1 AND x1<=y AND x<=x2 AND x2<=y)) IMPLIES sign_ext(polynomial(p(pj), n(pj))(x1)) = sign_ext(polynomial(p(pj), n(pj))(x2))" )"1" "jj" "x" "b" )"1" "jj" "b" "y" )"1" "2+jj" "x" "b" )"1" "2+jj" "b" "y" )"1" assert )"1" "1" expand "number_sign_changes" "1" "1" assert )nil )))))"2" case "jj = 0" )"1" "1" assert )"1" expand "sign_ext" )"1" "1" "1" "1" assert )"1" "1" case "polynomial(p(1), n(1))(x) > 0" )"1" case "polynomial(p(1), n(1))(y) < 0" )"1" case "NOT number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), 1)`num = 0" )"1" expand "number_sign_changes" "1" assert )"1" expand "number_sign_changes" "1" expand "sign_ext" "1" nil )))))))))"2" case "NOT number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(y), 1)`num = 1" )"1" expand "number_sign_changes" "1" expand "number_sign_changes" "1" expand "sign_ext" "1" assert )nil )))))))"2" case "NOT number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), 2)`num = 1" )"1" expand "number_sign_changes" "1" expand "number_sign_changes" "1" expand "number_sign_changes" "1" expand "sign_ext" "1" assert )nil )))))))))"2" case "NOT number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(y), 2)`num = 1" )"1" expand "number_sign_changes" "1" expand "number_sign_changes" "1" expand "number_sign_changes" "1" expand "sign_ext" "1" assert )nil )))))))))"2" assert )"2" nil )))))))))))"2" nil )))"2" nil )))"2" nil )))))))))))))))))"2" nil )))))))))))))))"2" nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )nil nil ))nil 3587920247"" case "FORALL (dd,j, m: nat, n: [nat -> nat], p: [nat -> [nat -> real]], AND AND (FORALL (c: real, i: nat):AND AND c <= y AND polynomial(p(i), n(i))(c) = 0AND (FORALL (c: real):AND c <= y AND polynomial(p(0), n(0))(c) = 0 IMPLIESAND j<= m AND polynomial(p(j), n(j))(y) /= 0AND sturm_sequence?(p, n, m) AND p(1) = poly_deriv(p(0))AND n(1) = n(0) - 1LET nsc =LAMBDA (xyz: real, pj: nat):LAMBDA AND IF polynomial(p(0), n(0))(y) = 0 THEN 1 ELSE 0 ENDIF)") "1" (skeep)"1" (inst - "j" "j" "m" "n" "p" "x" "y" )"1" (assert )"1" (replace -3)"1" (replace -4) (("1" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "dd" )"1" (assert ) nil nil )"2" (skeep)"2" (assert )"2" (case "NOT j = 0" )"1" (assert ) nil nil )"2" (hide -2)"2" (replaces -1)"2" (expand "number_sign_changes" )"2" (expand "sign_ext" 2)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" assert )"2" "1" "poly_intermediate_value_inc" )"1" "p(0)" "0" "n(0)" "x" "y" )"1" assert )"1" "1" "cc" "0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(0)" "0" "n(0)" "x" "y" )"2" assert )"2" "2" "cc" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" "x" "0" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem 1 "jj" )"3" (flatten)"3" (skeep)"3" (assert )"3" (case "NOT j = 1+jj" )"1" (inst - "j" "m" "n" "p" "x" "y" )"1" (assert )"1" (replace -4)"1" (replace -5) (("1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (replaces -1)"2" (assert )"2" (inst-cp - "x" "jj" )"2" (assert )"2" (inst-cp - "x" "1+jj" )"2" (assert )"2" case "polynomial(p(jj),n(jj))(y)/=0" )"1" "1" "jj" "m" "n" "p" "x" "y" )"1" assert )"1" replace -4)"1" replace -5)"1" "1" "1" assert )"1" expand "number_sign_changes" "1" assert )"1" "1" expand "sign_ext" "1" "1" "1" "1" assert )"1" "1" "poly_intermediate_value_inc" )"1" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"1" assert )"1" "1" "cc" "1+jj" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "poly_intermediate_value_dec" )"2" "p(1+jj)" "0" "n(1+jj)" "x" "y" )"2" assert )"2"
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.792Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
