|
(sturmsquarefree
(sturm_sequence?_TCC1 0
(sturm_sequence?_TCC1-1 nil 3583755671 ("" (subtype-tcc) nil 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(^ const-decl "real" exponentiation nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/= const-decl "boolean" notequal nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(sturm_sequence?_TCC2 0
(sturm_sequence?_TCC2-1 nil 3583755671 ("" (subtype-tcc) nil 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(poly_deriv const-decl "real" polynomials "reals/")
(^ const-decl "real" exponentiation nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(/= const-decl "boolean" notequal nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(sturm_sequence_degree_1 0
(sturm_sequence_degree_1-1 nil 3588942625
("" (skeep)
(("" (expand "sturm_sequence?")
(("" (assert)
(("" (split +)
(("1" (skeep) (("1" (assert) nil nil)) nil)
("2" (skeep)
(("2" (case "i = 1")
(("1" (replaces -1)
(("1" (replace -5)
(("1" (expand "poly_deriv" -2)
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (skeep) (("3" (assert) nil nil)) nil)
("4" (skeep)
(("4" (assert)
(("4" (replaces -1)
(("4" (replace -2) (("4" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sturm_sequence? const-decl "bool" sturmsquarefree nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(poly_deriv const-decl "real" polynomials "reals/")
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(polynomial const-decl "[real -> real]" polynomials "reals/")
(sigma def-decl "real" sigma "reals/")
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(max_npreal_0 formula-decl nil min_max "reals/")
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(sturm_seq_repeated_root 0
(sturm_seq_repeated_root-1 nil 3584191381
("" (skeep)
((""
(case "FORALL (i:nat): i-1>=0 AND i+1<=m AND polynomial(p(i),n(i))(x)=0 IMPLIES (polynomial(p(i-1),n(i-1))(x)=0 IFF polynomial(p(i+1),n(i+1))(x)=0)")
(("1" (skeep)
(("1"
(case "FORALL (j:nat): i-j>=0 IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i-k), n(i-k))(x) = 0")
(("1"
(case "FORALL (j:nat): i+j<=m IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i+k), n(i+k))(x) = 0")
(("1" (skeep)
(("1" (case "j>=i")
(("1" (inst - "j-i")
(("1" (assert)
(("1" (inst - "j-i") (("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil))
nil)
("2" (inst -2 "i-j")
(("1" (assert)
(("1" (inst -2 "i-j") (("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (hide (-1 2))
(("2" (induct "j")
(("1" (assert)
(("1" (skeep) (("1" (assert) nil nil)) nil)) nil)
("2" (assert)
(("2" (skosimp*)
(("2" (assert)
(("2" (case "k!1=0 OR k!1=1")
(("1" (ground) nil nil)
("2" (flatten)
(("2" (inst-cp - "k!1-1")
(("2" (inst - "k!1-2")
(("1"
(assert)
(("1"
(assert)
(("1"
(inst - "i-1+k!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "j")
(("1" (assert)
(("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)
("2" (skosimp*)
(("2" (assert)
(("2" (case "k!1=0")
(("1" (assert) nil nil)
("2" (assert)
(("2" (inst-cp - "k!1-1")
(("2" (case "k!1=1")
(("1" (hide -2)
(("1" (assert)
(("1"
(inst - "i")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (inst - "k!1-2")
(("1" (assert)
(("1"
(inst - "i-k!1+1")
(("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*) (("3" (assert) nil nil)) nil)
("4" (assert)
(("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)
("5" (skosimp*) (("5" (assert) nil nil)) nil)
("6" (skosimp*) (("6" (assert) nil nil)) nil)
("7" (skosimp*) (("7" (assert) nil nil)) nil))
nil))
nil)
("3" (skosimp*) (("3" (assert) nil nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (skeep)
(("2" (assert)
(("2" (expand "sturm_sequence?")
(("2" (flatten)
(("2" (inst - "x" "i")
(("2" (assert)
(("2" (expand "sign_ext" -7)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2" (lift-if)
(("2"
(assert)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF const-decl "[bool, bool -> bool]" booleans nil)
(polynomial const-decl "[real -> real]" polynomials "reals/")
(sequence type-eq-decl nil sequences nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(k!1 skolem-const-decl "nat" sturmsquarefree nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(m skolem-const-decl "nat" sturmsquarefree nil)
(j skolem-const-decl "upto(m)" sturmsquarefree nil)
(i skolem-const-decl "nat" sturmsquarefree nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(k!1 skolem-const-decl "nat" sturmsquarefree nil)
(sturm_sequence? const-decl "bool" sturmsquarefree nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(sturm_seq_last_nonzero 0
(sturm_seq_last_nonzero-1 nil 3588410248
("" (skeep)
(("" (skeep)
((""
(case "NOT FORALL (xyzp:real): polynomial(p(m),n(m))(xyzp) = 0")
(("1" (skeep)
(("1" (expand "sturm_sequence?")
(("1" (flatten)
(("1" (inst -6 "xyz" "xyzp")
(("1" (expand "sign_ext" -6)
(("1" (assert)
(("1" (assert)
(("1" (lift-if) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "polynomial_eq_coeff")
(("2" (inst - "p(m)" "LAMBDA (i:nat): 0" "n(m)")
(("2" (assert)
(("2" (flatten)
(("2" (hide -2)
(("2" (split -)
(("1" (inst - "n(m)")
(("1" (expand "sturm_sequence?")
(("1" (flatten)
(("1" (inst -5 "m") (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality 1)
(("2" (inst - "x!1")
(("2" (assert)
(("2" (replaces -1)
(("2" (expand "polynomial" +)
(("2"
(rewrite "sigma_restrict_eq_0")
(("2"
(skosimp*)
(("2"
(assert)
(("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)
((polynomial_eq_coeff formula-decl nil polynomials "reals/")
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sigma_restrict_eq_0 formula-decl nil sigma "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sturm_sequence? const-decl "bool" sturmsquarefree 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 "[T, T -> boolean]" equalities nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(polynomial const-decl "[real -> real]" polynomials "reals/"))
shostak))
(sturm_seq_first_signs_eq 0
(sturm_seq_first_signs_eq-1 nil 3587370024
("" (skeep)
((""
(case "NOT (polynomial(p(0), n(0))(x) /= 0 AND
polynomial(p(0), n(0))(y) /= 0)")
(("1" (hide 2)
(("1" (inst-cp - "x")
(("1" (inst - "y") (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (flatten)
(("2" (assert)
(("2" (inst-cp - "b")
(("2" (assert)
(("2" (flatten)
(("2"
(case "polynomial(poly_deriv(p(0)),max(n(0)-1,0))(b) = 0")
(("1" (expand "sturm_sequence?")
(("1" (flatten)
(("1" (inst -8 "b")
(("1" (assert)
(("1" (expand "sign_ext" -8)
(("1" (assert)
(("1"
(lift-if)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "poly_continuous")
(("2"
(inst - "poly_deriv(p(0))" "max(n(0)-1,0)" "b"
"abs(polynomial(poly_deriv(p(0)),n(0)-1)(b))")
(("1" (skeep -)
(("1"
(case "EXISTS (deltiv:posreal): FORALL (x1:real): abs(b-x1))
(("1"
(case "sign_ext(polynomial(p(0), n(0))(x)) =
-sign_ext(polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b))
AND
sign_ext(polynomial(p(0), n(0))(y)) =
sign_ext(polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b))")
(("1" (hide (-2 -3))
(("1"
(flatten)
(("1"
(expand "sturm_sequence?")
(("1"
(flatten)
(("1"
(inst -9 "b")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 6)
(("2"
(case
"polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)>0")
(("1"
(skeep -2)
(("1"
(case
"FORALL (x1,x2:real): abs(x1-b))
(("1"
(inst-cp - "b-deltiv/2" "b")
(("1"
(inst-cp - "b" "b+deltiv/2")
(("1"
(label "hyplem" -1)
(("1"
(hide "hyplem")
(("1"
(assert)
(("1"
(split +)
(("1"
(expand "sign_ext")
(("1"
(lift-if)
(("1"
(assert)
(("1"
(split 1)
(("1"
(propax)
nil
nil)
("2"
(assert)
(("2"
(hide -1)
(("2"
(split -)
(("1"
(replace
-7)
(("1"
(assert)
(("1"
(lemma
"poly_intermediate_value_dec")
(("1"
(inst
-
"p(0)"
"0"
"n(0)"
"x"
"b-deltiv/2")
(("1"
(assert)
(("1"
(split
-)
(("1"
(skeep
-1)
(("1"
(inst
-
"cc")
(("1"
(inst
-
"cc")
(("1"
(inst
-
"cc")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
-
"b-deltiv/2")
(("2"
(split
-)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "sign_ext")
(("2"
(lift-if)
(("2"
(assert)
(("2"
(split 1)
(("1"
(assert)
(("1"
(hide -3)
(("1"
(split -)
(("1"
(replace
-8)
(("1"
(assert)
(("1"
(lemma
"poly_intermediate_value_dec")
(("1"
(inst
-
"p(0)"
"0"
"n(0)"
"b+deltiv/2"
"y")
(("1"
(assert)
(("1"
(split
-)
(("1"
(skeep
-1)
(("1"
(inst
-
"cc")
(("1"
(inst
-
"cc")
(("1"
(inst
-
"cc")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
-
"b+deltiv/2")
(("2"
(split
-)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skeep)
(("2"
(lemma
"poly_strictly_increasing")
(("2"
(inst
-
"p(0)"
"n(0)"
"x1"
"x2")
(("2"
(assert)
(("2"
(case "n(0)=0")
(("1"
(replaces -1)
(("1"
(expand "polynomial")
(("1"
(expand "sigma")
(("1"
(expand "sigma")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skeep)
(("2"
(expand "max")
(("2"
(assert)
(("2"
(inst - "c")
(("2"
(assert)
(("2"
(split -)
(("1"
(inst
-
"c")
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand
"abs")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"abs"
(-1
-2
-3
-4
-5
1))
(("2"
(lift-if)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)<0")
(("1"
(hide 1)
(("1"
(skeep -2)
(("1"
(case
"FORALL (x1,x2:real): abs(x1-b) polynomial(p(0),n(0))(x2)")
(("1"
(inst-cp - "b-deltiv/2" "b")
(("1"
(inst-cp
-
"b"
"b+deltiv/2")
(("1"
(label "hyplem" -1)
(("1"
(hide "hyplem")
(("1"
(assert)
(("1"
(split +)
(("1"
(expand
"sign_ext")
(("1"
(lift-if)
(("1"
(assert)
(("1"
(split 1)
(("1"
(replace
-9)
(("1"
(assert)
(("1"
(lemma
"poly_intermediate_value_inc")
(("1"
(inst
-
"p(0)"
"0"
"n(0)"
"x"
"b-deltiv/2")
(("1"
(assert)
(("1"
(split
-)
(("1"
(skeep
-1)
(("1"
(inst
-
"cc")
(("1"
(inst
-
"cc")
(("1"
(inst
-
"cc")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
-
"b-deltiv/2")
(("2"
(split
-3)
(("1"
(assert)
(("1"
(hide-all-but
2)
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("3"
(assert)
(("3"
(hide-all-but
2)
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"sign_ext")
(("2"
(lift-if)
(("2"
(assert)
(("2"
(split 1)
(("1"
(propax)
nil
nil)
("2"
(assert)
(("2"
(hide
-2)
(("2"
(split
-)
(("1"
(replace
-7)
(("1"
(assert)
(("1"
(lemma
"poly_intermediate_value_inc")
(("1"
(inst
-
"p(0)"
"0"
"n(0)"
"b+deltiv/2"
"y")
(("1"
(assert)
(("1"
(split
-)
(("1"
(skeep
-1)
(("1"
(inst
-
"cc")
(("1"
(inst
-
"cc")
(("1"
(inst
-
"cc")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
-
"b+deltiv/2")
(("2"
(split
-)
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skeep)
(("2"
(lemma
"poly_strictly_decreasing")
(("2"
(inst
-
"p(0)"
"n(0)"
"x1"
"x2")
(("2"
(assert)
(("2"
(case "n(0)=0")
(("1"
(replaces -1)
(("1"
(expand
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.43 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.
|
