Impressum more_polynomial_props.prf
Sprache: Lisp
(more_polynomial_propsnil 3591712357"" (induct "n" )"1" (assert )"1" (skeep)"1" (inst + "0" )"1" (assert )"1" (split +)"1" (grind) nil nil )"2" (skeep) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "n" )"2" (flatten)"2" (skeep)"2" (inst - "a" )"2" (assert )"2" case " ((EXISTS (x): polynomial(a, 1+n)(x) /= 0) AND ") "1" (hide -3)"1" (split -)"1" (flatten)"1" (case "a(1+n) = 0" )"1" (skosimp*)"1" (inst + "i!1" )"1" (assert )"1" "1" "1" "j" )"1" (assert ) nil nil ))nil ))nil )"2" "2" replace -2 :dir rl)"2" "2" expand "polynomial" 1)"2" expand "sigma" + 1)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "1+n" )"2" (assert )"2" (skosimp*) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case "a(1+n) /= 0" )"1" (flatten)"1" (inst 4 "1+n" )"1" (assert )"1" (skosimp*) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp*)"2" (inst + "x!1" )"2" (flatten)"2" rewrite "polynomial_rec" 2)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (ground)"1" (lemma "polynomial_eq_coeff" )"1" (inst - "a" "LAMBDA (ii:nat): 0" "1+n" )"1" (flatten)"1" (hide -2)"1" (split -)"1" "1" (inst - "i!1" ) nil nil ))nil )"2" "2" "x!1" )"2" "2" "2" expand "polynomial" )"2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "polynomial" )"2" (rewrite "sigma_restrict_eq_0" )"2" (skosimp*)"2" (inst + "i!1" )"2" "2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )nil polynomials nil )NOT const-decl "[bool -> bool]" booleans nil )nil sigma nil )nil sigma nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )nil polynomials nil )"real" reals nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"real" sigma nil )"real" exponentiation nil )"real" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )"[real -> real]" polynomials nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil sequences nil )nil defined_types 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 ))nil 3587828917 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3587828917 ("" (subtype-tcc) nil nil )"real" reals 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 )nil real_types nil )"bool" reals nil )nil real_types nil )"odd_int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"{j: nonneg_int | j >= i}" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"boolean" notequal nil ))nil ))nil 3587828907"" (lemma "poly_continuous" )"" (skeep)"" (inst - "poly_deriv(a)" "pn-1" "y" "epsil" )"" (assert )"" (skeep -1)"" (inst + "delta" )"" (skeep)"" (lemma "poly_mean_value" )"" (case "x < y" )"1" (inst - "a" "pn" "x" "y" )"1" (assert )"1" (skeep -)"1" case "%1 = %2" ) (! -4 2)"1" (replace -1)"1" replace -5 :dir rl)"1" "cc" )"1" "1" (propax) nil nil )"2" expand "abs" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) (("2" (field) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "a" "pn" "y" "x" )"2" (assert )"2" (skeep -1)"2" (replace -3 :dir rl)"2" (inst - "cc" )"2" "1" (propax) nil nil )"2" expand "abs" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )nil polynomials nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"[numfield, numfield -> numfield]" number_fields nil )"real" more_polynomial_props nil )"real" more_polynomial_props nil )nil reals nil )nil real_props nil )"real" reals nil )nil real_props nil )"odd_int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[real -> real]" polynomials nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil real_types nil )nil real_types nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" polynomials nil )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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"int" integers nil )"(total_order?[real])" nil )nil polynomials nil ))nil )nil 3587821660"" "PQ" "LAMBDA (a:sequence[real],ki:nat): (FORALL (y: real, epsil: posreal): AND x /= y IMPLIES") "1" (case "FORALL (a:sequence[real],ki:nat): PQ(a,ki)" )"1" (skeep)"1" (inst - "a" "pn-1" )"1" (expand "PQ" -1)"1" (assert ) (("1" (inst - "y" "epsil" ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" case "FORALL (kc:real,nm:nat,ki:nat): (LET apow = (LAMBDA (ii:nat): IF ii = nm THEN kc ELSE 0 ENDIF) IN PQ(apow,ki))" )"1" (induct "ki" 1)"1" (hide -)"1" (skeep)"1" (expand "PQ" )"1" (skeep)"1" (case "a(1) = 0" )"1" (inst + "1" )"1" (skeep)"1" (expand "polynomial" +)"1" (expand "sigma" )"1" expand "sigma" )"1" expand "sigma" )"1" replace -1)"1" assert )"1" expand "poly_deriv" )"1" "1" assert )"1" expand "abs" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "epsil/abs(a(1))" )"1" (skeep)"1" (expand "polynomial" +)"1" (expand "sigma" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "poly_deriv" )"1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" case "a(1)*(x-y)/(x-y) = a(1)" )"1" replace -1)"1" assert )"1" expand "abs" +)"1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (split)"1" (cross-mult 1) nil nil )"2" (cross-mult 1) nil nil ))nil )"3" (expand "abs" )"3" (lift-if) (("3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (inst - "a(j+2)" "j+2" "j+1" )"2" (skoletin -2)"2" (inst - "a" )"2" (expand "PQ" (-1 -3 1))"2" (skeep)"2" (inst - "y" "epsil/2" )"2" (inst - "y" "epsil/2" )"2" "2" "min(delta!1,delta!2)" )"2" "2" "x" )"2" "x" )"2" assert )"2" case "FORALL (xy:real): polynomial(a,2+j)(xy) = polynomial(a,1+j)(xy) + polynomial(apow,2+j)(xy)" )"1" rewrite -1)"1" rewrite -1)"1" "1" case "FORALL (xy:real): polynomial(poly_deriv(a),1+j)(xy) = polynomial(poly_deriv(a),j)(xy) + polynomial(poly_deriv(apow),1+j)(xy)" )"1" rewrite -1)"1" "1" expand "abs" "1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "polynomial" )"2" expand "sigma" "2" expand "sigma" )"2" case "%1 = 0" )"1" "1" assert )"1" expand "poly_deriv" )"1" expand "apow" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" expand "poly_deriv" )"2" expand "apow" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "polynomial" )"2" expand "sigma" "2" expand "sigma" )"2" case "%1 = 0" )"1" "1" expand "apow" )"1" nil nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "apow" )"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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "(FORALL (y: real, epsil: posreal,nm:posnat,kc:real): AND x /= y IMPLIES") "1" (skeep)"1" (case "nm = 0" )"1" (replaces -1)"1" (assert )"1" (hide-all-but 1)"1" (expand "PQ" )"1" (skeep)"1" (inst + "1" )"1" (skeep)"1" expand "poly_deriv" )"1" expand "polynomial" + 1)"1" rewrite "sigma_restrict_eq_0" )"1" assert )"1" case "%1 = 0" )"1" "1" expand "abs" )"1" (assert ) nil nil ))nil ))nil )"2" "2" expand "polynomial" )"2" rewrite "sigma_minus" )"2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "nmzero" 1)"2" (hide (-2 3))"2" (skoletin 2)"2" (expand "PQ" 1)"2" (skeep)"2" (inst - "y" "epsil" "nm" "kc" )"1" (skeep -2)"1" "delta" )"1" "1" "x" )"1" assert )"1" case "1+ki<nm" )"1" case "%1 = 0" )"1" "1" expand "abs" +)"1" (assert ) nil nil ))nil ))nil )"2" "2" case "%1 = 0" )"1" case "%1 = 0" )"1" (assert ) nil nil )"2" case "%1 = 0" )"1" assert )nil nil )"2" case "%1 = 0" )"1" case "%1 = 0" )"1" assert )nil nil )"2" expand "polynomial" "2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "apow" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "polynomial" "2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "apow" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "polynomial" 1)"2" expand "poly_deriv" "2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "apow" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "polynomial(poly_deriv(apow), ki)(y) = y ^ (nm - 1) * kc * nm" )"1" case "FORALL (xy:real): polynomial(apow, 1 + ki)(xy) = kc * xy ^ nm" )"1" "x" )"1" "y" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" expand "polynomial" "2" "sigma_eq_one_arg" )"2" "nm" )"2" "2" assert )"2" "1" expand "apow" "1" nil nil ))nil )"2" "2" expand "apow" "2" "2" nil nil ))nil ))nil ))nil )"3" "3" expand "apow" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "polynomial" 1)"2" "sigma_eq_one_arg" )"2" "nm-1" )"2" "2" assert )"2" "1" "1" expand "poly_deriv" "1" expand "apow" "1" "1" "1" "1" expand "^" )"1" expand "expt" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "poly_deriv" "2" expand "apow" "2" nil nil ))nil ))nil ))nil )"3" "3" expand "poly_deriv" "3" expand "apow" "3" 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 )"2" (hide-all-but 1)"2" case "(FORALL (y: real, epsil: posreal, nm: posnat, kc: real): AND x /= y IMPLIES") "1" (skeep)"1" (case "kc = 0" )"1" (replaces -1)"1" (assert )"1" (expand "abs" +) (("1" (propax) nil nil ))nil ))nil ))nil )"2" (case "NOT abs(kc)>0" )"1" (expand "abs" 1)"1" (lift-if) (("1" (ground) nil nil )) nil ))nil )"2" (inst - "y" "epsil/abs(kc)" "nm" "kc" )"1" (skeep -2)"1" (inst + "delta" )"1" (skeep)"1" "x" )"1" assert )"1" "1" rewrite "abs_mult" :dir rl)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (split)"1" (cross-mult 1) nil nil )"2" (cross-mult 1) nil nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "binomial_theorem" )"2" (skeep) (("2" (postpone) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil )nil shostak))nil 3587829356 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"real" reals nil ))nil ))nil 3587829358"" (skeep)"" (case "NOT FORALL (RR:real): RR=0 IFF (RR>=0 AND RR<=0)" )"1" (skosimp*) (("1" (ground) nil nil )) nil )"2" (rewrite -1 1)"2" (hide -1)"2" (split +)"1" (lemma "poly_deriv_limit" )"1" "eppy" "-polynomial(poly_deriv(a), pn - 1)(y)/2" )"1" (inst - "a" "y" "eppy" "pn" )"1" (skeep -2)"1" case "NOT FORALL (x:real): abs(x-y)<delta AND x/=y IMPLIES (polynomial(a, pn)(x) - polynomial(a, pn)(y)) / (x - y) < 0" )"1" (skeep)"1" (inst - "x" )"1" (assert )"1" (expand "abs" -3)"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (name "xy" "y + min(delta,epsil)/2" )"2" (inst - "xy" )"2" (assert )"2" (split -)"1" "1" assert )"1" "xy" )"1" "1" (assert ) nil nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "poly_deriv_limit" )"2" "eppy" "polynomial(poly_deriv(a), pn - 1)(y)/2" )"2" (inst - "a" "y" "eppy" "pn" )"1" (skeep -2)"1" case "NOT FORALL (x:real): abs(x-y)<delta AND x/=y IMPLIES (polynomial(a, pn)(x) - polynomial(a, pn)(y)) / (x - y) > 0" )"1" (skeep)"1" (inst - "x" )"1" (assert )"1" (expand "abs" -3)"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (name "xy" "y - min(delta,epsil)/2" )"2" (inst - "xy" )"2" (assert )"2" (split -)"1" "1" "xy" )"1" "1" (assert ) nil nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil ) (>= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans 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 )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" more_polynomial_props nil )nil real_types nil )nil real_types nil )nil extra_real_props nil )nil more_polynomial_props nil )"(strict_total_order?[real])" real_props nil )"real" more_polynomial_props nil )nil real_types nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil real_props nil )"posreal" nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" polynomials nil )"[real -> real]" polynomials nil )nil sequences nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"int" integers nil )"real" reals nil ))nil 3587832241 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"real" reals nil ))nil ))nil 3587832242"" (skeep)"" (lemma "square_free_min" )"" (inst - "-a" "epsil" "y" "-c" "pn" )"" (assert )"" (split -)"1" (hide-all-but (-1 1))"1" (case "NOT poly_deriv(-a) = (-1)*poly_deriv(a)" )"1" (expand "poly_deriv" 1)"1" (decompose-equality 1)"1" (hide-all-but 1) (("1" (grind) nil nil ))nil ))nil ))nil )"2" (replaces -1)"2" (lemma "scal_polynomial" )"2" (expand "const_fun" )"2" (expand "*" )"2" (inst - _ _ "-1" )"2" (inst - "poly_deriv(a)" "pn-1" )"2" (decompose-equality -1)"2" "y" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (replace -1 1 :dir rl)"2" (hide -1)"2" (expand "polynomial" )"2" (case "FORALL (ccc:real): -ccc = (-1)*ccc" )"1" (rewrite -1 1)"1" (rewrite "sigma_scal" :dir rl)"1" (rewrite "sigma_eq" )"1" (skosimp*) (("1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (hide (-1 2))"3" (skeep)"3" (inst - "x" )"3" (assert )"3" case "(-1)*polynomial(-a, pn)(x) = polynomial(a,pn)(x)" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (expand "polynomial" )"2" (rewrite "sigma_scal" :dir rl)"2" (rewrite "sigma_eq" )"2" "2" "2" (grind :exclude "^" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil more_polynomial_props nil )"int" integers nil )nil sigma nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (T_low type-eq-decl nil sigma nil )nil sigma nil )"real" sigma nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"boolean" notequal nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops nil )"[bool, bool -> bool]" booleans nil )"[real -> real]" polynomials nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops nil )nil polynomials nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops nil )"real" polynomials nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )nil integers nil )nil integers nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T -> real]" real_fun_ops nil )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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil ))nil 3589548521 ("" (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 )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3589548523"" (skeep)"" (decompose-equality 1)"" (name "j" "x!1" )"" (replace -1)"" (hide -1)"" (expand "poly_deriv" )"" (expand "poly_shift" )"" (rewrite "sigma_scal_right" 1 :dir rl)"1" (rewrite "sigma_sum" )"1" (rewrite "sigma_shift_fun_eq" )"1" (hide 2)"1" (skosimp*)"1" (assert )"1" (factor 1)"1" " binom_absorption" )"1" "1+j" "1+i!1+j" )"1" assert )"1" replace -1 +)"1" "1" "i!1" )"1" (field) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"nat" more_polynomial_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sequences nil )"real" polynomials nil )"sequence[real]" polynomials 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 )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"posint" nil )nil sigma nil )IF const-decl "[boolean, T, T -> T]" if_def nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil integers nil )nil integers nil )"posnat" binomial nil )"boolean" notequal nil )"real" exponentiation nil )nil sigma nil )nil sigma nil )"real" reals nil )nil sigma nil )"int" integers nil )nil integers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"odd_int" integersnil )"even_int" integersnil )"real" reals nil )"rat" rationals nil )nil integers nil )"rat" rationals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"rat" rationals nil )nil binomial_identities nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sigma nil )"real" reals nil )"[T, T -> boolean]" equalities nil ))nil 3589549521"" (subtype-tcc) nil nil ) ((/= const-decl "boolean" notequal nil ))nil ))nil 3589549523"" (skeep)"" (lemma "power_linear_polynomial" )"" (inst + "power_linear(-y,1,m)" )"" (assert )"" (split +)"1" (expand "power_linear" 1)"1" (assert )"1" (expand "C" 1)"1" (assert )"1" (expand "^" 1)"1" (lemma "expt_1n_aux" )"1" (inst?)"1" (assert )"1" (replace -1)"1" expand "expt" +)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -) (("2" (grind) nil nil )) nil )"3" (skeep) (("3" (inst?) (("3" (assert ) nil nil )) nil ))nil )"4" (lemma "deriv_power_linear" )"4" (skeep)"4" (inst?)"4" (replace -1)"4" (expand "max" )"4" (assert )"4" (rewrite "scal_polynomial2" )"4" (inst?) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil polynomials nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil polynomials nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil polynomials nil )"int" integers nil )"(total_order?[real])" nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"posnat" factorial "ints/" )"nonneg_int" nil )"posnat" binomial nil )"real" exponentiation nil )"posrat" nil )"real" exponentiation nil )"posnat" exponentiation nil )nil exponentiation nil )nil factorial "ints/" )"posrat" nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" exponentiation nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"real" polynomials nil )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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil 3591538151"" (skeep)"" (lemma "polynomial_prod_def" )"" case "NOT polynomial(a,n) = polynomial(polynomial_prod(b,m,g,p),m+p)" )"1" (hide 5)"1" (decompose-equality +)"1" (inst - "b" "g" "p" "m" "x!1" )"1" (inst - "x!1" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (case "m+p < n" )"1" case "polynomial(a, n) = polynomial(polynomial_prod(b, m, g, p), n)" )"1" (lemma "polynomial_eq_coeff" )"1" (inst?)"1" (assert )"1" (inst - "n" )"1" (expand "polynomial_prod" -1)"1" (expand "max" -1)"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -2 +)"2" (expand "polynomial" 1)"2" (decompose-equality +)"2" (lemma "sigma_split" )"2" (inst - _ "n" "0" "m+p" )"2" (inst?)"2" (assert )"2" (replaces -1 +)"2" (assert )"2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "polynomial_prod" 1)"2" expand "max" )"2" expand "sigma" +)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "polynomial_eq_coeff" )"2" "LAMBDA (i:nat): IF i<=n THEN a(i) ELSE 0 ENDIF" "polynomial_prod(b,m,g,p)" "m+p" )"2" (case "m + p > n" )"1" (assert )"1" (replace -3 :dir rl)"1" (flatten)"1" (hide -3)"1" (splash -2)"1" (inst - "m+p" )"1" assert )"1" expand "polynomial_prod" -1)"1" expand "max" -1)"1" expand "sigma" -1)"1" expand "sigma" -1)"1" "nzreal_times_nzreal_is_nzreal" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sigma_split" )"2" "PG" "%1" ) (! 1 2))"2" replace -1)"2" "2" expand "polynomial" 1)"2" "m+p" "0" "n" )"2" "2" assert )"2" "2" case "%1 = 0" )"1" "1" assert )"1" expand "PG" +)"1" expand "polynomial" "1" rewrite "sigma_eq" )nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "m+p = n" )"1" (replace -1 :dir rl)"1" (assert )"1" (hide -2)"1" (lemma "polynomial_eq_coeff" )"1" "1" assert )"1" "1" (inst - "i" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil polynomials nil )"bool" reals nil )"(total_order?[real])" nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma nil )nil sigma nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"boolean" notequal nil )"real" exponentiation nil )"posint" nil )"odd_int" integersnil )"real" reals nil )nil sigma nil )"[bool, bool -> bool]" booleans nil )nil sigma nil )nil polynomials nil )"(strict_total_order?[real])" real_props nil )"real" sigma nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" reals nil )nil naturalnumbers nil )"(total_order?[real])" nil )"bool" reals nil )"[real -> real]" more_polynomial_props nil )nil sigma nil )nil real_types nil )nil reals nil )"(strict_total_order?[real])" real_props nil )"nat" more_polynomial_props nil )"nat" more_polynomial_props nil )"nat" more_polynomial_props nil )"real" reals nil )"nonneg_int" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"[real -> real]" polynomials nil )"real" polynomials nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3591543095"" (subtype-tcc) nil nil ) ((/= const-decl "boolean" notequal nil ))nil ))nil 3591543097"" (skeep)"" (case "k = 0" )"1" (replaces -1)"1" (assert )"1" (expand "^" )"1" (expand "expt" )"1" (assert )"1" (case "m > n" )"1" "aa" "LAMBDA (i:nat): IF i<=n THEN a(i) ELSE 0 ENDIF" )"1" (lemma "polynomial_eq_coeff" )"1" (inst - "aa" "b" "m" )"1" (assert )"1" (flatten)"1" (hide -2)"1" "1" "m" )"1" expand "aa" -1)"1" (assert ) nil nil ))nil ))nil )"2" "2" "x!1" )"2" replace -3 :dir rl)"2" expand "polynomial" 1 1)"2" "sigma_split" )"2" "m" "0" "n" )"2" "2" assert )"2" "2" case "%1 = 0" )"1" "1" assert )"1" expand "polynomial" "1" rewrite "sigma_eq" )"1" "1" expand "aa" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "aa" "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" (case "n > m" )"1" "bb" "LAMBDA (i:nat): IF i<=m THEN b(i) ELSE 0 ENDIF" )"1" (lemma "polynomial_eq_coeff" )"1" (inst - "a" "bb" "n" )"1" (flatten)"1" (hide -2)"1" "1" "n" )"1" expand "bb" -1)"1" (assert ) nil nil ))nil ))nil )"2" expand "polynomial" + 2)"2" "2" "sigma_split" )"2" "n" "0" "m" )"2" "2" assert )"2" "2" case "%1 = 0" )"1" "1" assert )"1" "x!1" )"1" replace -3 +)"1" assert )"1" expand "polynomial" "1" case "FORALL (diggy:real): 1*diggy=diggy" )"1" rewrite "1" rewrite "sigma_eq" )"1" "1" expand "bb" "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "bb" 1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "NOT m = n" )"1" (assert ) nil nil )"2" (hide (1 2))"2" (replace -1)"2" (assert )"2" "polynomial_eq_coeff" )"2" "a" "b" "n" )"2" "2" "2" "1" (inst - "n" ) nil nil )"2" "2" "x!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" (assert )"2" (lemma "linear_power_is_differentiable" )"2" (inst - "k" "y" )"2" (assert )"2" (skolem -1 "G" )"2" (flatten)"2" (lemma "polynomial_prod_degrees" )"2" (inst - "a" "G" "b" "n" "k" "m" )"2" (assert )"2" (split -)"1" (flatten)"1" (assert )"1" "n" )"1" assert )"1" replace -2 4)"1" expand "polynomial_prod" +)"1" expand "max" +)"1" expand "sigma" +)"1" expand "sigma" +)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst -5 "x!1" )"2" replace -5 +)"2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" exponentiation nil )"bool" reals nil )nil polynomials nil )"(strict_total_order?[real])" real_props nil )"[real -> real]" polynomials nil )nil sigma nil )"real" reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sigma nil )nil sigma nil )"real" reals nil )"posint" nil )"real" sigma nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma nil )nil sigma nil )"(total_order?[real])" nil )nil naturalnumbers nil )"[nat -> real]" more_polynomial_props nil )nil sequences nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(total_order?[real])" nil )"[nat -> real]" more_polynomial_props nil )"real" exponentiation nil )nil nil )"nonneg_int" nil )"real" polynomials nil )"int" integers nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" reals nil )nil more_polynomial_propsnil ))nil 3592659204"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"real" reals nil ))nil ))nil 3592659204"" (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 )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"real" polynomials nil )"real" reals nil )"int" integers nil )"real" reals nil ))nil ))nil 3592659205"" case "FORALL (a: sequence[real], n: nat, x, y: real): AND AND AND AND AND OR AND polynomial(a,n)(x)<0") "1" (skeep)"1" (case "polynomial(a,n)(x)<0" )"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (inst - "-a" "n" "x" "y" )"2" (assert )"2" (rewrite "neg_polynomial" :dir rl)"2" (assert )"2" (case "poly_deriv(-a) = -poly_deriv(a)" )"1" (replace -1)"1" (rewrite "neg_polynomial" :dir rl)"1" (assert )"1" (expand "-" )"1" (assert )"1" (case "polynomial(a,n)(x)=0" )"1" "1" "x" )"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "1" expand "sign_ext" (-1 +))"1" "1" (ground) nil nil ))nil ))nil )"2" "2" "z" )"2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (decompose-equality) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "sign_ext" +)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (assert )"2" case "polynomial(poly_deriv(a), n - 1)(x) = 0" )"1" (inst - "x" ) (("1" (assert ) nil nil )) nil )"2" (assert )"2" case "polynomial(poly_deriv(a), n - 1)(x) >=0" )"1" (ground) nil nil )"2" (hide (2 3))"2" (lemma "poly_decreasing" )"2" "a" "n" "x" "y" )"2" assert )"2" "2" "poly_intermediate_value_inc" )"2" "poly_deriv(a)" "0" "n-1" "x" "c" )"2" assert )"2" "2" "cc!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (hide 2) (("4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil )nil polynomials nil )nil polynomials nil )"[T -> real]" real_fun_ops nil )nil polynomials nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"posint" nil )"posint" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans 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 )"bool" reals nil ) (< const-decl "bool" reals nil )"[T, T -> boolean]" equalities nil )"[real -> real]" polynomials nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" polynomials nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" nil ))nil 3592664083"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"real" reals nil ))nil ))nil 3592664083"" (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 )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"real" polynomials nil )"real" reals nil )"int" integers nil )"real" reals nil ))nil ))nil 3592664088"" case "FORALL (a: sequence[real], n: nat, x, y: real): AND AND AND AND AND OR AND ") "1" (skeep)"1" (case "polynomial(a,n)(x)>0" )"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (inst - "-a" "n" "x" "y" )"2" (assert )"2" (rewrite "neg_polynomial" :dir rl)"2" (assert )"2" (case "poly_deriv(-a) = -poly_deriv(a)" )"1" (replace -1)"1" (rewrite "neg_polynomial" :dir rl)"1" (assert )"1" (expand "-" )"1" (assert )"1" (case "polynomial(a,n)(x)=0" )"1" "1" "x" )"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "1" expand "sign_ext" (-1 +))"1" "1" (ground) nil nil ))nil ))nil )"2" "2" "z" )"2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (decompose-equality) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "sign_ext" +)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (lift-if)"2" (assert )"2" case "polynomial(poly_deriv(a), n - 1)(x) = 0" )"1" (inst - "x" ) (("1" (assert ) nil nil )) nil )"2" (assert )"2" case "polynomial(poly_deriv(a), n - 1)(x) >=0" )"1" (ground) nil nil )"2" (hide (2 3))"2" (lemma "poly_decreasing" )"2" "a" "n" "y" "x" )"2" assert )"2" "2" "poly_intermediate_value_dec" )"2" "poly_deriv(a)" "0" "n-1" "c" "x" )"2" assert )"2" "2" "cc!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (hide 2) (("4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil )nil polynomials nil )nil polynomials nil )"[T -> real]" real_fun_ops nil )nil polynomials nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"real" reals nil )"posint" nil )"posint" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans 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 )nil sequences nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"[real -> real]" polynomials nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" polynomials nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" nil ))nil ))nil 3591032268"" (subtype-tcc) nil nil ) ((/= const-decl "boolean" notequal nil ))nil ))nil 3591032268"" (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 )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3591032268"" (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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"int" integers nil )"real" reals nil ))nil ))nil 3591032268"" (subtype-tcc) nil nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"boolean" notequal nil )"real" reals nil )"int" integers nil ))nil ))nil 3591090184"" (skeep)"" (expand "max_linear_div_power?" )"" (ground)"1" (skeep) (("1" (inst + "b" ) (("1" (assert ) nil nil )) nil ))nil )"2" (skeep)"2" (case "n = m" )"1" (replace -1)"1" (assert )"1" (inst + "b" "m*b" )"1" (split +)"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (skeep)"3" (lemma "linear_power_is_differentiable" )"3" (inst - "m" "y" )"3" (assert )"3" (skolem -1 "g" )"3" "3" "3" case "FORALL (j:nat): j<=m IMPLIES a(j)=g(j)*b(0)" )"1" "x" )"1" case "polynomial(poly_deriv(a),m-1)(x) = polynomial(poly_deriv(g),m-1)(x)*b(0)" )"1" "1" replace -4)"1" expand "polynomial" +)"1" expand "sigma" +)"1" expand "sigma" +)"1" expand "*" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "polynomial" +)"2" rewrite "sigma_scal_right" "2" rewrite "sigma_eq" )"2" "2" "2" expand "poly_deriv" "2" "1+n!1" )"2" assert )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "polynomial_eq_coeff" )"2" "a" "b(0)*g" "m" )"2" assert )"2" "2" "2" "1" "1" "j" )"1" expand "*" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" replace -6 1)"2" expand "polynomial" "2" expand "sigma" "2" expand "sigma" "2" "x!1" )"2" replace "2" rewrite "scal_polynomial2" )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" (inst - "1" )"4" (mult-by 1 "m" )"4" (assert )"4" (expand "polynomial" (-1 1))"4" rewrite "sigma_scal_right" 1 :dir rl)"4" expand "*" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (label "neqm" 1)"2" (hide "neqm" )"2" case "EXISTS (q:[nat->real]): FORALL (x:real): polynomial(q,n-m)(x) = (x-y)^1*polynomial(poly_deriv(b),n-m-1)(x) + m*polynomial(b,n-m)(x)" )"1" (skeep)"1" case "FORALL (x): ") "1" (inst + "b" "q" )"1" (assert )"1" (split +)"1" (propax) nil nil )"2" (propax) nil nil )"3" (assert )"3" "y" )"3" assert )"3" assert )"3" replace -2 +)"3" "1" )"3" "3" "m" )"3" assert )"3" expand "^" -1)"3" expand "expt" -1)"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (lemma "linear_power_is_differentiable" )"2" (inst - "m" "y" )"2" (assert )"2" "z" )"2" "2" "2" assert )"2" case "NOT polynomial(poly_deriv(a),n-1) = polynomial(poly_deriv(polynomial_prod(z,m,b,n-m)),n-1)" )"1" case "NOT polynomial(poly_deriv(LAMBDA (i:nat): IF i>n THEN 0 ELSE a(i) ENDIF),n-1) = polynomial(poly_deriv(polynomial_prod(z,m,b,n-m)),n-1)" )"1" "1" "aq" "%1" )"1" replace -1)"1" case "aq = polynomial_prod(z, m, b, n - m)" )"1" assert )nil nil )"2" "polynomial_eq_coeff" )"2" "aq" "polynomial_prod(z, m, b, n - m)" "n" )"2" "2" "2" "1" "1" case "x!1 > n" )"1" expand "aq" "1" assert )"1" expand "polynomial_prod" "1" expand "max" )"1" assert )"1" expand "sigma" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" rewrite "polynomial_prod_def" "2" "x!1" )"2" "x!1" )"2" assert )"2" replace "2" replace "2" expand "polynomial" "2" rewrite "sigma_restrict_eq" )"2" "2" expand "restrict" )"2" "2" expand "aq" )"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 )"2" replace -1 1 :dir rl)"2" "2" expand "polynomial" 1)"2" rewrite "sigma_restrict_eq" )"2" "2" "2" expand "restrict" )"2" expand "poly_deriv" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" " poly_product_rule" )"2" "2" "2" "x" )"2" assert )"2" "neqm" )"2" assert )"2" replace "2" replace "2" "x" )"2" "x" )"2" replace "2" replace "2" "x" )"2" replace "2" assert )"2" "expt_plus" )"2" "m-1" "1" "x-y" )"1" assert )nil nil )"2" "2" replace "2" expand "^" "2" expand "expt" "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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide 3)"2" "DIGG" "LAMBDA (ii:nat): IF ii = n-m THEN poly_deriv(b)(n-m-1) + m*b(n-m) ELSIF ii>0 THEN poly_deriv(b)(ii-1) - y*poly_deriv(b)(ii) + m*b(ii) ELSE -y*poly_deriv(b)(0) + m*b(0) ENDIF" )"1" (inst + "DIGG" )"1" (skeep)"1" "IP" "LAMBDA (i:nat): IF i = 1 THEN 1 ELSIF i = 0 THEN -y ELSE 0 ENDIF" )"1" case "x-y = polynomial(IP,1)(x)" )"1" replace -1 1)"1" expand "^" 1)"1" expand "expt" 1)"1" expand "expt" 1)"1" rewrite "polynomial_prod_def" )"1" rewrite "scal_polynomial2" "1" expand "polynomial" 1)"1" rewrite "sigma_sum" )"1" rewrite "sigma_restrict_eq" )"1" "1" "1" expand "restrict" )"1" "1" assert )"1" "1" nil nil )"2" "2" case "DIGG(x!1) = ") "1" assert )nil nil )"2" "2" "2" expand "DIGG" "2" expand "polynomial_prod" )"2" expand "max" )"2" assert )"2" case "x!1 = 0" )"1" "1" assert )"1" "sigma_eq_one_arg" )"1" "1" "0" )"1" assert )"1" "1" replace "1" expand "IP" "1" expand "*" )"1" "neqm" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "neqm" )"2" assert )nil nil ))nil )"3" nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" "2" "1" "1" "1" assert )"1" expand "sigma" "1" expand "sigma" "1" expand "IP" "1" expand "*" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" rewrite "sigma_reverse" "1" expand "sigma" "1" expand "sigma" "1" assert )"1" case "NOT %1 = 0" )"1" "1" rewrite "sigma_restrict_eq_0" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "IP" "2" expand "*" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )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 )"3" "neqm" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "neqm" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "neqm" )"2" assert )"2" expand "IP" 2)"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*)"3" (assert )"3" (reveal "neqm" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (reveal "neqm" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" more_polynomial_props nil )"nat" exponentiation nil )"real" exponentiation nil )"nat" exponentiation nil )nil polynomials nil )nil exponentiation nil )nil reals nil )"real" more_polynomial_props nil )"real" more_polynomial_props nil )"nonneg_int" nil )nil sigma nil )"[T -> real]" sigma nil )nil polynomials nil )"nat" more_polynomial_props nil )"nat" more_polynomial_props nil )"[nat -> real]" more_polynomial_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" polynomials nil )"real" reals nil )nil sigma_nat nil )"posint" nil )nil sigma nil )nil sigma nil )"[nat -> real]" more_polynomial_props nil )"odd_int" integersnil )"[nat -> real]" more_polynomial_props nil )nil sigma nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"[T -> real]" real_fun_ops nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil reals nil )nil real_props nil )nil polynomials nil )nil polynomials nil )nil naturalnumbers nil )"posnat" more_polynomial_props nil )"nat" more_polynomial_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil sigma nil )nil sigma nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"int" integers nil )nil sigma nil )"real" sigma nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" polynomials nil )"[real -> real]" polynomials nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sequences nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil nil )"[T, T -> boolean]" equalities nil )nil integers nil )"bool" reals nil )nil integers nil )"int" integers 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 )"(total_order?[real])" nil ))nil )nil 3591089825"" case "NOT FORALL (a: sequence[real], n: nat, y: real): AND polynomial(a, n)(y) = 0 IMPLIESAND FORALL (x):AND polynomial(b, n - m)(y) /= 0)") "1" (hide 2)"1" (induct "n" )"1" (skeep)"1" (expand "polynomial" -1)"1" (expand "sigma" )"1" (expand "sigma" ) (("1" (propax) nil )))))))))"2" (skolem 1 "nn" )"2" (flatten)"2" (skeep)"2" (lemma "polynomial_zero_factor" )"2" (inst - "a" "nn+1" "y" )"2" (assert )"2" (skeep -1)"2" (case "polynomial(g,nn)(y)/=0" )"1" (inst + "g" "1" )"1" (assert )"1" (expand "^" +)"1" expand "expt" +)"1" expand "expt" +)"1" (propax) nil )))))))))))"2" (flatten)"2" (inst - "g" "y" )"2" (assert )"2" case "g(nn)/=0" )"1" assert )"1" "1" "1" assert )"1" "b" "m+1" )"1" assert )"1" "1" "x" )"1" "x" )"1" assert )"1" case "FORALL (rr:real): x*rr-rr*y = (x-y)^1*rr" )"1" rewrite -1)"1" "1" replace "1" assert )"1" "1" assert )"1" replace "1" assert )"1" "expt_plus" )"1" "1" assert )"1" replace "1" assert )nil )))))"2" "2" replace "2" expand "^" "2" expand "expt" "2" nil )))))))))))))))))))))))))))))"2" "2" nil )))))))))))))))))))))))))"2" "2" assert )"2" "polynomial_eq_coeff" )"2" "DIG" "LAMBDA (ii:nat): IF ii = 1+nn THEN g(nn) ELSIF ii>0 THEN g(ii-1) - g(ii)*y ELSE -g(0)*y ENDIF" )"1" "a" "DIG" "1+nn" )"1" "1" "1" "1" "1+nn" )"1" expand "DIG" -1)"1" assert )nil )))))"2" "2" "x!1" )"2" assert )"2" replace -4 1)"2" expand "polynomial" "2" "IG" "LAMBDA (i: nat): g(i) * (IF i = 0 THEN 1 ELSE x!1 ^ i ENDIF)" )"2" replace "2" case "sigma(0,nn,IG)=sigma(0,1+nn,LAMBDA (ii:nat): IF ii=0 THEN 0 ELSE IG(ii-1) ENDIF)" )"1" "x!1" )"1" replace "1" rewrite "sigma_scal_right" "1" rewrite "sigma_scal_right" "1" case "sigma(0, nn, LAMBDA (i: nat): IG(i) * y) = sigma(0, 1+nn, LAMBDA (i: nat): IF i >nn THEN 0 ELSE IG(i) * y ENDIF)" )"1" replace "1" rewrite "sigma_minus" )"1" rewrite "sigma_restrict_eq" )"1" "1" "1" expand "restrict" )"1" "1" assert )"1" "1" expand "DIG" "1" assert )"1" expand "IG" "1" assert )nil )))))))"2" "2" assert )"2" "1" case "NOT x!2 = 1+nn" )"1" assert )nil )"2" replace "2" assert )"2" expand "DIG" "2" expand "IG" "2" "2" assert )nil )))))))))))))"2" expand "IG" "2" expand "DIG" "2" "2" assert )"2" "1" replace "1" expand "^" "1" expand "expt" "1" expand "expt" "1" nil )))))))))"2" "expt_plus" )"2" "x!2-1" "1" "x!1" )"1" assert )"1" replace "1" expand "^" "1" expand "expt" "1" expand "expt" "1" assert )nil )))))))))))"2" assert )"2" "2" replace "2" expand "^" "2" expand "expt" "2" nil )))))))))))))))))))))))))))))))))))))))"2" "2" assert )nil )))))))))))))"2" "2" expand "sigma" "2" rewrite "sigma_restrict_eq" )"2" "2" expand "restrict" )"2" nil )))))))))))))))))))"2" "2" assert )nil )))))"2" case "FORALL (k:nat): k<=nn IMPLIES sigma(0, k, IG) = LAMBDA (ii: nat): IF ii = 0 THEN 0 ELSE IG(ii - 1) ENDIF)") "1" "1" assert )nil )))"2" "k" )"1" assert )"1" "1" expand "IG" )"1" nil )))))))"2" "2" assert )"2" expand "sigma" "2" nil )))))))"3" "3" assert )nil )))))"3" "3" assert )nil )))))"3" "3" assert )nil )))))))))))))))))))))))))))"2" "2" assert )nil )))))))))))))))))))))))))))))))))))"3" (skosimp*) (("3" (assert ) nil )))"4" (skosimp*) (("4" (assert ) nil )))))))"2" (skeep)"2" (inst - "a" "n" "y" )"2" (assert )"2" (skeep)"2" (case "n = m" )"1" (replace -1)"1" (assert )"1" (inst + "m" )"1" (expand "max_linear_div_power?" )"1" (inst + "b" "m*b" )"1" (split +)"1" (skeep)"1" (inst - "x" ) (("1" (assert ) nil )))))"2" (inst - "1" ) (("2" (assert ) nil )))"3" (skeep)"3" "linear_power_is_differentiable" )"3" "m" "y" )"3" assert )"3" "g" )"3" "3" case "FORALL (j:nat): j<=m IMPLIES a(j)=g(j)*b(0)" )"1" "x" )"1" case "polynomial(poly_deriv(a),m-1)(x) = polynomial(poly_deriv(g),m-1)(x)*b(0)" )"1" "1" replace -4)"1" expand "polynomial" "1" expand "sigma" +)"1" expand "sigma" "1" expand "*" )"1" nil )))))))))))))"2" "2" expand "polynomial" +)"2" rewrite "sigma_scal_right" "2" rewrite "sigma_eq" )"2" "2" "2" expand "poly_deriv" "2" "1+n!1" )"2" assert )"2" replace "2" assert )nil )))))))))))))))))))))))))"2" "polynomial_eq_coeff" )"2" "a" "b(0)*g" "m" )"2" assert )"2" "2" "2" "1" "1" "j" )"1" expand "*" )"1" assert )nil )))))))"2" "2" "x!1" )"2" "2" replace "2" expand "polynomial" "2" expand "sigma" "2" expand "sigma" "2" "x!1" )"2" replace "2" rewrite "scal_polynomial2" )nil )))))))))))))))))))))))))))))))))))))))))))))"4" (inst - "1" )"4" (flatten)"4" "m" )"4" assert )"4" expand "polynomial" (-1 1))"4" rewrite "sigma_scal_right" "4" expand "*" )"4" assert )nil )))))))))))))))))))))))))))"2" (label "neqm" 1)"2" (hide "neqm" )"2" case "EXISTS (q:[nat->real]): FORALL (x:real): polynomial(q,n-m)(x) = (x-y)^1*polynomial(poly_deriv(b),n-m-1)(x) + m*polynomial(b,n-m)(x)" )"1" (skeep)"1" case "FORALL (x): ") "1" (inst + "m" )"1" (expand "max_linear_div_power?" )"1" (inst + "b" "q" )"1" assert )"1" "1" "1" "x" )"1" (assert ) nil )))))"2" "1" )"2" (assert ) nil )))"3" (propax) nil )"4" "y" )"4" assert )"4" assert )"4" replace -2 +)"4" "1" )"4" "4" "m" )"4" assert )"4" expand "^" -1)"4" expand "expt" "4" assert )nil )))))))))))))))))))))))))))))))"2" (lemma "linear_power_is_differentiable" )"2" (inst - "m" "y" )"2" (assert )"2" "z" )"2" "2" assert )"2" "2" case "NOT polynomial(poly_deriv(a),n-1) = polynomial(poly_deriv(polynomial_prod(z,m,b,n-m)),n-1)" )"1" case "NOT polynomial(poly_deriv(LAMBDA (i:nat): IF i>n THEN 0 ELSE a(i) ENDIF),n-1) = polynomial(poly_deriv(polynomial_prod(z,m,b,n-m)),n-1)" )"1" "1" "aq" "%1" )"1" replace -1)"1" case "aq = polynomial_prod(z, m, b, n - m)" )"1" (assert ) nil )"2" "polynomial_eq_coeff" )"2" "aq" "polynomial_prod(z, m, b, n - m)" "n" )"2" "2" "2" "1" "1" case "x!1 > n" )"1" expand "aq" "1" assert )"1" expand "polynomial_prod" "1" expand "max" )"1" assert )"1" expand "sigma" "1" nil )))))))))))))"2" "x!1" )"2" assert )nil )))))))"2" "2" rewrite "polynomial_prod_def" "2" "x!1" )"2" "x!1" )"2" "2" assert )"2" replace "2" replace "2" expand "polynomial" "2" rewrite "sigma_restrict_eq" )"2" "2" expand "restrict" )"2" "2" expand "aq" )"2" nil )))))))))))))))))))))))))))))))))))))))))))))))"2" replace -1 1 :dir rl)"2" "2" expand "polynomial" 1)"2" rewrite "sigma_restrict_eq" )"2" "2" "2" expand "restrict" )"2" expand "poly_deriv" )"2" nil )))))))))))))))))))"2" " poly_product_rule" )"2" "2" "2" "x" )"2" assert )"2" "neqm" )"2" assert )"2" replace "2" replace "2" "x" )"2" "x" )"2" replace "2" replace "2" "x" )"2" replace "2" assert )"2" "expt_plus" )"2" "m-1" "1" "x-y" )"1" assert )nil )"2" "2" replace "2" expand "^" "2" expand "expt" "2" "2" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))"3" (assert ) nil )))))"2" (hide 3)"2" "DIGG" "LAMBDA (ii:nat): IF ii = n-m THEN poly_deriv(b)(n-m-1) + m*b(n-m) ELSIF ii>0 THEN poly_deriv(b)(ii-1) - y*poly_deriv(b)(ii) + m*b(ii) ELSE -y*poly_deriv(b)(0) + m*b(0) ENDIF" )"1" (inst + "DIGG" )"1" (skeep)"1" "IP" "LAMBDA (i:nat): IF i = 1 THEN 1 ELSIF i = 0 THEN -y ELSE 0 ENDIF" )"1" case "x-y = polynomial(IP,1)(x)" )"1" replace -1 1)"1" expand "^" 1)"1" expand "expt" 1)"1" expand "expt" 1)"1" rewrite "polynomial_prod_def" )"1" rewrite "scal_polynomial2" "1" expand "polynomial" 1)"1" rewrite "sigma_sum" )"1" rewrite "sigma_restrict_eq" )"1" "1" "1" expand "restrict" )"1" "1" assert )"1" "1" nil )"2" "2" case "DIGG(x!1) = ") "1" assert )nil )"2" "2" "2" expand "DIGG" "2" expand "polynomial_prod" )"2" expand "max" )"2" assert )"2" case "x!1 = 0" )"1" "1" assert )"1" "sigma_eq_one_arg" )"1" "1" "0" )"1" assert )"1" "1" replace "1" expand "IP" "1" expand "*" )"1" "neqm" )"1" assert )nil )))))))))"2" "neqm" )"2" assert )nil )))"3" nil )))))))"2" "2" assert )nil )))))))))))"2" assert )"2" assert )"2" "2" "1" "1" "1" assert )"1" expand "sigma" "1" expand "sigma" "1" expand "IP" "1" expand "*" )"1" nil )))))))))))))))"2" "2" assert )"2" rewrite "sigma_reverse" "1" expand "sigma" "1" expand "sigma" "1" assert )"1" case "NOT %1 = 0" )"1" "1" rewrite "sigma_restrict_eq_0" )"1" "1" "1" assert )nil )))))"2" "2" assert )nil )))))))"2" "2" assert )"2" expand "IP" "2" expand "*" )"2" assert )nil )))))))))"3" "3" assert )nil )))"4" "4" assert )nil )))"5" "5" assert )nil )))))))))))"2" "2" assert )nil )))))))))))))))))))))))))))))))"3" "neqm" )"3" assert )nil )))))))))))))))"2" "2" "2" "neqm" )"2" assert )nil )))))))))))))))))))))))))))))"2" assert )"2" "neqm" )"2" assert )"2" expand "IP" 2)"2" "2" nil )))))))))))))))))))"2" (skosimp*) (("2" (assert ) nil )))"3" (skosimp*) (("3" (assert ) nil )))"4" (skosimp*)"4" (assert )"4" (reveal "neqm" )"4" (assert ) nil )))))))))))"3" (assert )"3" (reveal "neqm" ) (("3" (assert ) nil )))))"4" (assert ) nil )))))))))))))))))"3" (skosimp*) (("3" (assert ) nil )))"4" (skosimp*) (("4" (assert ) nil ))))nil )nil nil ))nil 3591634826"" (subtype-tcc) nil nil ) ((/= const-decl "boolean" notequal nil ))nil ))nil 3591634835"" (skeep)"" (rewrite "max_linear_div_power_rew" )"" (split)"1" (flatten)"1" (skosimp*)"1" (assert )"1" (inst + "b!1" "n-m" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (case "NOT m<=n" )"1" (hide 2)"1" (lemma "polynomial_prod_def" )"1" (lemma "linear_power_is_differentiable" )"1" (inst - "m" "y" )"1" (assert )"1" (skolem - "aa" )"1" (flatten)"1" (skeep)"1" (hide -4)"1" "aa" "b" "k" "m" _)"1" case "NOT polynomial(a,n) = polynomial(polynomial_prod(aa,m,b,k),k+m)" )"1" "1" "x!1" )"1" "x!1" )"1" replace -4 :dir rl)"1" replace -3)"1" assert )"1" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "EXISTS (D:nat): D<=k AND b(D)/=0 AND FORALL (i:nat): i>D AND i<=k IMPLIES b(i)=0" )"1" "1" "pp" "polynomial_prod(aa, m, b, k)" )"1" replace -1)"1" case "pp(D+m)/=0" )"1" "1" case "NOT polynomial(LAMBDA (i:nat): IF i>n THEN 0 ELSE a(i) ENDIF,k+m) = polynomial(pp,k+m)" )"1" "1" "1" "x!1" )"1" "1" "1" expand "polynomial" "1" "sigma_split" )"1" "1" "n" )"1" assert )"1" "1" case "%1 = 0" )"1" "1" expand "polynomial" "1" rewrite "sigma_eq" )nil nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "polynomial_eq_coeff" )"2" "2" assert )"2" "D+m" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "pp" -1)"2" "2" expand "polynomial_prod" )"2" assert )"2" "sigma_eq_one_arg" )"2" "1" "m" )"1" assert )"1" "1" expand "max" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "D-i+m" )"2" assert )nil nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "EXISTS (ii:nat): ii<=k AND b(ii)/=0" )"1" "1" "1" case "FORALL (kk:nat): kk>=ii IMPLIES EXISTS (D: nat): AND AND (FORALL (i: nat): i > D AND i <= kk IMPLIES b(i) = 0)") "1" "k" )"1" (assert ) nil nil ))nil )"2" "2" "kk" )"1" assert )"1" case "ii = 0" )"1" "1" assert )"1" "0" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" assert )"2" case "j>=ii" )"1" assert )"1" case "b(1+j)/=0" )"1" "1" "1+j" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "D" )"2" assert )"2" "2" "i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "b(1+j)/=0" )"1" "1+j" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "polynomial" )"2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "i!1" )"2" assert )"2" "2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skeep)"2" "bb" "LAMBDA (i:nat): IF i<=k THEN b(i) ELSE 0 ENDIF" )"2" (inst + "bb" )"2" (assert )"2" case "polynomial(bb,n-m) = polynomial(b,k)" )"1" (assert ) nil nil )"2" (hide 3)"2" case "NOT EXISTS (i:nat): i<=k AND i>n-m AND b(i)/=0" )"1" (case "k <= n-m" )"1" expand "polynomial" 2 1)"1" "1" "sigma_split" )"1" "1" "k" )"1" assert )"1" "1" case "%1 = 0" )"1" "1" assert )"1" expand "polynomial" "1" rewrite "sigma_eq" )"1" "1" "1" expand "bb" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "bb" 1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT k>n-m" )"1" (assert ) nil nil )"2" "2" "2" expand "polynomial" + 2)"2" "sigma_split" )"2" "2" "n-m" )"2" assert )"2" "2" case "%1 = 0" )"1" "1" expand "polynomial" "1" rewrite "sigma_eq" )"1" "1" expand "bb" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )"2" "2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "linear_power_is_differentiable" )"2" case "NOT k>n-m" )"1" "1" (assert ) nil nil ))nil )"2" "m" "y" )"2" assert )"2" "AA" )"2" "2" assert )"2" "2" "polynomial_prod_def" )"2" case "EXISTS (i:nat): i<=k AND i>n-m AND b(i)/=0 AND FORALL (ij:nat): ij>i AND ij<=k IMPLIES b(ij)=0" )"1" "D" )"1" "1" case "polynomial(b,k) = polynomial(b,D)" )"1" replace -1)"1" "AA" "b" "D" "m" "1" "pp" "polynomial_prod(AA, m, b, D)" )"1" "aa" "LaMBDA (i:nat): IF i<=n THEN a(i) ELSE 0 ENDIF" )"1" case "FORALL (ij:nat): ij<=m+k IMPLIES aa(ij) = pp(ij)" )"1" "m+D" )"1" assert )"1" expand "aa" "1" expand "pp" "1" expand "polynomial_prod" "1" expand "max" "1" expand "sigma" "1" expand "sigma" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "polynomial_eq_coeff" )"2" "aa" "pp" "m+k" )"2" assert )"2" "2" "2" "1" "1" "ij" )nil nil ))nil )"2" "2" case "NOT polynomial(aa,k+m)=polynomial(a,n)" )"1" "1" expand "polynomial" "1" "sigma_split" )"1" "1" "n" )"1" assert )"1" "1" case "%1 = 0" )"1" "1" assert )"1" expand "polynomial" "1" rewrite "sigma_eq" )"1" "1" expand "aa" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )"2" "2" expand "aa" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" replace "2" case "polynomial(pp,k+m) = polynomial(pp,D+m)" )"1" "1" replace "1" "x!1" )"1" replace "1" "x!1" )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "FORALL (ij:nat): ij>D+m IMPLIES pp(ij) = 0" )"1" expand "polynomial" "1" "1" "sigma_split" )"1" "1" "D+m" )"1" assert )"1" "1" case "%1 = 0" )"1" "1" expand "polynomial" "1" nil nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "pp" )"2" expand "polynomial_prod" )"2" expand "max" )"2" assert )"2" expand "sigma" )"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 )"2" "2" expand "polynomial" "2" "sigma_split" )"2" "2" "D" )"2" assert )"2" "2" case "%1 = 0" )"1" "1" expand "polynomial" "1" nil nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (i:nat): i>n-m AND i<=k IMPLIES b(i) = 0" )"1" "1" expand "polynomial" "1" "sigma_split" )"1" "1" "n-m" )"1" assert )"1" "1" case "%1 = 0" )"1" "1" assert )"1" expand "polynomial" "1" rewrite "sigma_eq" )"1" "1" expand "bb" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (kk:nat): (EXISTS (i: nat): AND AND AND AND ij <= n-m+1+kk IMPLIES b(ij) = 0)) OR (FORALL (i: nat): i > n - m AND i <= n-m+1+kk IMPLIES b(i) = 0)") "1" "k-n+m-1" )"1" assert )"1" nil nil ))nil ))nil )"2" "2" "kk" )"1" assert )"1" "1" "n-m+1" )"1" assert )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "kk" )"2" "2" assert )"2" case "b(n-m+2+kk)=0" )"1" "1" "1" "i!1" )"1" "1" "1" "ij!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i" )"2" nil nil ))nil ))nil ))nil )"2" "n-m+2+kk" )"2" assert )"2" "2" "1" assert )nil nil )"2" "ij!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil more_polynomial_propsnil )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 )nil integers nil )"bool" reals nil )nil integers nil )"(total_order?[real])" nil )"nat" more_polynomial_props nil )"nat" more_polynomial_props nil )"[nat -> real]" more_polynomial_props nil )"[nat -> real]" more_polynomial_props nil )"real" reals nil )"[nat -> real]" more_polynomial_props nil )nil nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"[T, T -> boolean]" equalities nil )"[real -> real]" polynomials nil )"real" polynomials nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )nil naturalnumbers nil )nil defined_types nil )"[nat -> real]" more_polynomial_props nil )nil sigma nil )nil integers nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"posnat" more_polynomial_props nil )"nat" more_polynomial_props nil )"{k: int | i <= k AND j <= k}" nil )"{s: rat | s >= q AND s >= r}" nil )"int" integers nil )nil polynomials nil )nil naturalnumbers nil )nil sigma nil )nil sigma nil )nil sigma nil )"posint" nil )"real" sigma nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )nil sigma nil )nil sigma nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil polynomials nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil ))nil ))nil 3591628357"" case "FORALL (a: sequence[real], n: nat, y: real, m, kp: posnat): AND NOT max_linear_div_power?(a, n, y)(kp)") "1" (skeep)"1" (inst-cp - "a" "n" "y" "m" "kp" )"1" (inst - "a" "n" "y" "kp" "m" ) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (rewrite "max_linear_div_power_rew" )"2" (rewrite "max_linear_div_power_rew" )"2" (flatten)"2" (assert )"2" (skolem - "bm" )"2" (skolem - "bk" )"2" (flatten)"2" case "NOT FORALL (x): polynomial(bm,n-m)(x) = (x-y)^(kp-m)*polynomial(bk,n-kp)(x)" )"1" case "FORALL (x): x/=y IMPLIES polynomial(bm, n - m)(x) = ") "1" "linear_power_is_differentiable" )"1" (inst - "kp-m" "y" )"1" assert )"1" "D" )"1" "1" "polynomial_prod_def" )"1" case "NOT FORALL (x): x/=y IMPLIES polynomial(bm,n-m)(x) = polynomial(polynomial_prod(D, kp - m, bk, n - kp), kp - m + (n - kp))(x)" )"1" "1" "D" "bk" "n-kp" "kp-m" "x" )"1" "x" )"1" replace -4)"1" "x" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "polynomial(bm, n - m) = ") "1" "1" "y" )"1" "D" "bk" "n-kp" "kp-m" "y" )"1" "y" )"1" replace -6)"1" assert )"1" replace "1" case "0^(kp-m) = 0" )"1" assert )nil nil )"2" expand "^" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (aa:[nat->real],nm:nat): (FORALL (x): x/=y IMPLIES polynomial(aa,nm)(x)=0) IMPLIES polynomial(aa,nm) = (LAMBDA (x): 0)" )"1" "bm-polynomial_prod(D, kp - m, bk, n - kp)" "n-m" )"1" assert )"1" "1" rewrite "polynomial_sub" )"1" expand "-" )"1" "1" "1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x" )"2" assert )"2" rewrite "polynomial_sub" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "poly_continuous" )"2" "2" "aa" "nm" "x!1" "abs(polynomial(aa,nm)(x!1))/2" )"1" "1" "y-delta!1/2" )"1" "x!1" )"1" assert )"1" "1" replace "1" assert )"1" "y-delta!1/2" )"1" assert )"1" "1" expand "abs" )"1" "1" "1" "1" nil nil ))nil ))nil ))nil ))nil )"2" expand "abs" "2" assert )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 ))nil ))nil )"2" (hide (2 3 4))"2" (skeep)"2" "x" )"2" "x" )"2" assert )"2" "2" "expt_plus" )"2" "m" "kp-m" "x-y" )"2" assert )"2" "2" "(x-y)^m" )"1" assert )"1" replace -4)"1" assert )"1" nil nil ))nil ))nil ))nil )"2" "2" "expt_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "y" )"2" (assert )"2" (expand "^" -1)"2" expand "expt" -1)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil more_polynomial_propsnil )"(total_order?[real])" nil )nil polynomials nil )nil polynomials nil )"[T -> real]" real_fun_ops nil )"{y: posreal | y >= x}" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"posreal" nil )"real" reals nil )nil real_types nil )"real" more_polynomial_props nil )"nat" more_polynomial_props nil )"[nat -> real]" more_polynomial_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"nnreal" nil )nil polynomials nil )"nat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" exponentiation nil )"nat" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"real" polynomials nil )"int" integers nil )nil nil )nil reals nil )nil exponentiation nil )nil real_props nil )nil extra_real_props nil )"real" more_polynomial_props nil )"real" more_polynomial_props nil )"posnat" more_polynomial_props nil )nil reals nil )nil real_props nil )nil exponentiation nil )"(total_order?[real])" nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[real -> real]" polynomials nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props 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 )nil integers nil )"bool" reals nil )nil integers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" more_polynomial_props nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3591709973"" (skeep)"" (rewrite "max_linear_div_power_rew2" )"" (rewrite "max_linear_div_power_rew2" )"" (skosimp*)"" (inst + "b!1" "k!1" )"" (assert )"" (skeep)"" (inst - "x" )"" (inst - "x" )"" (lemma "expt_plus" )"" (inst?)"1" (assert )"1" (replace -1) (("1" (assert ) nil nil ))nil ))nil )"2" (flatten)"2" (replace -1)"2" (expand "^" )"2" expand "expt" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil more_polynomial_propsnil )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 )nil integers nil )"bool" reals nil )nil integers nil )nil exponentiation nil )"real" exponentiation nil )"real" exponentiation nil )"odd_int" integers nil )"real" reals nil )nil reals nil )"real" more_polynomial_props nil )"real" more_polynomial_props nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil ))nil 3591455656"" (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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"real" polynomials nil )"bool" more_polynomial_props nil )"real" reals nil )"int" integers nil )"real" reals nil ))nil ))nil 3591455656"" (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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" exponentiation nil )"[real -> real]" polynomials nil )"real" polynomials nil )"bool" more_polynomial_props nil )"real" reals nil )"int" integers nil )"real" reals nil ))nil ))nil 3591455878"" (skeep)"" (expand "max_linear_div_power?" -)"" (skeep)"" (case "n = 0" )"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (assert )"2" (rewrite "max_linear_div_power_rew" )"2" (inst + "q" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" more_polynomial_props nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"(total_order?[real])" nil )nil more_polynomial_propsnil )nil sequences nil )"real" polynomials nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"int" integers nil ))nil 3589289206"" case "NOT FORALL (a: sequence[real], n: nat, y: real): AND polynomial(a, n)(y) = 0 IMPLIESAND FORALL (x):AND polynomial(b, n - m)(y) /= 0)") "1" (hide 2)"1" (induct "n" )"1" (skeep)"1" (expand "polynomial" -1)"1" (expand "sigma" )"1" (expand "sigma" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skolem 1 "nn" )"2" (flatten)"2" (skeep)"2" (lemma "polynomial_zero_factor" )"2" (inst - "a" "nn+1" "y" )"2" (assert )"2" (skeep -1)"2" (case "polynomial(g,nn)(y)/=0" )"1" (inst + "g" "1" )"1" (assert )"1" (expand "^" +)"1" expand "expt" +)"1" expand "expt" +)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (inst - "g" "y" )"2" (assert )"2" case "g(nn)/=0" )"1" assert )"1" "1" "1" assert )"1" "b" "m+1" )"1" assert )"1" "1" "x" )"1" "x" )"1" assert )"1" case "FORALL (rr:real): x*rr-rr*y = (x-y)^1*rr" )"1" rewrite -1)"1" "1" replace "1" assert )"1" "1" assert )"1" replace "1" assert )"1" "expt_plus" )"1" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil )"2" "2" replace "2" expand "^" "2" expand "expt" "2" nil nil ))nil ))nil ))nil ))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 )"2" "2" assert )"2" "polynomial_eq_coeff" )"2" "DIG" "LAMBDA (ii:nat): IF ii = 1+nn THEN g(nn) ELSIF ii>0 THEN g(ii-1) - g(ii)*y ELSE -g(0)*y ENDIF" )"1" "a" "DIG" "1+nn" )"1" "1" "1" "1" "1+nn" )"1" expand "DIG" -1)"1" assert )nil nil ))nil ))nil )"2" "2" "x!1" )"2" assert )"2" replace -4 1)"2" expand "polynomial" "2" "IG" "LAMBDA (i: nat): g(i) * (IF i = 0 THEN 1 ELSE x!1 ^ i ENDIF)" )"2" replace "2" case "sigma(0,nn,IG)=sigma(0,1+nn,LAMBDA (ii:nat): IF ii=0 THEN 0 ELSE IG(ii-1) ENDIF)" )"1" "x!1" )"1" replace "1" rewrite "sigma_scal_right" "1" rewrite "sigma_scal_right" "1" case "sigma(0, nn, LAMBDA (i: nat): IG(i) * y) = sigma(0, 1+nn, LAMBDA (i: nat): IF i >nn THEN 0 ELSE IG(i) * y ENDIF)" )"1" replace "1" rewrite "sigma_minus" )"1" rewrite "sigma_restrict_eq" )"1" "1" "1" expand "restrict" )"1" "1" assert )"1" "1" expand "DIG" "1" assert )"1" expand "IG" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" case "NOT x!2 = 1+nn" )"1" assert )nil nil )"2" replace "2" assert )"2" expand "DIG" "2" expand "IG" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "IG" "2" expand "DIG" "2" "2" assert )"2" "1" replace "1" expand "^" "1" expand "expt" "1" expand "expt" "1" nil nil ))nil ))nil ))nil ))nil )"2" "expt_plus" )"2" "x!2-1" "1" "x!1" )"1" assert )"1" replace "1" expand "^" "1" expand "expt" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace "2" expand "^" "2" expand "expt" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sigma" "2" rewrite "sigma_restrict_eq" )"2" "2" expand "restrict" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" case "FORALL (k:nat): k<=nn IMPLIES sigma(0, k, IG) = LAMBDA (ii: nat): IF ii = 0 THEN 0 ELSE IG(ii - 1) ENDIF)") "1" "1" assert )nil nil ))nil )"2" "k" )"1" assert )"1" "1" expand "IG" )"1" nil nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "sigma" "2" nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))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 ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil )"2" (skeep)"2" (inst - "a" "n" "y" )"2" (assert )"2" (skeep)"2" (inst + "m" )"2" (rewrite "max_linear_div_power_rew" )"2" (assert )"2" (inst + "b" )"2" (split)"1" (skeep)"1" (inst - "x" ) (("1" (assert ) nil nil ))nil ))nil )"2" (inst - "1" ) (("2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (hide 2) (("4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil )nil more_polynomial_propsnil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil polynomials nil )"real" reals nil )"nat" more_polynomial_props nil )nil extra_real_props nil )"(strict_total_order?[real])" real_props nil )nil sigma nil )"real" reals nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"real" more_polynomial_props nil )"int" integers nil )"[nat -> real]" more_polynomial_props nil )"[T -> real]" sigma nil )nil sigma nil )nil sigma nil )nil sigma nil )nil naturalnumbers nil )"[nat -> real]" more_polynomial_props nil )"[numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"(total_order?[real])" nil )"real" more_polynomial_props nil )"real" more_polynomial_props nil )nil reals nil )"even_int" integersnil )"odd_int" integers nil )nil exponentiation nil )"real" exponentiation nil )"posint" nil )"(total_order?[real])" nil )nil polynomials nil )"real" sigma nil )nil naturalnumbers nil )nil defined_types nil )"real" reals nil )"real" reals 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers 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 )"[T, T -> boolean]" equalities nil )"[real -> real]" polynomials nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3591458539"" case " FORALL (a: sequence[real], n: nat, y: real, nz: nzreal, m: posnat): ") "1" (skeep)"1" (inst-cp - "a" "n" "y" "nz" "m" )"1" (inst - "nz*a" "n" "y" "1/nz" "m" )"1" (case "(1/nz)*(nz*a) = a" )"1" (ground) nil nil )"2" (hide-all-but 1)"2" (decompose-equality)"2" (expand "*" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (rewrite "max_linear_div_power_rew" +)"2" (rewrite "max_linear_div_power_rew" -)"2" (flatten)"2" (assert )"2" (skeep)"2" (inst + "nz*b" )"2" (assert )"2" (split +)"1" (skeep)"1" (inst - "x" )"1" (rewrite "scal_polynomial2" )"1" rewrite "scal_polynomial2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "scal_polynomial2" )"2" (flatten)"2" (mult-by 1 "nz" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil more_polynomial_propsnil )"(total_order?[real])" nil )"int" integers nil )nil real_props nil )nil reals nil )"[real -> real]" polynomials nil )nil polynomials nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"nzreal" nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" reals nil )"[T, T -> boolean]" equalities 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 )"boolean" notequal nil )nil reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[bool, bool -> bool]" booleans nil )"bool" more_polynomial_props nil )"[T -> real]" real_fun_ops nil ))nil 3591632939"" (skeep)"" (case "polynomial(b,j)(y)/=0" )"1" (flatten)"1" (assert )"1" (case "k = m" )"1" (assert ) nil nil )"2" (hide 3)"2" (lemma "max_linear_div_power_unique" )"2" (inst?)"2" (case "NOT k = 0" )"1" (inst - "k" )"1" (assert )"1" (rewrite "max_linear_div_power_rew2" +)"1" (inst + "b" "j" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (replaces -1)"2" (expand "^" )"2" (expand "expt" )"2" (hide -1)"2" rewrite "max_linear_div_power_rew2" -)"2" "2" "y" )"2" "y" )"2" assert )"2" expand "^" )"2" expand "expt" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (case "k < m" )"1" (assert ) nil nil )"2" (hide 2)"2" case "EXISTS (jk:posnat): b(jk)/=0 AND polynomial(b,j) = polynomial(b,jk)" )"1" (skeep)"1" (replace -1)"1" (lemma "poly_max_zero_power" )"1" (inst - "b" "jk" "y" )"1" (assert )"1" (skolem -1 "bm" )"1" "max_linear_div_power_additive" )"1" "a" "n" "y" "k" "bm" "b" "jk" )"1" assert )"1" replace -6)"1" "max_linear_div_power_unique" )"1" "a" "n" "y" "bm+k" "m" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "FORALL (i:nat): i<=j IMPLIES b(i)=0" )"1" (case "polynomial(b,j) = (LAMBDA (x:real): 0)" )"1" (replaces -1)"1" (hide -1)"1" (assert )"1" (expand "max_linear_div_power?" )"1" (skosimp*)"1" "poly_continuous" )"1" "b!1" "n-m" "y" "abs(polynomial(b!1, n - m)(y))/2" )"1" "1" "y-delta!1/2" )"1" assert )"1" expand "abs" -1 1)"1" assert )"1" "y-delta!1/2" )"1" assert )"1" "nzreal_times_nzreal_is_nzreal" )"1" "(-1 * (delta!1 / 2)) ^ m" "polynomial(b!1, n - m)(y - delta!1 / 2)" )"1" assert )"1" "y-delta!1/2" )"1" "y-delta!1/2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" 1)"2" assert )"2" "2" (ground) nil nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (decompose-equality 1)"2" (expand "polynomial" 1)"2" (rewrite "sigma_restrict_eq_0" )"2" (skosimp*)"2" "i!1" )"2" assert )"2" "2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-2 -3))"2" (lemma "polynomial_degree_existence" )"2" (inst - "b" "j" )"2" (assert )"2" (split -)"1" (skeep -1)"1" "i" )"1" (assert ) nil nil )"2" assert )"2" case "i = 0" )"1" "1" assert )"1" "1" expand "polynomial" -2)"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" "2" "polynomial_eq_coeff" )"2" "b" "(LAMBDA (i:nat): 0)" "j" )"2" "2" "2" "1" "1" "i" )nil nil ))nil )"2" "2" "x!1" )"2" "2" "2" expand "polynomial" "2" rewrite "sigma_restrict_eq_0" )"2" "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 )"[real -> real]" polynomials nil )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 )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"real" exponentiation nil )"nat" exponentiation nil )"real" reals nil )"real" reals nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"nat" more_polynomial_props nil )nil more_polynomial_propsnil )NOT const-decl "[bool -> bool]" booleans nil )nil more_polynomial_propsnil )"[T, T -> boolean]" equalities nil )nil integers nil )"bool" reals nil )nil integers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )nil sigma nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma nil )nil sigma nil )"(total_order?[real])" nil )"nnreal" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" more_polynomial_props nil )"posnat" more_polynomial_props nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[nat -> real]" more_polynomial_props nil )"real" more_polynomial_props nil )nil real_types nil )"posreal" nil )nil real_types nil )nil reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"odd_int" integers nil )"nzreal" nil )"nzreal" exponentiation nil )"real" reals nil )"real" reals nil )nil polynomials nil )"bool" more_polynomial_props nil )nil more_polynomial_propsnil )nil polynomials nil )
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.1.1Bemerkung:
(vorverarbeitet am 2026-05-03)
¤ *Bot Zugriff
2026-05-26
