Impressum compute_sturm.prf
Sprache: Lisp
(compute_sturmnil 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 )"RealOrder" real_orders "reals/" )"real" compute_sturm nil )"set[real]" compute_sturm nil )set type-eq-decl nil sets nil )"int" integers nil )"below(m)" compute_sturm nil )"bool" functions nil )"posint" nil )"RealOrder" real_orders "reals/" )"(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 nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"below(m)" compute_sturm nil )"boolean" notequal nil )"[below(m) -> (A)]" compute_sturm nil )"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 nil )"below(m)" compute_sturm nil )"set[real]" compute_sturm nil )"[below(m) -> (A)]" compute_sturm nil )"real" compute_sturm nil )"real" compute_sturm nil )"below(m)" compute_sturm 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 nil )"posint" nil )"bool" functions nil )"real" compute_sturm nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"bool" functions nil )"real" compute_sturm nil )"set[real]" compute_sturm 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 ("" (subtype-tcc) nil nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )"real" polynomials "reals/" )"boolean" notequal 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 )"bool" reals nil )nil integers nil )nil integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"boolean" notequal nil )"real" polynomials "reals/" ))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 )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" 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 )"bool" reals nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"listn[int](0)" gcd_coeff nil )"listn[real](0)" polynomial_division nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )nil naturalnumbers nil )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )"int" integers 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 )"bool" reals nil )nil integers nil )nil integers nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"{s: rat | s >= q AND s >= r}" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )"int" integers nil ))nil ))nil 3593788956"" (skeep)"" (name "sl" "remainder_seq(a, n, poly_deriv(a), n - 1)" )"" (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 )"3" "-" "length(sl)-1" "3" "3" case "i=0" )"1" "array2list[int](1 + n)(a)" )"1" replace "1" "1" replace "1" replace "1" "1" "1" case "j=1" )"1" replace "1" "1" replace "1" "array2list[int](n)(poly_deriv(a))" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "length(sl) -1 -j" )"2" assert )"2" "2" "2" "length(sl) - 1 - j" "length(sl) -2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "frizzy2" -1)"2" "frizzy2" )"2" case "NOT %1" )"1" "1" "sl" )"1" "1" expand "is_neg_remainder_list?" "1" "1" expand "P" "1" assert )"1" replace "1" replace "1" "1" "list2array_sound[int]" )"1" "1" replace "1" assert )"1" "1" "1" "1" "array2list[int](n)(poly_deriv(a))" )"1" replace "1" assert )"1" "array2list[int](n)(poly_deriv(a))" )"1" "x!1" )"1" replace "1" assert )"1" expand "poly_deriv" "1" "1" "list2array_sound[int]" )"1" "1" assert )"1" replace "1" "array2list[int](1+n)(a)" )"1" "1+x!1" )"1" "1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "array2list[int](n)(poly_deriv(a))" )"2" "2" replace "2" expand "poly_deriv" "2" "list2array_sound[int]" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "poly_deriv" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "frizzy3" "2" "frizzy3" )"2" case "NOT %1" )"1" "1" assert )"1" expand "N" "1" assert )"1" "sl" )"1" "1" expand "is_neg_remainder_list?" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"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" )"2" assert )"2" "2" expand "N" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "N" "3" assert )nil 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" "frizzy2" )"3" "j-2" "j-1" )"3" assert )"3" "3" "3" expand "P" )"3" expand "N" )"3" assert )"3" "list2array_sound[int]" )"3" "3" assert )"3" "3" "3" expand "max" )"3" "3" "3" "sl" )"3" "3" expand "is_neg_remainder_list?" )"3" "3" "length(sl) - j + 1 -1" "length(sl)-j+1" )"3" "length(sl)-j+1-2" "length(sl) - j + 1 -1" )"3" assert )"3" 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 )"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 ))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" replace "3" "0" )"3" assert )"3" expand "poly_deriv" "3" assert )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" "frizzy2" )"7" "j-2" "j-1" )"1" assert )"1" assert )"1" expand "N" "1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "N" 1)"3" (assert ) 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 )nil number_fields nil )"real" polynomials "reals/" )nil sequences nil )nil integers nil )nil integers nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )"T" list_props nil )nil nat_types nil )"bool" reals nil )"nat" list_props nil )"bool" reals nil )"bool" remainder_sequence nil )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 )"RealOrder" real_orders "reals/" )"(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" sturm nil )nil real_props nil )nil real_props nil )nil real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"[numfield, numfield -> numfield]" number_fields nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )nil listn "structures/" )"posnat" compute_sturm nil )"[nat -> int]" compute_sturm nil )"int" integers nil )nil min_max "reals/" )"nat" compute_sturm nil )"{crem: (is_neg_remainder_list?(a, n, poly_deriv(a), n - 1)) | AND length(nth(crem, 0)) = 0}" compute_sturm nil )"nat" compute_sturm nil )nil polynomial_pseudo_dividenil )nil polynomials "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"real" reals nil )nil integers nil )"list[int]" polynomial_pseudo_dividenil )"[nat -> int]" compute_sturm nil )"int" compute_sturm nil )"list[int]" compute_sturm nil )"[bool, bool -> bool]" booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil polynomial_pseudo_dividenil )"nzreal" real_typesnil )"bool" reals nil )nil real_types nil )nil real_types nil )"[real -> real]" polynomials "reals/" )"[T -> real]" real_fun_ops "reals/" )"[numfield -> numfield]" number_fields nil )nil polynomial_division nil )"DivType" polynomial_division nil )"posint" nil )"(null?)" list_adt nil )"[list -> boolean]" list_adt nil )"int" compute_sturm nil )nil min_max "reals/" )"[nat -> [nat -> int]]" compute_sturm nil )nil array2list "structures/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"posint" nil )"[nat -> int]" compute_sturm nil )NOT const-decl "[bool -> bool]" booleans nil )nil naturalnumbers nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"listn[real](0)" polynomial_division nil )"listn[int](0)" gcd_coeff nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil ))nil 3595179342"" (subtype-tcc) nil nil ) nil nil ))nil 3595179342"" (subtype-tcc) nil nil )"real" polynomials "reals/" )"int" integers nil ))nil ))nil 3595179342"" (subtype-tcc) nil nil )"real" polynomials "reals/" )) nil ))nil 3594568781 ("" (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 )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )"int" integers nil ))nil ))nil 3594568781 ("" (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 )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"listn[int](0)" gcd_coeff nil )"listn[real](0)" polynomial_division nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"int" integers nil ))nil ))nil 3594568781 ("" (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 )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"{s: rat | s >= q AND s >= r}" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"int" integers nil ))nil ))nil 3594568781 ("" (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 )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )"{s: rat | s >= q AND s >= r}" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"int" integers nil )"posint" nil )"even_int" integersnil )"int" integers nil ))nil ))nil 3594568781 ("" (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 )"bool" reals nil ) (list type-decl nil list_adt nil )nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" compute_sturm nil )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"listn[int](0)" gcd_coeff nil )"listn[real](0)" polynomial_division nil )"{k: int | i <= k AND j <= k}" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )nil naturalnumbers nil )"bool" reals nil )"rat" exponentiation nil )"nzreal" exponentiation nil )"{s: rat | s >= q AND s >= r}" nil )"real" exponentiation nil )"[real -> real]" polynomials "reals/" )"boolean" notequal nil )"int" integers nil )"real" reals nil ))nil ))nil 3594568781 ("" (subtype-tcc) nil nil )"posrat" nil )"{s: rat | s >= q AND s >= r}" nil )"nzreal" exponentiation nil )"rat" exponentiation nil )nil naturalnumbers nil )"bool" reals nil )"{crem: (is_neg_remainder_list?(g, n, h, m)) | AND length(nth(crem, 0)) = 0}" nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"{k: int | i <= k AND j <= k}" nil )"listn[real](0)" polynomial_division nil )"listn[int](0)" gcd_coeff nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"bool" compute_sturm nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"boolean" notequal nil )"posreal" more_polynomial_props"reals/" )"real" polynomials "reals/" )"posnat" binomial "reals/" )"[real -> real]" polynomials "reals/" )"real" exponentiation nil )"int" integers nil )"real" reals nil )"posint" nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posreal" nil ))nil ))nil 3595067092"" (skeep)"" (typepred "sl" )"" (hide -1)"" (label "slname" -1)"" (expand "Eq_computed_remainder?" )"" (label "xlty" -2)"" (skoletin 2)"" (label "rootnamename" -1)"" (skoletin 1)"" (label "Asetname" -1)"" (label "final" 1)"" (hide "final" )"" expand "roots_closed_int" :assert ? none)"" (skoletin -2)"" "newaname" -2)"" replace "newaname" :dir rl)"" "" "Pname" -2)"" "" "Nname" -2)"" "" "Mname" -2)"" "" "nscnormname" "" "" "nschighlowname" "" "" "newlowname" "" "" "newhighname" "" "" "Nrootsname" "" "" "adjlowname" "" case "NOT polynomial(a,n) = polynomial(newa,n)" )"1" "1" "1" "poly_eq_le_degree" )"1" "1" assert )"1" "1" expand "newa" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "computed_sturm_spec" )"2" "newa" "n" )"2" assert )"2" replace "slname" "2" replace "Pname" "2" replace "Nname" "2" assert )"2" "polyeq" "2" "1" "1" "css" "1" case "NOT (P(0) = newa AND N(0) = n)" )"1" expand "P" "1" expand "N" "1" assert )nil nil ))nil ))nil )"2" "2" case "NOT (P(1) = poly_deriv(newa) AND N(1) = n-1)" )"1" expand "constructed_sturm_sequence?" "css" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "sturm" )"2" "M" "N" "P" "newlow" "newhigh" )"1" "1" replace "nscnormname" "1" assert )"1" replace "Nrootsname" "1" "1" "final" )"1" case "NOT rootnum>=0" )"1" "1" assert )nil nil ))nil )"2" assert )"2" "adjlowname" )"2" "adjlowname" )"1" "1" "1" assert )"1" "1" "LAMBDA (i:below(rootnum)): IF i=Nroots THEN x ELSE bij(i) ENDIF" )"1" assert )"1" expand "bijective?" )"1" "1" "1" expand "injective?" )"1" "1" "1" "1" "1" assert )"1" "1" "x1" "x2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" case "y!1 = x" )"1" "Nroots" )"1" assert )nil nil ))nil )"2" "y!1" )"1" "1" "x!1" )"1" assert )nil nil ))nil ))nil )"2" "final" )"2" case "NOT polynomial(P(0),N(0))(y!1)=0" )"1" "1" assert )"1" expand "Aset" "1" nil nil ))nil ))nil ))nil )"2" assert )"2" "y!1" )"2" "2" expand "Aset" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "i" )"2" "bij(i)" )"2" assert )"2" "poly_rootless_width_def" )"2" "2" assert )"2" "1" "bij(i)" "0" )"1" assert )"1" assert )"1" expand "Aset" "1" assert )"1" "poly_n_deriv_def" )"1" "a" )"1" assert )"1" "1" assert )"1" expand "abs" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" expand "Aset" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" assert )"2" "2" "bij" )"1" assert )"1" expand "bijective?" )"1" "1" "1" expand "injective?" )"1" "1" "x1" "x2" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"1" "1" "x!1" )nil nil ))nil )"2" assert )"2" "y!1" )"2" "2" expand "Aset" "2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" "1" nil nil ))nil )"2" "2" expand "Aset" "2" assert )"2" "bij(x1)" )"2" assert )"2" "1" expand "newlow" "1" "1" assert )"1" "1" nil nil )"2" "2" "poly_rootless_width_def" )"2" "2" assert )"2" "1" "bij(x1)" "0" )"1" assert )"1" assert )"1" "1" "poly_n_deriv_def" )"1" "1" assert )nil nil ))nil ))nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "n" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "newhigh" "2" "2" "1" nil nil )"2" assert )"2" "2" assert )"2" "poly_rootless_width_def" )"2" "2" assert )"2" "1" "bij(x1)" "0" )"1" assert )"1" assert )"1" "1" "poly_n_deriv_def" )"1" "1" assert )nil nil ))nil ))nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "n" )"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 )"2" expand "newlow" "2" expand "newhigh" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" assert )nil nil )"4" "4" assert )"4" expand "newlow" "4" "4" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" "poly_rootless_width_def" )"2" "2" "1" assert )"1" "x - poly_rootless_width(a, n, x, TRUE) / 2" "0" )"1" assert )"1" assert )"1" "poly_n_deriv_def" )"1" "1" assert )"1" "1" assert )"1" expand "abs" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" "5" assert )"5" expand "newhigh" "5" "5" "1" "1" assert )nil nil ))nil )"2" "2" assert )"2" "poly_rootless_width_def" )"2" "2" "1" assert )"1" "y+ poly_rootless_width(a, n, y, TRUE) / 2" "0" )"1" assert )"1" assert )"1" "poly_n_deriv_def" )"1" "1" "1" assert )"1" expand "abs" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "newhigh" "2" nil nil ))nil ))nil )"3" expand "newlow" "3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "newa" "2" nil nil ))nil )"3" "3" expand "newa" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" compute_sturm nil )"boolean" notequal nil )nil integers nil )"bool" reals nil )nil integers 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" list_adt nil )nil defined_types nil )nil list_adt nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"odd_int" integers nil )"int" integers nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"real" reals nil )"real" reals nil )"(bijective?[T, T])" identity nil )"[bool, bool -> bool]" booleans nil )"nat" list_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" array2list "structures/" )nil nat_types nil )"T" list_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil number_sign_changes nil )"NSC" number_sign_changes nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" more_polynomial_props"reals/" )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" real_orders "reals/" )nil compute_sturm nil )"numfield" compute_sturm nil )"numfield" compute_sturm nil )"nzreal" real_typesnil )"nzreal" nil )nil polynomials "reals/" )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil more_polynomial_props"reals/" )"bool" functions nil )"(Aset)" compute_sturm nil )"bool" functions nil )"[below(nscnorm(newlow)`num - nscnorm(newhigh)`num) -> AND AND polynomial(P(0), N(0))(xr) = 0}]" nil )"[real -> NSC]" compute_sturm nil )"real" compute_sturm nil )"[real -> boolean]" compute_sturm nil )"int" compute_sturm nil )"int" compute_sturm nil )"(Aset)" compute_sturm nil )"[below(nscnorm(newlow)`num - nscnorm(newhigh)`num) -> AND AND polynomial(P(0), N(0))(xr) = 0}]" nil )nil sturm nil )"bool" sturm nil )"real" polynomials "reals/" )"[nat -> [nat -> int]]" compute_sturm nil )"listn[int](0)" gcd_coeff nil )"listn[real](0)" polynomial_division nil )"[nat -> int]" compute_sturm nil )"RealOrder" real_orders "reals/" )"(strict_total_order?[real])" real_props nil )"posint" nil )nil polynomials "reals/" )"[nat -> int]" compute_sturm nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"rat" exponentiation nil )"nzreal" exponentiation nil )"RealOrder" real_orders "reals/" )"(total_order?[real])" nil )"rat" rationals nil )"int" integers nil )"[real -> real]" polynomials "reals/" )nil sequences nil )"bool" functions nil )nil naturalnumbers nil )"bool" booleans nil )"int" compute_sturm nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil ))nil ))nil 3595068138"" (skeep)"" (typepred "sl" )"" (hide -1)"" (label "slname" -1)"" (expand "Eq_computed_remainder?" )"" (label "xlty" -2)"" (skoletin 2)"" (label "rootnamename" -1)"" (skoletin 1)"" (label "Asetname" -1)"" (label "slname" -4)"" (label "final" 1)"" (hide "final" )"" expand "roots_closed_int" :assert ? none)"" "" "newaname" -2)"" "" replace -3 :dir rl)"" "Pname" -2)"" "" "Nname" -2)"" "" "Mname" -2)"" "" "nscnormname" "" "" "nschighlowname" "" "" "newlowname" "" "" "newhighname" "" "" "Nrootsname" "" "" "adjlowname" "" replace "" assert )"" case "NOT polynomial(a,n) = polynomial(newa,n)" )"1" "1" "1" "poly_eq_le_degree" )"1" "1" assert )"1" "1" expand "newa" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "computed_sturm_spec" )"2" "newa" "n" )"2" assert )"2" replace "slname" "2" replace "Pname" "2" replace "Nname" "2" "polyeq" "2" "1" "1" "css" "1" replace "Mname" "1" assert )"1" case "NOT (P(0) = newa AND N(0) = n)" )"1" expand "P" "1" expand "N" "1" assert )nil nil ))nil ))nil )"2" "2" case "NOT (P(1) = poly_deriv(newa) AND N(1) = n-1)" )"1" expand "constructed_sturm_sequence?" "css" )
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.518Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-02)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
