|
(more_polynomial_props
(polynomial_degree_existence 0
(polynomial_degree_existence-1 nil 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
(EXISTS (i: upto(1+n)): a(i) /= 0))")
(("1" (hide -3)
(("1" (split -)
(("1" (flatten)
(("1" (case "a(1+n) = 0")
(("1" (skosimp*)
(("1" (inst + "i!1")
(("1" (assert)
(("1"
(split +)
(("1"
(skeep)
(("1"
(inst - "j")
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide (-2 3))
(("2"
(replace -2 :dir rl)
(("2"
(decompose-equality 1)
(("2"
(expand "polynomial" 1)
(("2"
(expand "sigma" + 1)
(("2"
(replaces -1)
(("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"
(replaces -1)
(("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"
(skosimp*)
(("1" (inst - "i!1") nil nil))
nil)
("2"
(decompose-equality 1)
(("2"
(inst + "x!1")
(("2"
(flatten)
(("2"
(replaces -2)
(("2"
(expand "polynomial")
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(skosimp*)
(("2"
(lift-if)
(("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"
(flatten)
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subrange type-eq-decl nil integers nil)
(polynomial_eq_coeff formula-decl nil polynomials nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil sigma nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sigma_restrict_eq_0 formula-decl nil sigma nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(polynomial_rec formula-decl nil polynomials nil)
(real_times_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(sigma def-decl "real" sigma nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(> const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(polynomial const-decl "[real -> real]" polynomials nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(sequence type-eq-decl nil sequences nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(poly_deriv_limit_TCC1 0
(poly_deriv_limit_TCC1-1 nil 3587828917 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(poly_deriv_limit_TCC2 0
(poly_deriv_limit_TCC2-1 nil 3587828917 ("" (subtype-tcc) nil nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(/= const-decl "boolean" notequal nil))
nil))
(poly_deriv_limit 0
(poly_deriv_limit-2 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"
(invoke (case "%1 = %2") (! -4 2)
(! 2 1 1 2))
(("1" (replace -1)
(("1"
(replace -5 :dir rl)
(("1"
(inst - "cc")
(("1"
(split -)
(("1" (propax) nil nil)
("2"
(expand "abs")
(("2"
(lift-if)
(("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"
(split -)
(("1" (propax) nil nil)
("2"
(expand "abs")
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(poly_mean_value formula-decl nil polynomials nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(FDX_44 skolem-const-decl "real" more_polynomial_props nil)
(FDX_45 skolem-const-decl "real" more_polynomial_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nonzero_times3 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(polynomial const-decl "[real -> real]" polynomials nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(poly_deriv const-decl "real" polynomials nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(poly_continuous formula-decl nil polynomials nil))
nil)
(poly_deriv_limit-1 nil 3587821660
(""
(name "PQ"
"LAMBDA (a:sequence[real],ki:nat): (FORALL (y: real, epsil: posreal):
EXISTS (delta: posreal):
FORALL (x: real):
abs(x - y) < delta AND x /= y IMPLIES
abs(polynomial(poly_deriv(a), ki+1 - 1)(y) -
(polynomial(a, ki+1)(x) - polynomial(a, ki+1)(y)) / (x - y))
< epsil)")
(("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"
(replaces -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"
(cross-mult 1)
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"
(skosimp*)
(("2"
(inst + "min(delta!1,delta!2)")
(("2"
(skeep)
(("2"
(inst - "x")
(("2"
(inst - "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"
(hide -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"
(hide -1)
(("1"
(expand
"abs"
(-1 -3 +))
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2"
(expand
"polynomial")
(("2"
(expand
"sigma"
+
1)
(("2"
(expand
"sigma")
(("2"
(invoke
(case
"%1 = 0")
(!
1
2
1))
(("1"
(replaces
-1)
(("1"
(assert)
(("1"
(expand
"poly_deriv")
(("1"
(expand
"apow")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(expand
"poly_deriv")
(("2"
(expand
"apow")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(skeep)
(("2"
(expand "polynomial")
(("2"
(expand
"sigma"
+
1)
(("2"
(expand "sigma")
(("2"
(invoke
(case
"%1 = 0")
(! 1 2 1))
(("1"
(replaces -1)
(("1"
(expand
"apow")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(skosimp*)
(("2"
(expand
"apow")
(("2"
(lift-if)
(("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):
EXISTS (delta: posreal):
FORALL (x: real):
abs(x - y) < delta AND x /= y IMPLIES
abs(kc*nm*y^(nm-1) -
(kc*x^nm -kc*y^nm) / (x - y))
< epsil)")
(("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"
(invoke
(case "%1 = 0")
(! 2 1 1 2 1))
(("1"
(replaces -1)
(("1"
(expand "abs")
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide 3)
(("2"
(expand "polynomial")
(("2"
(rewrite "sigma_minus")
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(lift-if)
(("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"
(inst + "delta")
(("1"
(skeep)
(("1"
(inst - "x")
(("1"
(assert)
(("1"
(case "1+ki)
(("1"
(invoke
(case "%1 = 0")
(! 2 1 1))
(("1"
(replaces -1)
(("1"
(expand "abs" +)
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide 3)
(("2"
(invoke
(case "%1 = 0")
(! 1 1 1))
(("1"
(invoke
(case "%1 = 0")
(! 1 1 2))
(("1" (assert) nil nil)
("2"
(invoke
(case "%1 = 0")
(! 1 1 1))
(("1"
(assert)
nil
nil)
("2"
(invoke
(case "%1 = 0")
(! 1 1 1))
(("1"
(invoke
(case "%1 = 0")
(! 1 1 2))
(("1"
(assert)
nil
nil)
("2"
(expand
"polynomial"
1)
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(skosimp*)
(("2"
(expand
"apow"
1)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"polynomial"
1)
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(skosimp*)
(("2"
(expand
"apow"
1)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "polynomial" 1)
(("2"
(expand
"poly_deriv"
1)
(("2"
(rewrite
"sigma_restrict_eq_0")
(("2"
(skosimp*)
(("2"
(expand
"apow"
1)
(("2"
(propax)
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"
(inst-cp - "x")
(("1"
(inst - "y")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide 4)
(("2"
(skeep)
(("2"
(expand
"polynomial"
1)
(("2"
(lemma
"sigma_eq_one_arg")
(("2"
(inst
-
_
_
_
"nm")
(("2"
(inst?)
(("2"
(assert)
(("2"
(split -)
(("1"
(expand
"apow"
-1
2)
(("1"
(propax)
nil
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"apow"
1)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(expand
"apow"
1)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "polynomial" 1)
(("2"
(lemma
"sigma_eq_one_arg")
(("2"
(inst - _ _ _ "nm-1")
(("2"
(inst?)
(("2"
(assert)
(("2"
(split -)
(("1"
(replaces -1)
(("1"
(expand
"poly_deriv"
1)
(("1"
(expand
"apow"
1)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(replaces
-1)
(("1"
(expand
"^")
(("1"
(expand
"expt"
1)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(expand
"poly_deriv"
1)
(("2"
(expand
"apow"
1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(expand
"poly_deriv"
1)
(("3"
(expand
"apow"
1)
(("3"
(propax)
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):
EXISTS (delta: posreal):
FORALL (x: real):
abs(x - y) < delta AND x /= y IMPLIES
abs(nm * y ^ (nm - 1) -
(x ^ nm - y ^ nm) / (x - y))
< epsil)")
(("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"
(inst - "x")
(("1"
(assert)
(("1"
(cross-mult -2)
(("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))
(square_free_min_TCC1 0
(square_free_min_TCC1-1 nil 3587829356 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(polynomial const-decl "[real -> real]" polynomials nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(square_free_min 0
(square_free_min-1 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"
(name "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))
(("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"
(cross-mult -1)
(("1"
(assert)
(("1"
(inst -6 "xy")
(("1"
(split -)
(("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"
(name "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) 0")
(("1" (skeep)
(("1" (inst - "x")
(("1" (assert)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.163 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
