Quelle polynomial_division.prf
Sprache: Lisp
(polynomial_divisionnil 3582383554 ("" (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 )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )"{s: rat | s >= q AND s >= r}" nil )"{k: int | i <= k AND j <= k}" nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"int" integers nil ))nil ))nil 3582383554 ("" (subtype-tcc) nil nil ) nil nil ))nil 3582383554 ("" (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 )"boolean" notequal nil )"odd_int" integers nil ))nil ))nil 3582383554 ("" (subtype-tcc) nil nil )"DivType" polynomial_division nil )) nil ))nil 3582383554"" (skosimp*) (("" (assert ) (("" (postpone) nil nil )) nil )) nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3582383554 ("" (termination-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 )nil naturalnumbers nil )"boolean" notequal nil )"odd_int" integers nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"DivType" polynomial_division nil ))nil ))nil 3582383609 ("" (termination-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 )nil naturalnumbers nil )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"DivType" polynomial_division nil )"nonneg_int" nil ))nil ))nil 3582544163 ("" (termination-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 )"boolean" notequal nil )"odd_int" integers nil ))nil ))nil 3582555120 ("" (termination-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 )"boolean" notequal nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(divides(n))" divides nil )"(divides(m))" divides nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"int" integers nil )"posint" nil ))nil ))nil 3582385231"" case "FORALL (g, h: sequence[real], i, m, n: nat): AND i<=n-m AND (n-m-i) <= n - m IMPLIESLET pd = poly_divide(g, n)(h, m)((n-m-i)) IN") "1" (skeep)"1" (inst - "g" "h" "n-m-i" "m" "n" )"1" (assert )"1" (split -)"1" (propax) nil nil )"2" (skeep)"2" (assert )"2" (expand "poly_divide" )"2" (expand "make_divtype" )"2" (expand "polynomial" + 1)"2" (expand "sigma" )"2" (expand "sigma" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skeep)"2" (expand "poly_divide" )"2" (expand "make_divtype" )"2" (expand "polynomial" + 1)"2" (expand "sigma" )"2" (expand "sigma" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "NOT FORALL (g, h: sequence[real], i, m, n: nat): AND i = n - m IMPLIESLET pd = poly_divide(g, n)(h, m)(i) IN") "1" (hide 2)"1" (skeep)"1" (replaces -1)"1" (assert )"1" (skeep 2)"1" (assert )"1" (name "pd" "poly_divide(g, n)(h, m)(n - m)" )"1" (replace -1)"1" (expand "poly_divide" :assert ? none)"1" (lift-if)"1" (split -)"1" "1" assert )"1" expand "make_divtype" )"1" "1" assert )"1" case "%1=0" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" "1" assert )"1" expand "*" )"1" expand "make_divtype" )"1" replace -1 :dir rl)"1" assert )"1" rewrite "polynomial_n0" )"1" rewrite "polynomial_n0" )"1" assert )"1" "scal_polynomial" )"1" "(1/h(0))*g" "n" "h(0)" )"1" expand "*" )"1" "1" "x" )"1" expand "const_fun" )"1" "1" rewrite "poly_eq_le_degree" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mz" 1)"2" "mz" )"2" "2" "2" assert )"2" expand "make_divtype" )"2" assert )"2" case "NOT polynomial(pd`quot, pd`qdeg)(x) = (g(n)/h(m))*x^(n-m)" )"1" "1" "1" assert )"1" replace "1" assert )"1" expand "polynomial" )"1" "sigma_eq_one_arg" )"1" "1" "n-m" )"1" assert )"1" "1" "1" assert )"1" "1" "1" assert )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "mul_x_to_n_polynomial" )"2" case "n = m" )"1" assert )"1" "1" assert )"1" "1" "1" assert )"1" replace "1" assert )"1" expand "polynomial" "1" rewrite "sigma_scal" "1" rewrite "sigma_scal_right" "1" expand "polynomial" )"1" expand "sigma" "1" expand "sigma" "1" case "x^0 = 1" )"1" "1" assert )"1" case "NOT g(m)*x^m = h(m) * x ^ m * (g(m) / h(m))" )"1" assert )nil nil )"2" "2" assert )"2" rewrite "sigma_sum" )"2" rewrite "sigma_eq" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "h" "m" "n-m" )"1" assert )"1" "1" "x" )"1" assert )"1" expand "*" )"1" replace "1" "scal_polynomial" )"1" "%1" "n" "g(n)/h(m)" )"1" expand "const_fun" )"1" expand "*" )"1" "1" "x" )"1" replace "1" replace "1" assert )"1" "1" assert )"1" rewrite "polynomial_rec" "1" "polynomial_rec" )"1" "%1" "n" "x" )"1" assert )"1" "1" case "NOT g(n)*x^n=h(m) * x ^ n * (g(n) / h(m))" )"1" assert )nil nil )"2" "2" assert )"2" rewrite "sum_polynomial_eq_degree_eval" )"1" assert )"1" rewrite "poly_eq_le_degree" )"1" "1" "1" "1" assert )"1" expand "+" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )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 ))nil ))nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "poly_divide" )"2" (assert )"2" (expand "make_divtype" )"2" case "%1 = 0" ) (! 3 2 1))"1" (assert ) nil nil )"2" expand "polynomial" 1)"2" rewrite "sigma_restrict_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (induct "i" )"1" (assert ) nil nil )"2" (assert )"2" (skeep)"2" (inst?)"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil )"3" (skeep)"3" (assert )"3" (skeep)"3" (inst - "g" "h" "m" "n" )"3" (inst - "g" "h" "n-m" "m" "n" )"1" (assert )"1" (skeep)"1" (inst - "x" )"1" (inst - "x" )"1" (assert )"1" "ii" "n-m-j" )"1" case "NOT n-m-j-1=ii-1" )"1" (assert ) nil nil )"2" case "ii = 0" )"1" (assert ) nil nil )"2" "2" "2" case "ii<=0" )"1" expand "ii" -1)"1" (assert ) nil nil ))nil )"2" "2" "pd" "poly_divide(g,n)(h,m)(ii-1)" )"1" replace -1)"1" "1" expand "poly_divide" assert ?"1" "1" "1" "1" assert )"1" expand "poly_divide" )"1" nil nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )"1" "1" assert )"1" expand "make_divtype" )"1" "1" assert )"1" rewrite "polynomial_n0" )"1" rewrite "polynomial_n0" )"1" assert )"1" "scal_polynomial" )"1" "(1/h(0))*g" "n" "h(0)" )"1" "1" "x" )"1" expand "const_fun" )"1" expand "*" )"1" "1" rewrite "poly_eq_le_degree" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mz" "2" "mz" )"2" "1" "1" assert )nil nil ))nil )"2" "2" "2" "2" assert )"2" "2" "2" "AA" "%1" )"1" replace "1" expand "make_divtype" "1" replace "1" assert )"1" case "NOT polynomial(AA,ii-2+m)(x) = polynomial(ldt`rem,ldt`rdeg)(x)+polynomial(LAMBDA (jj:nat): IF jj<ii-1 THEN 0 ELSE (-thisterm)*h(jj+1-ii) ENDIF,m+ii-1)(x)" )"1" case "NOT ldt`rdeg = m+ii-1" )"1" expand "ldt" "1" expand "poly_divide" "1" expand "make_divtype" "1" "mz" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" rewrite "sum_polynomial_eq_degree_eval" )"1" "polynomial_rec" )"1" "%1" "ii-1+m" "x" )"1" assert )"1" replace "1" "1" expand "+" )"1" case "NOT ldt`rem(ii - 1 + m) * x ^ (ii - 1 + m) = -(h(m) * x ^ (ii - 1 + m)) * (-thisterm)" )"1" "1" assert )nil nil ))nil )"2" "2" assert )"2" case "FORALL (bb,aa:real): bb+-aa+aa = bb" )"1" "%1" "%2" )"1" "1" rewrite "poly_eq_le_degree" )"1" "1" "1" expand "AA" "1" "ii!1" )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" replace "2" assert )"2" "BB" "%1" )"2" replace "2" case "NOT FORALL (jj:nat): polynomial(BB,ii-1+jj)(x) = (-thisterm)*x^(ii-1)*polynomial(h,jj)(x)" )"1" "jj" )"1" assert )"1" rewrite "polynomial_n0" )"1" assert )"1" rewrite "polynomial_rec" "1" case "NOT %1 = %2" )"1" expand "BB" "1" nil nil ))nil )"2" "2" assert )"2" expand "polynomial" "2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "BB" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "ii = 1" )"1" "1" assert )"1" rewrite "polynomial_n0" )"1" assert )"1" expand "BB" "1" case "x^0 = 1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" rewrite "polynomial_rec" "2" replace "2" "polynomial_rec" )"2" "h" "1+j!1" "x" )"2" assert )"2" "2" assert )"2" "expt_plus" )"2" case "NOT x ^ (ii - 1) * x ^ (1 + j!1) = x^(ii+j!1)" )"1" case "x/=0" )"1" "ii-1" "1+j!1" "x" )"1" assert )nil nil ))nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "BB" "2" assert )"2" "2" "h(1+j!1)*(-thisterm)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "m" )"2" "2" case "NOT polynomial(ldt`quot WITH [(ii - 1) := thisterm], n - m)(x) + (-thisterm)*x^(ii-1) = polynomial(ldt`quot,n-m)(x)" )"1" "RD" "LAMBDA (k:nat): IF k=ii-1 THEN -thisterm ELSE 0 endif" )"1" case "NOT polynomial(RD,n-m)(x) = (-thisterm)*x^(ii-1)" )"1" case "NOT n-m >=ii-1" )"1" assert )nil nil )"2" "2" expand "polynomial" )"2" "sigma_eq_one_arg" )"2" "2" "ii-1" )"2" assert )"2" "1" "1" expand "RD" )"1" nil nil ))nil ))nil )"2" "2" "2" expand "RD" )"2" "2" nil nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "RD" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sum_polynomial_eq_degree_eval" )"2" rewrite "poly_eq_le_degree" )"2" "2" "2" expand "+" )"2" expand "RD" "2" "2" "2" "-thisterm+thisterm=0" )"1" "1" expand "ldt" "1" "1" case "FORALL (kk:nat): kk<=n-m AND n-m-kk > ii-1 IMPLIES poly_divide(g,n)(h,m)(n-m-kk)`quot(ii-1)=0" )"1" "(n-m)-ii" )"1" assert )nil nil ))nil )"2" "2" "kk" )"1" assert )"1" expand "poly_divide" "1" expand "make_divtype" "1" "mz" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "poly_divide" "2" expand "make_divtype" "2" "mz" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT ldt`qdeg = n-m" )"1" expand "ldt" "1" expand "poly_divide" "1" expand "make_divtype" "1" nil nil ))nil ))nil ))nil )"2" "mz" )"2" assert )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )nil defined_types nil )nil naturalnumbers nil )"nat" polynomial_division nil )"nat" polynomial_division nil )"posint" nil )"int" polynomial_division nil )"[nat -> real]" polynomial_division nil )"[nat -> real]" polynomial_division nil )"odd_int" integersnil )nil exponentiation nil )nil extra_real_props nil )nil reals nil )"real" polynomial_division nil )"nzreal" exponentiation nil )"nzrat" rationalsnil )"nat" exponentiation nil )"nat" exponentiation nil )"DivType" polynomial_division nil )"[nat -> real]" polynomial_division nil )"real" reals nil )"posint" nil )"[numfield -> numfield]" number_fields nil )"even_int" integersnil )"nat" polynomial_division nil )"nat" polynomial_division nil )"(strict_total_order?[real])" real_props nil )"real" exponentiation nil )"real" exponentiation nil )"[T -> real]" real_fun_ops "reals/" )nil polynomials "reals/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[T -> real]" real_fun_ops "reals/" )nil polynomials "reals/" )"[T -> real]" real_fun_ops "reals/" )nil polynomials "reals/" )"nzreal" nil )"real" reals nil )"real" reals nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil polynomials "reals/" )"nat" polynomial_division nil )"nat" polynomial_division nil )nil integers nil )nil integers nil )nil polynomials "reals/" )nil polynomials"reals/" )"[T -> real]" real_fun_ops "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"odd_int" integers nil )"even_int" integersnil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"(total_order?[real])" nil )"real" reals nil )"real" sigma "reals/" )"DivType" polynomial_division nil )"nat" polynomial_division nil )"nat" polynomial_division nil )"nat" polynomial_division nil )"(total_order?[real])" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil polynomial_division nil )"[T, T -> boolean]" equalities nil )"[real -> real]" polynomials "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"DivType" polynomial_division nil ))nil 3582556619"" (skeep)"" (skoletin 2)"" (flatten)"" (case "m = 0" )"1" (assert )"1" (hide 2)"1" (expand "poly_divide" )"1" (assert )"1" (replaces -1)"1" (assert )"1" (expand "make_divtype" )"1" (replaces -1) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (assert )"2" (case "m<=n" )"1" (expand "poly_divide" )"1" (expand "make_divtype" )"1" (replaces -2) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert )"2" (expand "poly_divide" )"2" (expand "make_divtype" )"2" (replaces -1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )nil polynomial_division nil )"[T, T -> boolean]" equalities nil )"DivType" polynomial_division nil )"bool" reals nil ) (> const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"nzreal" nil )"DivType" polynomial_division nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil ))nil 3583064979"" (skeep)"" (skoletin 2)"" (expand "poly_divide" :assert ? none)"" (expand "make_divtype" )"" (lift-if)"" (assert )"" (split -)"1" (ground) nil nil )"2" (flatten)"2" (split -)"1" (flatten)"1" (replace -1) (("1" (assert ) nil nil )) nil ))nil )"2" (flatten)"2" (replaces -1)"2" (assert )"2" (split -)"1" (flatten)"1" "1" (assert ) nil nil ))nil ))nil )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )"[bool, bool -> bool]" booleans nil )nil polynomial_division nil )"[T, T -> boolean]" equalities nil )"DivType" polynomial_division nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"DivType" polynomial_division nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"nzreal" nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.95 Sekunden
(vorverarbeitet am 2026-04-29)
¤ *© Formatika GbR, Deutschland
2026-05-26
