(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)"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)"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)"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)"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" quality 99%
¤ 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.69Bemerkung:
(vorverarbeitet)
¤ *Bot Zugriff
