SSL compute_sturm_tarski.prf
Interaktion und
(compute_sturm_tarskinil 3619442978 ("" (subtype-tcc) nil nil ) nil nil ))nil 3619442978"" (skeep)"" (expand "polynomial_prod" )"" (assert )"" case "FORALL (abc:[nat->int],i1,i2:nat): rational_pred(sigma(i1,i2,abc)) AND integer_pred(sigma(i1,i2,abc))" )"1" (inst?)"1" (hide 2)"1" (skosimp*)"1" (expand "poly_deriv" ) (("1" (propax) nil nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (assert )"2" (induct "i2" )"1" (skeep)"1" (expand "sigma" )"1" (lift-if)"1" (assert )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (inst - "abc" "i1" )"2" (flatten)"2" (expand "sigma" +)"2" (assert )"2" (lift-if)"2" assert )"2" "integers.closed_plus" )"2" "2" assert )"2" "rationals.closed_plus" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"int" integers nil )"int" integers nil )"real" polynomials "reals/" )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[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 )"[bool, bool -> bool]" booleans nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[nat -> int]" compute_sturm_tarski nil )"[nat -> int]" compute_sturm_tarski nil )"nat" compute_sturm_tarski nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil sequences nil )"real" polynomials "reals/" )"[numfield, numfield -> numfield]" number_fields nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"real" reals nil )nil integers nil )nil rationals nil )nil rationals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil naturalnumbers nil )nil defined_types nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3594487196"" (skeep)"" (case "NOT m-1>=0" )"1" (hide 2)"1" (expand "bijective?" )"1" (flatten)"1" (expand "surjective?" )"1" (inst - "x" )"1" (assert ) (("1" (skosimp*) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (copy -2)"2" (expand "bijective?" -1)"2" (flatten)"2" (copy -2)"2" (expand "surjective?" -1)"2" (inst - "x" )"2" (skolem -1 "ii" )"2" "LAMBDA (i:below(m-1)): IF i<ii THEN bij(i) ELSE bij(i+1) ENDIF" )"1" (expand "bijective?" +)"1" (split +)"1" (expand "injective?" 1)"1" "1" "1" "1" "1" assert )"1" expand "injective?" -3)"1" "1" "x1" "x2" )"1" (assert ) nil nil ))nil )"2" "x1" "1+x2" )"2" (assert ) nil nil ))nil )"3" "1+x1" "x2" )"3" (assert ) nil nil ))nil )"4" "1+x1" "1+x2" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" "2" "y" )"2" "y" )"2" assert )"2" "jj" )"2" case "ii = jj" )"1" expand "injective?" )"1" "ii" "jj" )"1" (assert ) nil nil ))nil ))nil )"2" "2" assert )"2" case "jj<ii" )"1" "jj" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "jj-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "injective?" )"2" (skeep)"2" (inst - "1+i" "ii" )"2" (assert ) nil nil )) nil ))nil ))nil )"3" (expand "injective?" )"3" (skeep)"3" (inst - "i" "ii" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )"bool" functions nil )"bool" functions nil )"(total_order?[real])" nil )"real" compute_sturm_tarski nil )"set[real]" compute_sturm_tarski nil )set type-eq-decl nil sets nil )"int" integers nil )"below(m)" compute_sturm_tarski nil )"bool" functions nil )"posint" nil )"(strict_total_order?[real])" real_props nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"nat" compute_sturm_tarski nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"below(m)" compute_sturm_tarski nil )"boolean" notequal nil )"[below(m) -> (A)]" compute_sturm_tarskinil )"posint" nil ))nil 3594488379"" case "FORALL (x, y: real, m: nat, A: set[real], bij: [below(m) -> (A)],i,j:below(m)): AND A(x) AND A(y) AND x /= y AND i<j AND bij(i)=x AND bij(j)=y IMPLIESAND AND r /= y}]):") "1" (skeep)"1" (copy -2)"1" (expand "bijective?" -1)"1" (flatten)"1" (expand "surjective?" -2)"1" (inst-cp - "x" )"1" (inst - "y" )"1" (skosimp*)"1" (case "x!1 < x!2" )"1" (inst - "y" "x" "m" "A" "bij" "x!1" "x!2" )"1" (assert )"1" (skosimp*)"1" (inst + "bijec!1" )"1" assert )"1" expand "bijective?" (-5 2))"1" "1" "1" expand "injective?" (-5 1))"1" (propax) nil nil ))nil )"2" expand "surjective?" (-6 1))"2" "2" "y!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "x" "y" "m" "A" "bij" "x!2" "x!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (case "NOT m-2>=0" )"1" (hide 3) (("1" (assert ) nil nil )) nil )"2" (assert )"2" "LAMBDA (ii:below(m-2)): IF ii<i THEN bij(ii) ELSIF ii+1 < j THEN bij(ii+1) ELSE bij(ii+2) ENDIF" )"1" (expand "bijective?" )"1" (flatten)"1" (split)"1" (expand "injective?" )"1" (skosimp*)"1" (lift-if)"1" (lift-if)"1" (lift-if)"1" "1" assert )"1" "1" "x1!1" "x2!1" )"1" (assert ) nil nil ))nil )"2" "x1!1" "1+x2!1" )"2" (assert ) nil nil ))nil )"3" "x1!1" "2+x2!1" )"3" (assert ) nil nil ))nil )"4" "1+x1!1" "x2!1" )"4" (assert ) nil nil ))nil )"5" "1+x1!1" "1+x2!1" )"5" (assert ) nil nil ))nil )"6" "1+x1!1" "2+x2!1" )"6" (assert ) nil nil ))nil )"7" "2+x1!1" "x2!1" )"7" (assert ) nil nil ))nil )"8" "2+x1!1" "1+x2!1" )"8" (assert ) nil nil ))nil )"9" "2+x1!1" "2+x2!1" )"9" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (inst - "y!1" )"2" (skosimp*)"2" (case "x!1 = i OR x!1 = j" )"1" (ground) nil nil )"2" "2" "ii" "x!1" )"2" "2" assert )"2" case "ii < i" )"1" "ii" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" case "ii-1<j" )"1" "ii-1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" "ii-2" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (expand "bijective?" )"2" (flatten)"2" (assert )"2" (expand "injective?" )"2" (inst-cp - "i" "2+ii!1" )"2" (assert )"2" assert )"2" "j" "2+ii!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (skeep)"3" (expand "bijective?" )"3" (flatten)"3" (expand "injective?" )"3" (inst-cp - "1+ii" "i" )"3" (assert )"3" (assert )"3" "1+ii" "j" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "bijective?" )"4" (flatten)"4" (expand "injective?" )"4" (skeep)"4" (inst-cp - "ii" "i" )"4" (assert )"4" (assert )"4" (inst - "ii" "j" )"4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )"nat" compute_sturm_tarski nil )"below(m)" compute_sturm_tarski nil )"set[real]" compute_sturm_tarski nil )"[below(m) -> (A)]" compute_sturm_tarskinil )"real" compute_sturm_tarski nil )"real" compute_sturm_tarski nil )"below(m)" compute_sturm_tarski nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"below(m)" compute_sturm_tarski nil )"posint" nil )"bool" functions nil )"real" compute_sturm_tarski nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"real" compute_sturm_tarski nil )"set[real]" compute_sturm_tarski nil )"int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )set type-eq-decl nil sets nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" functions nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3593788550"" (skeep)"" (assert )"" (expand "der_prod" )"" (expand "polynomial_prod" )"" (expand "max" )"" (expand "sigma" )"" (expand "sigma" )"" (expand "poly_deriv" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"real" polynomials "reals/" )"real" sigma "reals/" )"real" polynomials "reals/" )"(divides(n))" divides nil )"(divides(m))" divides nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"int" compute_sturm_tarski nil ))nil ))nil 3593788550 ("" (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 )"int" integers nil )"(strict_total_order?[real])" real_props nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"posint" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"list[int]" polynomial_pseudo_divide"Sturm/" )"{k | abs(k) < abs(j)}" mod nil )"list[int]" gcd_coeff "Sturm/" )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"T" list_props nil )nil nat_types nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" compute_sturm_tarski nil )"bool" remainder_sequence"Sturm/" )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"boolean" notequal nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"posint" nil )"int" integers nil ))nil ))nil 3593788550 ("" (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 )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"list[int]" gcd_coeff "Sturm/" )"{k | abs(k) < abs(j)}" mod nil )"list[int]" polynomial_pseudo_divide"Sturm/" )"(total_order?[real])" nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"posint" nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"T" list_props nil )nil nat_types nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" compute_sturm_tarski nil )"bool" remainder_sequence"Sturm/" )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"boolean" notequal nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"posint" nil )"int" integers nil ))nil ))nil 3593788550 ("" (subtype-tcc) nil nil )"boolean" notequal nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"int" integers nil )"posint" nil ))nil ))nil 3593790499 ("" (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 )"int" integers nil )"(strict_total_order?[real])" real_props nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"posint" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"{s: rat | s >= q AND s >= r}" nil )"list[int]" polynomial_pseudo_divide"Sturm/" )"{k | abs(k) < abs(j)}" mod nil )"list[int]" gcd_coeff "Sturm/" )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"T" list_props nil )nil nat_types nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" compute_sturm_tarski nil )"bool" remainder_sequence"Sturm/" )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"boolean" notequal nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"posint" nil )"int" integers nil ))nil ))nil 3593788956"" (skeep)"" "sl" "remainder_seq(a, ") "" (replace -1)"" "P" "LAMBDA (j: nat): IF j < length(sl)LAMBDA (i: nat): 0)") "1" (replaces -1)"1" "N" " LAMBDA (j: nat): IF j < length(sl)max (length(nth(sl, length(sl) - 1 - j)) - 1, 0)") "1" (name "M" "length(sl)-1" )"1" (replace -1)"1" (assert )"1" (replace -1)"1" (replace -2)"1" (replace -3)"1" (split +)"1" (copy 2)"1" "1" expand "constructed_sturm_sequence?" )"1" case "NOT %1" ) (! 2 1))"1" "1" "1" expand "P" -1)"1" expand "N" -1)"1" assert )"1" expand "max" -1)"1" "1" assert )"1" "1" "1" case "NOT length(sl)-1-i = 0" )"1" assert )"1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" "0" "length(sl)-1-i" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "sl" )"2" "2" expand "is_neg_remainder_list?" )"2" "2" "length(sl)-1-i" )"2" assert )"2" "list2array_sound[int]" )"2" "nth(sl,length(sl)-1-i)" "0" "length(nth(sl, length(sl) - 1 - i)) - 1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "frizzy1" -1)"2" assert )"2" replace -1)"2" "frizzy1" )"2" case "NOT %1" )"1" "1" "1" expand "N" 1)"1" expand "max" 1)"1" "1" "1" "1" assert )"1" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" "1" "1" "length(sl)-1-j" "length(sl)-1-i" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sl" )"2" "2" expand "is_neg_remainder_list?" "2" "2" "0" "length(sl)-1-j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "sl" )"3" "3" expand "is_neg_remainder_list?" "3" "3" "length(sl)-1-j" "length(sl)-1-i" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "frizzy2" -1)"2" "frizzy2" )"2" case "NOT %1" )"1" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" "1" "1" assert )"1" expand "N" "1" expand "max" "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "frizzy2" "2" "frizzy2" )"2" case "NOT %1" )"1" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" "1" "1" expand "P" "1" replace "1" replace "1" "1" "list2array_sound[int]" )"1" "1" replace "1" assert )"1" "1" "1" "1" expand "der_prod" )"1" "array2list[int] LAMBDA (i: nat):") "1" replace "1" "x!1" )"1" replace "1" assert )"1" expand "poly_deriv" "1" expand "polynomial_prod" "1" case "NOT N(0)=n" )"1" "1" expand "N" "1" expand "max" "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" rewrite "sigma_eq" )"1" "1" "1" "list2array_sound[int]" )"1" case "NOT 1 - n!1 + x!1 >= 0" )"1" assert )nil nil )"2" "2" assert )"2" replace "2" "array2list[int](1+n)(a)" )"2" "1-n!1+x!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "der_prod(a,n,g,k)(i)" )"2" expand "der_prod" "2" assert )"2" case "FORALL (jj:int): rational_pred(jj)" )"1" "der_prod(a,n,g,k)(i)" )"1" expand "der_prod" )"1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" case "x!1 < k+n" )"1" assert )nil nil )"2" case "NOT N(0)=n" )"1" expand "N" "1" expand "max" "1" replace "1" assert )nil nil ))nil ))nil ))nil )"2" replace "2" assert )"2" expand "polynomial_prod" "2" rewrite "sigma_restrict_eq_0" "1" "1" nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )"2" "der_prod((list2array[int] ") "2" "der_prod((list2array[int] ") "2" expand "der_prod" "2" assert )"2" case "NOT N(0)=n" )"1" expand "N" "1" expand "max" )"1" replace "1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" case "FORALL (jj:int): rational_pred(jj)" )"1" "der_prod((list2array[int] ") "1" expand "der_prod" "1" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "N" "3" expand "max" "3" replace "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "frizzy3" "2" "frizzy3" )"2" case "NOT %1" )"1" "1" assert )"1" expand "N" "1" assert )"1" expand "max" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "frizzy4" "2" "frizzy4" )"2" case "NOT %1" )"1" "1" expand "N" "1" expand "M" "1" assert )nil nil ))nil ))nil ))nil )"2" replace "2" "frizzy5" "2" "frizzy5" )"2" case "NOT %1" )"1" "1" expand "P" "1" expand "M" "1" assert )"1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" assert )"1" case "nth(sl,0) = null" )"1" "1" "1" nil nil ))nil ))nil )"2" "2" "nth" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "frizzy6" "2" replace "frizzy6" )"2" "frizzy6" )"2" case "NOT %1" )"1" "1" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" "length(sl)-1-j" )"1" assert )"1" case "NOT P(j-2) = list2array[int](0)(nth(sl, 1 + length(sl) - j))" )"1" "1" "1" "ii" "x!1" )"1" "1" expand "P" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT N(j-2) = length(nth(sl, 1 + length(sl) - j)) - 1" )"1" expand "N" "1" assert )"1" expand "max" )"1" "1" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" "0" "1+length(sl)-j" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT P(j-1) = list2array[int](0)(nth(sl, length(sl) - j))" )"1" expand "P" "1" nil nil ))nil )"2" case "NOT N(j-1) = length(nth(sl, length(sl) - j)) - 1" )"1" expand "N" "1" expand "max" "1" "1" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" "0" "length(sl)-j" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" replace "2" replace "2" assert )"2" case "NOT P(j) = list2array[int](0)(nth(sl, length(sl) - j-1))" )"1" expand "P" "1" nil nil ))nil )"2" case "NOT N(j) = length(nth(sl, length(sl) - j - 1)) - 1" )"1" expand "N" "1" expand "max" "1" "1" assert )"1" "1" case "NOT j = M" )"1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" "0" "M-j" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "M" "2" assert )"2" replace "2" assert )"2" case "NOT length(adjusted_remainder(P(j - 2), N(j - 2))(P(j - 1), N(j - 1))) = 0" )"1" assert )nil nil )"2" "adjusted_remainder_empty" )"2" "1" assert )"1" "1" assert )"1" "1" )"1" assert )"1" "1" case "NOT %1 = 0" )"1" "1" case "NOT N(j)=0" )"1" assert )"1" expand "N" "1" expand "max" "1" nil nil ))nil ))nil ))nil )"2" case "P(j)(0)=0" )"1" assert )"1" replace "1" rewrite "polynomial_n0" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "list2array_sound[int]" )"2" "nth(sl,0)" "0" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "2" "2" expand "polynomial" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "i!1" )"2" assert )"2" expand "*" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "N" )"3" expand "max" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "N" )"2" nil nil ))nil ))nil )"3" "3" expand "N" )"3" nil nil ))nil ))nil )"4" "4" expand "N" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" expand "P" )"2" expand "N" )"2" assert )"2" "list2array_sound[int]" )"2" "2" assert )"2" "2" "2" expand "max" )"2" "2" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" "length(sl) - j + 1 -1" "length(sl)-j+1" )"1" "length(sl)-j+1-2" "length(sl) - j + 1 -1" )"1" assert )"1" case "NOT FORALL (ab1,ab2,ab3:nat): ab1 < ab2 AND ab2 < ab3 IMPLIES (NOT ab3-1<0)" )"1" "1" nil nil ))nil )"2" "length(nth(sl, length(sl) - 1 - j))" "length(nth(sl, length(sl) - j))" "length(nth(sl, 1 + length(sl) - j))" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (ab3:nat): NOT (i>ab3-1 AND i<ab3)" )"1" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "3" expand "P" )"3" expand "N" )"3" assert )"3" "list2array_sound[int]" )"3" "3" assert )"3" "3" "3" expand "max" )"3" "3" "1" replace "1" case "i < 0" )"1" assert )nil nil )"2" case "FORALL (pjk:nat): pjk-1<0 IMPLIES pjk = 0" )"1" "length(nth(sl,length(sl)-j))" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" case "FORALL (aa:int): NOT (i>aa-1 AND i<aa)" )"1" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" assert )"4" "frizzy1" )"4" nil nil ))nil ))nil ))nil ))nil )"2" "2" "frizzy2" )"2" "j-2" "j-1" )"1" assert )"1" "1" expand "N" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" replace "2" assert )"2" replace "2" assert )"2" assert )"2" case "NOT length(sl)=3" )"1" assert )nil nil )"2" replace "2" assert )"2" "2" "2" expand "N" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "N" "3" assert )nil nil ))nil ))nil ))nil )"3" "3" expand "N" "3" assert )nil nil ))nil ))nil )"4" "4" expand "N" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "mini" "2" "mini" "2" "adjusted_remainder_def" )"2" "1" "mini" )"1" "1" "1" "1" "1" "1" case "thispoly = P(j) AND thisdeg = N(j)" )"1" "1" case "NOT N(j)>=0" )"1" expand "N" "1" assert )nil nil ))nil )"2" assert )"2" "2" replace "2" replace "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mini" )"2" "1" replace "1" expand "thispoly" "1" expand "thisrem" "1" replace "1" expand "thisdeg" "1" expand "thisrem" "1" replace "1" "1" "1" "list2array_sound[int]" )"1" "1" "1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "thisdeg" "2" expand "thisrem" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "frizzy1" )"2" nil nil ))nil ))nil )"3" "3" "3" expand "P" )"3" expand "N" )"3" expand "max" )"3" "3" "1" expand "list2array" )"1" "1" "1" expand "length" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "list2array_sound[int]" )"2" "2" assert )"2" "2" "2" case "FORALL (ab3:nat): NOT (ii>ab3-1 AND ii<ab3)" )"1" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" "4" expand "P" )"4" expand "N" )"4" assert )"4" "list2array_sound[int]" )"4" "4" assert )"4" "4" "4" expand "max" )"4" "4" "1" replace "1" case "ii < 0" )"1" assert )nil nil )"2" case "FORALL (pjk:nat): pjk-1<0 IMPLIES pjk = 0" )"1" "length(nth(sl,length(sl)-j))" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" case "FORALL (aa:int): NOT (ii>aa-1 AND ii<aa)" )"1" "1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "N" )"2" assert )nil nil ))nil ))nil )"3" "3" expand "N" )"3" assert )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 ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "frizzydizzy" "2" "frizzydizzy" )"2" case "NOT (M=-1 OR M=0 OR M=1)" )"1" assert )nil nil )"2" "1" assert )nil nil )"2" assert )nil nil )"3" assert )"3" "frizzy1" )"3" "frizzy2" )"3" "frizzy3" )"3" "frizzy4" )"3" "frizzy5" )"3" replace "3" "frizzy6" )"3" replace "3" assert )"3" "0" )"3" assert )"3" replace "3" expand "polynomial_prod" "3" case "NOT N(0) = n" )"1" expand "N" "1" "1" expand "max" "1" assert )"1" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" expand "sigma" )"2" expand "sigma" )"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 )"3" "3" expand "N" "3" "3" assert )nil nil ))nil ))nil ))nil )"4" assert )"4" "4" assert )nil nil ))nil ))nil )"5" "5" assert )"5" "1" expand "N" "1" assert )nil nil ))nil )"2" "frizzy1" )"2" nil nil ))nil ))nil ))nil ))nil )"6" "6" assert )nil nil ))nil )"7" "7" expand "N" "7" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "N" "3" assert )"3" expand "max" "3" assert )"3" "sl" )"3" assert )"3" expand "is_neg_remainder_list?" )"3" "3" "3" replace "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 )"3" "3" assert )"3" "3" expand "N" 1)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "sl" )"2" "2" expand "is_neg_remainder_list?" )"2" "2" assert )"2" expand "M" 1)"2" replace -3)"2" "2" "ii" "x!1" )"2" replace -1)"2" "list2array_sound[int]" )"2" "2" "2" assert )"2" "2" "1" "array2list[int](1+n)(a)" )"1" "ii" )"1" assert )nil nil ))nil ))nil )"2" "ii" )"2" "ii" )"2" "ii" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "sl" )"3" "3" expand "is_neg_remainder_list?" )"3" "3" expand "max" )"3" "3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (skeep) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (hide 3) (("2" (skeep) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" compute_sturm_tarski nil )nil integers nil )nil integers nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"T" list_props nil )nil nat_types nil )"bool" reals nil )"nat" list_props nil )"bool" reals nil )"bool" remainder_sequence"Sturm/" )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )"boolean" notequal 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 list_adt nil )nil numbers nil )"int" integers nil )"(total_order?[real])" nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"T" array2list "structures/" )"[bool, bool -> bool]" booleans nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"odd_int" integers nil )"even_int" integersnil )"bool" sturmtarski nil )nil integers nil )"bool" reals nil )"real" polynomials "reals/" )"real" polynomials "reals/" )nil sequences nil )nil min_max "reals/" )"real" reals nil )nil sigma "reals/" )"nat" compute_sturm_tarski nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"subrange(max(1 - n + x!1, 0), k)" nil )"[nat -> int]" compute_sturm_tarski nil )"posnat" compute_sturm_tarski nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )nil listn "structures/" )"nat" compute_sturm_tarski nil )"[nat -> int]" compute_sturm_tarski nil )nil min_max "reals/" )"int" compute_sturm_tarski nil )"[list -> boolean]" list_adt nil )"(null?)" list_adt nil )"DivType" polynomial_division "Sturm/" )nil polynomial_division "Sturm/" )"[numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_ops "reals/" )"[real -> real]" polynomials "reals/" )nil real_types nil )nil real_types nil )"nzreal" real_typesnil )nil polynomial_pseudo_divide"Sturm/" )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"[bool, bool -> bool]" booleans nil )"list[int]" compute_sturm_tarski nil )"int" compute_sturm_tarski nil )"[nat -> int]" compute_sturm_tarskinil )"list[int]" polynomial_pseudo_divide"Sturm/" )"real" exponentiation nil )nil polynomials "reals/" )"odd_int" integersnil )nil polynomial_pseudo_divide"Sturm/" )"nat" compute_sturm_tarski nil )"{crem: (is_neg_remainder_list?(a, n, der_prod(a, n, g, k), n - 1 + k)) | AND length(nth(crem, 0)) = 0}" nil )"real" sigma "reals/" )"[nat -> [nat -> int]]" compute_sturm_tarskinil )"posint" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil array2list "structures/" )"(strict_total_order?[real])" real_props nil )"[nat -> int]" compute_sturm_tarski nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"(total_order?[real])" nil )"int" integers nil ))nil 3595179342"" (subtype-tcc) nil nil ) nil nil ))nil 3595179342"" (skeep)"" (assert )"" (expand "der_prod" )"" (expand "polynomial_prod" )"" (expand "max" )"" (expand "sigma" )"" (expand "sigma" )"" (expand "poly_deriv" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"real" polynomials "reals/" )"real" sigma "reals/" )"real" polynomials "reals/" )"(divides(n))" divides nil )"(divides(m))" divides nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"int" compute_sturm_tarski nil ))nil ))nil 3619438219 ("" (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 )"boolean" notequal nil )nil naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm_tarski nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3619438219 ("" (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 )"boolean" notequal nil )nil naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm_tarski nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"listn[real](0)" polynomial_division"Sturm/" )"listn[int](0)" gcd_coeff "Sturm/" )"(total_order?[real])" nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"int" integers nil ))nil ))nil 3619438219 ("" (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 )"boolean" notequal nil )nil naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm_tarski nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"{s: rat | s >= q AND s >= r}" nil )"(total_order?[real])" nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"int" integers nil ))nil ))nil 3619438219 ("" (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 )"boolean" notequal nil )nil naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm_tarski nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"{s: rat | s >= q AND s >= r}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"even_int" integersnil )"int" integers nil ))nil ))nil 3619438219 ("" (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 )"boolean" notequal nil )nil naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm_tarski nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"{s: rat | s >= q AND s >= r}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"even_int" integersnil )"int" integers nil ))nil ))nil 3619438219 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3619438219"" (skeep)"" (assert )"" (expand "der_prod" )"" (expand "polynomial_prod" )"" (replaces -1)"" (expand "max" )"" (expand "sigma" )"" (expand "sigma" )"" (expand "poly_deriv" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"real" polynomials "reals/" )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"real" polynomials "reals/" )"real" sigma "reals/" )"int" compute_sturm_tarski nil ))nil ))nil 3619438219 ("" (subtype-tcc) nil nil )"int" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil integers nil )"boolean" notequal nil )nil naturalnumbers nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )"list[int]" gcd_coeff "Sturm/" )"{k | abs(k) < abs(j)}" mod nil )"list[int]" polynomial_pseudo_divide"Sturm/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"posint" nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"(strict_total_order?[real])" real_props nil )"int" integers nil )"T" list_props nil )nil nat_types nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" list_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"int" compute_sturm_tarski nil )"bool" remainder_sequence"Sturm/" )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )"bool" compute_sturm_tarski nil )"posint" nil ))nil ))nil 3619451118"" (skeep)"" (expand "TQ" )"" "sl" "remainder_seq(LAMBDA IF i <= nLAMBDA IF i <= n") "" (replace -1)"" (expand "compute_TQ_param" :assert ? none)"" (skoletin 3)"" (skoletin 1)"" (skoletin 1)"" (skoletin 1)"" (skoletin 1)"" (replace -2 -1)"" (assert )"" (hide -2)"" (lemma "sturm_tarski_unbounded" )"" "g" "k" "M" "N" "P" )"1" "1" assert )"1" replace -1)"1" replace -2)"1" case "FORALL (relo:[[real,real]->bool]): NSol(P(0),N(0),g,k,relo) = NSol(a,n,g,k,relo)" )"1" ">" )"1" "<" )"1" (assert ) nil nil ))nil ))nil )"2" "2" "2" expand "NSol" 1)"2" case "Sol(P(0), N(0), g, k, relo) = Sol(a, n, g, k, relo)" )"1" assert )nil nil )"2" "2" "1" expand "Sol" "1" case "polynomial(P(0), N(0))(x!1) =polynomial(a, n)(x!1)" )"1" assert )"1" nil nil ))nil )"2" "2" expand "P" "2" expand "N" "2" "computed_sturm_spec" )"2" "2" assert )"2" replace "2" "1" "1" replace "1" assert )"1" replace "1" "1" "polynomial_eq_coeff" )"1" "LAMBDA (i: nat): IF i <= n THEN a(i) ELSE 0 ENDIF" "a" "n" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "N" 1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "N" 1)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "computed_sturm_spec" )"2" "2" assert )"2" replace -6)"2" assert )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "N" 1)"2" assert )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"int" compute_sturm_tarski nil )NOT const-decl "[bool -> bool]" booleans nil )"T" array2list "structures/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"odd_int" integers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil number_sign_changes "Sturm/" )"bool" booleans nil )"NSC" number_sign_changes "Sturm/" )"[numfield, numfield -> numfield]" number_fields nil )"bool" integers nil )"[numfield -> numfield]" number_fields nil )nil naturalnumbers nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"finite_set[real]" sturmtarski nil )"{d: nat | " sturmtarski nil) "(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil sturmtarski nil )nil sequences nil )"[real -> real]" polynomials "reals/" )"[nat -> [nat -> int]]" compute_sturm_tarskinil )nil compute_sturm_tarski nil )"(total_order?[real])" nil )"listn[int](0)" gcd_coeff "Sturm/" )"listn[real](0)" polynomial_division"Sturm/" )"even_int" integersnil )nil polynomials "reals/" )"[nat -> int]" compute_sturm_tarski nil )"int" compute_sturm_tarski nil )"(total_order?[real])" nil )"int" integers nil )nil numbers nil )nil list_adt 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 )"boolean" notequal nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" remainder_sequence"Sturm/" )"bool" reals nil )"nat" list_props nil )"bool" reals nil )nil nat_types nil )"T" list_props nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" "Sturm/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )nil integers nil )nil integers nil )"int" compute_sturm_tarski nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3620147464"" (skeep)"" (case "polynomial(g1,k)=polynomial(g2,k)" )"1" (rewrite "TQ_def" )"1" (rewrite "TQ_def" )"1" (expand "NSol" )"1" (expand "Sol" )"1" (assert )"1" (replace -1) (("1" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (lemma "polynomial_eq_coeff" )"2" (inst?) (("2" (assert ) 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 )"finite_set[real]" sturmtarski nil )"{d: nat | " sturmtarski nil) "int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"bool" reals nil )nil integers nil )nil compute_sturm_tarski nil )nil polynomials "reals/" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.377Bemerkung:
(vorverarbeitet am 2026-05-05)
¤ *Bot Zugriff
2026-05-26
