| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Sturm/ (Beweissystem der NASA Version 6.0.9©) Datei vom 6.10.2014 mit Größe 956 kB |
|
Quelle sturmsquarefree.prfSprache: Lisp |
|||||||||||||||
|
(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 (("1" (skeep) (("1" (case "FORALL (j:nat): i-j>=0 IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i-k), n(i-k) (("1" (case "FORALL (j:nat): i+j<=m IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i+k), n(i+k) (("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)<deltiv IMPLIES (abs(b-x1)<del (("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)<deltiv AND abs(x2-b)<deltiv AND x1<x2 IMPLIES polynomial(p( (("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)<deltiv AND abs(x2-b)<deltiv AND x1<x2 IMPLIES polynomial(p( (("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 "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" (assert) 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)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (inst + "min(delta,min(b-x,y-b))") (("1" (hide-all-but (-2 -3 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (lift-if) (("2" (assert) (("2" (split 1) (("1" (propax) nil nil) ("2" (flatten) (("2" (expand "sturm_sequence?") (("2" (flatten) (("2" (inst -7 "b") (("2" (assert) (("2" (case "n(0) = 0") (("1" (replaces -1) (("1" (expand "polynomial" (-3 4)) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "max") (("2" (expand "sign_ext" -7) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("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) ("3" (assert) (("3" (case "n(0) = 0") (("1" (replace -1) (("1" (assert) (("1" (expand "polynomial" (-4 3)) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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 "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals 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) (= const-decl "[T, T -> boolean]" equalities nil) (poly_deriv const-decl "real" polynomials "reals/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (sturm_sequence? const-decl "bool" sturmsquarefree nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (n skolem-const-decl "[nat -> nat]" sturmsquarefree nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (p skolem-const-decl "[nat -> [nat -> real]]" sturmsquarefree nil) (b skolem-const-decl "real" sturmsquarefree nil) (posreal nonempty-type-eq-decl nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (poly_strictly_decreasing formula-decl nil polynomials "reals/") (poly_intermediate_value_inc formula-decl nil polynomials "reals/") (sigma def-decl "real" sigma "reals/") (real_times_real_is_real application-judgement "real" reals nil) (max_nnreal_0 formula-decl nil min_max "reals/") (poly_strictly_increasing formula-decl nil polynomials "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (abs_0_rew formula-decl nil abs_rews "ints/") (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (poly_intermediate_value_dec formula-decl nil polynomials "reals/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (y skolem-const-decl "real" sturmsquarefree nil) (x skolem-const-decl "real" sturmsquarefree nil) (delta skolem-const-decl "posreal" sturmsquarefree nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (max_npreal_0 formula-decl nil min_max "reals/") (poly_continuous formula-decl nil polynomials "reals/")) shostak)) (sturm_lem_no_roots 0 (sturm_lem_no_roots-1 nil 3587229961 ("" (skeep) (("" (name "f" "polynomial(p(0),n(0))") (("" (case "FORALL (j:nat): j<=m IMPLIES number_sign_changes(LAMBDA (i): polynomial(p(i), n(i) number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(y), j)`num AND sign_ext(number_ (("1" (inst - "m") (("1" (expand "sturm_sig") (("1" (assert) nil nil)) nil)) nil) ("2" (induct "j") (("1" (assert) (("1" (split) (("1" (expand "number_sign_changes") (("1" (propax) nil nil)) nil) ("2" (expand "number_sign_changes") (("2" (replace -1) (("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(0)" "0" "n(0)" "x" "y") (("2" (assert) (("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(0)" "0" "n(0)" "x" "y") (("2" (assert) (("2" (split -) (("1" (skeep -1) (("1" (inst - "cc" "0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (split -) (("1" (skeep -1) (("1" (inst - "cc" "0") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (hide-all-but (1 2 3)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (split -) (("1" (skeep -1) (("1" (inst - "cc" "0") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "sign_ext") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 "jj") (("2" (hide 2) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (flatten) (("2" (name "G" "LAMBDA (xx:real): LAMBDA (i): polynomial(p(i),n(i))(xx)") (("2" (copy -1) (("2" (decompose-equality -1) (("2" (inst-cp - "x") (("2" (inst - "y") (("2" (replaces -1) (("2" (replaces -1) (("2" (case "NOT sign_ext(G(x)(1+jj)) = sign_ext(G(y)(1+jj))") (("1" (hide 2) (("1" (expand "G" 1) (("1" (inst-cp - "x" "1+jj") (("1" (inst-cp - "y" "1+jj") (("1" (assert) (("1" (flatten) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "1+jj") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "1+jj") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "number_sign_changes" +) (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (inst - "y" "1+jj") (("1" (assert) (("1" (expand "G" -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "sign_ext" -5) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (inst - "x" "1+jj") (("3" (assert) (("3" (expand "G" -1) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (lift-if) (("4" (assert) nil nil)) nil) ("5" (lift-if) (("5" (assert) nil nil)) nil) ("6" (expand "sign_ext" -5) (("6" (assert) (("6" (lift-if) (("6" (assert) nil nil)) nil)) nil)) nil) ("7" (lift-if) (("7" (assert) nil nil)) nil) ("8" (lift-if) (("8" (lift-if) (("8" (assert) (("8" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("9" (lift-if) (("9" (lift-if) (("9" (lift-if) (("9" (assert) nil nil)) nil)) nil)) nil) ("10" (lift-if) (("10" (assert) nil nil)) nil) ("11" (lift-if) (("11" (lift-if) (("11" (lift-if) (("11" (assert) nil nil)) nil)) nil)) nil) ("12" (lift-if) (("12" (lift-if) (("12" (lift-if) (("12" (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) ((polynomial const-decl "[real -> real]" polynomials "reals/") (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) (= const-decl "[T, T -> boolean]" equalities 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) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (poly_intermediate_value_dec formula-decl nil polynomials "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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (poly_intermediate_value_inc formula-decl nil polynomials "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (G skolem-const-decl "[real -> [nat -> real]]" sturmsquarefree nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sturm_sig const-decl "nat" sturmsquarefree nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NSC type-eq-decl nil number_sign_changes nil) (number_sign_changes def-decl "NSC" number_sign_changes nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/")) shostak)) (sturm_lem_one_root 0 (sturm_lem_one_root-2 nil 3587808579 ("" (case " FORALL (b: real, dd,j, m: nat, n: [nat -> nat], p: [nat -> [nat -> real]], x, y: real): j<=dd AND x < y AND x < b AND b < y AND (FORALL (c: real, i: nat): i <= m AND x <= c AND c <= y AND polynomial(p(i), n(i))(c) = 0 IMPLIES c = b) AND (FORALL (c:real): x<=c AND c<=y AND polynomial(p(0),n(0))(c)=0 IMPLIES (polynomial(p(1),n(1))(c)/=0)) AND j <= m AND polynomial(p(j), n(j))(b) /= 0 AND sturm_sequence?(p, n, m) IMPLIES LET nsc = LAMBDA (xyz: real, pj: nat): number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(xyz), pj) IN sign_ext(nsc(x, j)`lastnz) = sign_ext(nsc(y, j)`lastnz) AND nsc(x, j)`num = nsc(y, j)`num + (IF polynomial(p(0), n(0))(b) = 0 THEN 1 ELSE 0 ENDIF)") (("1" (skeep) (("1" (inst - "b" "j" "j" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -5) (("1" (replace -6) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "dd") (("1" (assert) nil nil) ("2" (skeep) (("2" (assert) (("2" (case "NOT j = 0") (("1" (assert) nil nil) ("2" (hide -2) (("2" (replaces -1) (("2" (expand "number_sign_changes") (("2" (expand "sign_ext" 2) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(0)" "0" "n(0)" "x" "y") (("1" (assert) (("1" (skeep -) (("1" (inst - "cc" "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(0)" "0" "n(0)" "x" "y") (("2" (assert) (("2" (skeep -) (("2" (inst - "cc" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "poly_intermediate_value_dec") (("3" (inst - "p(0)" "0" "n(0)" "x" "y") (("3" (assert) (("3" (skeep -) (("3" (inst - "cc" "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (inst - "x" "0") (("4" (assert) nil nil)) nil) ("5" (inst - "x" "0") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem 1 "jj") (("3" (flatten) (("3" (skeep) (("3" (assert) (("3" (case "NOT j = 1+jj") (("1" (inst - "b" "j" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -6) (("1" (replace -7) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (inst-cp - "x" "jj") (("2" (assert) (("2" (inst-cp - "y" "jj") (("2" (assert) (("2" (inst-cp - "x" "1+jj") (("2" (assert) (("2" (inst-cp - "y" "1+jj") (("2" (assert) (("2" (case "polynomial(p(jj),n(jj))(b)/=0") (("1" (flatten) (("1" (inst - "b" "jj" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -6) (("1" (replace -7) (("1" (flatten) (("1" (split +) (("1" (assert) (("1" (expand "number_sign_changes" +) (("1" (assert) (("1" (hide -2) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "1+jj") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "1+jj") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (invoke (name "SQUAB" "%1") (! 1 2 2)) (("2" (replace -1) (("2" (label "SQUABname" -1) (("2" (hide "SQUABname") (("2" (expand "number_sign_changes" +) (("2" (expand "sign_ext" -1) (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (ground) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "1+jj") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sign_ext") (("2" (lift-if) (("2" (assert) (("2" (ground) (("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "1+jj") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil) ("4" (expand "sign_ext") (("4" (lift-if) (("4" (assert) (("4" (ground) (("4" (lemma "poly_intermediate_value_inc") (("4" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("4" (assert) (("4" (skeep -1) (("4" (inst - "cc" "1+jj") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand "sign_ext") (("5" (lift-if) (("5" (assert) (("5" (ground) (("5" (lemma "poly_intermediate_value_dec") (("5" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("5" (assert) (("5" (skeep -1) (("5" (inst - "cc" "1+jj") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (lift-if) (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (label "hyplem" -2) (("2" (hide "hyplem") (("2" (copy -9) (("2" (expand "sturm_sequence?" -1) (("2" (flatten) (("2" (hide (-1 -2 -3 -5)) (("2" (inst - "b" "jj") (("2" (assert) (("2" (case "jj = 0") (("1" (hide -2) (("1" (replaces -1) (("1" (assert) (("1" (split +) (("1" (expand "number_sign_changes" +) (("1" (lift-if) (("1" (expand "sign_ext" +) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(1)" "0" "n(1)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(1)" "0" "n(1)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "sign_ext(polynomial(p(0),n(0))(x))/=sign_ext(polynomial(p(0),n(0))(y))") (("1" (flatten) (("1" (expand "number_sign_changes" 2) (("1" (expand "number_sign_changes" 2) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(1)" "0" "n(1)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(1)" "0" "n(1)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sturm_seq_first_signs_eq") (("2" (inst - "b" "m" "n" "p" "x" "y") (("2" (assert) (("2" (split -) (("1" (flatten) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(1)" "0" "n(1)" "x" "b") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(1)" "0" "n(1)" "x" "b") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "c" "0") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "sign_ext" -1) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lemma "square_free_max") (("1" (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" (inst - "p(0)" "min(y-b,b-x)" "b" "0" "n(0)") (("1" (assert) (("1" (split -) (("1" (copy -12) (("1" (expand "sturm_sequence?" -1) (("1" (flatten) (("1" (hide -2) (("1" (inst -2 "b") (("1" (assert) (("1" (expand "max" -2) (("1" (expand "sign_ext" -2) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "x!1 = b") (("1" (assert) nil nil) ("2" (case "x!1 < b") (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(0)" "0" "n(0)" "x" "x!1") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(0)" "0" "n(0)" "x!1" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (expand "min" 1) (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "square_free_min") (("2" (inst - "p(0)" "min(y-b,b-x)" "b" "0" "n(0)") (("1" (assert) (("1" (split -) (("1" (copy -10) (("1" (expand "sturm_sequence?" -1) (("1" (flatten) (("1" (hide -2) (("1" (inst -2 "b") (("1" (assert) (("1" (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" (expand "max" -2) (("2" (assert) (("2" (expand "sign_ext" -2) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "x!1 = b") (("1" (assert) nil nil) ("2" (case "x!1 < b") (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(0)" "0" "n(0)" "x" "x!1") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(0)" "0" "n(0)" "x!1" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "n(0) = 0") (("1" (replaces -1) (("1" (expand "polynomial" (-1 +)) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("3" (expand "min" 1) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "polynomial(p(jj - 1), n(jj - 1))(b) /= 0") (("1" (case "sign_ext(polynomial(p(jj - 1), n(jj - 1))(b))=sign_ext(polynomial(p(jj - 1), n(jj - 1))(x (("1" (flatten) (("1" (case "sign_ext(polynomial(p(1 + jj), n(1 + jj))(b))=sign_ext(polynomial(p(1 + jj), n(1 + jj))(x (("1" (flatten) (("1" (assert) (("1" (split +) (("1" (expand "number_sign_changes" 1) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (invoke (name "SQUAB" "%1") (! 1 2 2)) (("2" (replaces -1) (("2" (case "sign_ext(polynomial(p(jj), n(jj))(x)) = - sign_ext(polynomial(p(jj), n(jj))(y))") (("1" (case "number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), jj-1)`num = number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(y), jj-1)`num + SQUAB") (("1" (expand "sign_ext") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "number_sign_changes" +) (("1" (expand "number_sign_changes" +) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "number_sign_changes" (-1 +)) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "number_sign_changes" -1) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lift-if) (("3" (assert) (("3" (ground) (("3" (expand "number_sign_changes" -1) (("3" (assert) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "number_sign_changes" +) (("2" (expand "number_sign_changes" +) (("2" (expand "sign_ext") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "number_sign_changes" 1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "number_sign_changes" -1) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lift-if) (("3" (assert) (("3" (ground) (("3" (expand "number_sign_changes" -1) (("3" (assert) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "number_sign_changes" -1) (("4" (assert) (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (lift-if) (("5" (assert) (("5" (split -2) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (split -2) (("1" (propax) nil nil) ("2" (flatten) (("2" (expand "number_sign_changes" 1) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "number_sign_changes" +) (("3" (expand "number_sign_changes" +) (("3" (expand "sign_ext") (("3" (lift-if) (("3" (lift-if) (("3" (lift-if) (("3" (assert) (("3" (ground) (("1" (lift-if) (("1" (split 2) (("1" (flatten) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (expand "number_sign_changes" -1) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "number_sign_changes" -2) (("3" (assert) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (expand "number_sign_changes" -1) (("4" (assert) (("4" (lift-if) (("4" (assert) nil nil)) nil)) nil)) nil) ("5" (lift-if) (("5" (split -1) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (split -2) (("1" (flatten) (("1" (expand "number_sign_changes" -1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "number_sign_changes" +) (("4" (expand "number_sign_changes" +) (("4" (expand "sign_ext") (("4" (lift-if) (("4" (lift-if) (("4" (lift-if) (("4" (assert) (("4" (ground) (("1" (lift-if) (("1" (split 2) (("1" (propax) nil nil) ("2" (flatten) (("2" (expand "number_sign_changes" 1) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "number_sign_changes" -1) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lift-if) (("3" (split -) (("1" (flatten) (("1" (expand "number_sign_changes" -1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (split -) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "hyplem") (("2" (inst?) (("2" (inst - "jj-1") (("2" (assert) (("2" (replace -13) (("2" (replace -14) (("2" (flatten) (("2" (expand "SQUAB") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT sign_ext(polynomial(p(jj), n(jj))(x)) = sign_ext(polynomial(p(jj), n(jj))(y))") (("1" (expand "sign_ext" (1 2)) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (case "number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), jj-1)`num = number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(y), jj-1)`num + SQUAB") (("1" (expand "sign_ext") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "number_sign_changes" +) (("1" (expand "number_sign_changes" +) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (assert) (("2" (split -) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("3" (expand "number_sign_changes" -1) (("3" (assert) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (lift-if) (("4" (split -) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "number_sign_changes" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "number_sign_changes" +) (("2" (expand "number_sign_changes" +) (("2" (expand "sign_ext") (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (assert) (("2" (split -) (("1" (split 2) (("1" (propax) nil nil) ("2" (expand "number_sign_changes" -1) (("2" (assert) (("2" (lift-if) (("2" (expand "number_sign_changes" 1) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil) ("3" (expand "number_sign_changes" -1) (("3" (assert) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (lift-if) (("4" (split -) (("1" (split 2) (("1" (propax) nil nil) ("2" (flatten) (("2" (expand "number_sign_changes" 1) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split +) (("1" (propax) nil nil) ("2" (flatten) (("2" (expand "number_sign_changes" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "number_sign_changes" +) (("3" (expand "number_sign_changes" +) (("3" (expand "sign_ext") (("3" (lift-if) (("3" (lift-if) (("3" (lift-if) (("3" (assert) (("3" (ground) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (split 2) (("1" (flatten) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("3" (expand "number_sign_changes" -1) (("3" (assert) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (lift-if) (("4" (split +) (("1" (flatten) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "number_sign_changes" +) (("4" (expand "number_sign_changes" +) (("4" (expand "sign_ext") (("4" (lift-if) (("4" (lift-if) (("4" (lift-if) (("4" (assert) (("4" (ground) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lift-if) (("2" (split -) (("1" (flatten) (("1" (expand "number_sign_changes" -1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (split -) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "number_sign_changes" -1) (("3" (assert) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (lift-if) (("4" (split -) (("1" (flatten) (("1" (expand "number_sign_changes" -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (split -) (("1" (expand "number_sign_changes" -1) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "number_sign_changes" 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) ("2" (assert) (("2" (hide 2) (("2" (reveal "hyplem") (("2" (inst?) (("2" (inst - "jj-1") (("2" (assert) (("2" (replace -13) (("2" (replace -14) (("2" (flatten) (("2" (expand "SQUAB") (("2" (propax) 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 (x1,x2:real): x<=x1 AND x1<x2 AND x2<=y IMPLIES sign_ext(polynomial(p(1 + jj), n(1 + jj) sign_ext(polynomial(p(1 + jj), n(1 + jj))(x2))") (("1" (inst-cp - "x" "b") (("1" (inst - "b" "y") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (label "squiggy" 9) (("2" (hide "squiggy") (("2" (expand "sign_ext" 1) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(1+jj)" "0" "n(1+jj)" "x1" "x2") (("1" (assert) (("1" (skeep -) (("1" (inst - "cc" "1+jj") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(1+jj)" "0" "n(1+jj)" "x1" "x2") (("2" (assert) (("2" (skeep -) (("2" (inst - "cc" "1+jj") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "x2") (("3" (inst - "x2" "1+jj") (("3" (assert) nil nil)) nil)) nil) ("4" (inst - "x1" "1+jj") (("4" (assert) nil nil)) nil) ("5" (inst - "x1" "1+jj") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "squiggy" 8) (("2" (hide "squiggy") (("2" (case "FORALL (x1,x2:real): x<=x1 AND x1<x2 AND x2<=y IMPLIES sign_ext(polynomial(p(jj - 1), n(jj - 1) sign_ext(polynomial(p(jj - 1), n(jj - 1))(x2))") (("1" (inst-cp - "x" "b") (("1" (inst - "b" "y") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "sign_ext" 1) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(jj-1)" "0" "n(jj-1)" "x1" "x2") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "jj-1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(jj-1)" "0" "n(jj-1)" "x1" "x2") (("2" (assert) (("2" (skeep -) (("2" (inst - "cc" "jj-1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "x2" "jj-1") (("3" (assert) nil nil)) nil) ("4" (inst - "x1" "jj-1") (("4" (assert) nil nil)) nil) ("5" (inst - "x1" "jj-1") (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide 7) (("2" (lemma "sturm_seq_repeated_root") (("2" (inst - "m" "n" "p" "b") (("2" (assert) (("2" (inst - "jj-1") (("2" (assert) (("2" (inst - "jj+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)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (sturm_seq_repeated_root formula-decl nil sturmsquarefree nil) (minus_real_is_real application-judgement "real" reals nil) (SQUAB skolem-const-decl "naturalnumber" sturmsquarefree nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (sturm_seq_first_signs_eq formula-decl nil sturmsquarefree nil) (square_free_min formula-decl nil more_polynomial_props "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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (square_free_max formula-decl nil more_polynomial_props "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (y skolem-const-decl "real" sturmsquarefree nil) (b skolem-const-decl "real" sturmsquarefree nil) (x skolem-const-decl "real" sturmsquarefree nil) (> const-decl "bool" reals nil) (n skolem-const-decl "[nat -> nat]" sturmsquarefree nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posreal nonempty-type-eq-decl nil real_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (max_nnreal_0 formula-decl nil min_max "reals/") (abs_nat_rew formula-decl nil abs_rews "ints/") (real_times_real_is_real application-judgement "real" reals nil) (sigma def-decl "real" sigma "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_gt_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_intermediate_value_inc formula-decl nil polynomials "reals/") (poly_intermediate_value_dec formula-decl nil polynomials "reals/") (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (/= const-decl "boolean" notequal nil) (sturm_sequence? const-decl "bool" sturmsquarefree nil) (NSC type-eq-decl nil number_sign_changes nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (number_sign_changes def-decl "NSC" number_sign_changes nil)) nil) (sturm_lem_one_root-1 nil 3587808541 ("" (case " FORALL (b: real, dd,j, m: nat, n: [nat -> nat], p: [nat -> [nat -> real]], x, y: real): j<=dd AND x < y AND x < b AND b < y AND (FORALL (c: real, i: nat): i <= m AND x <= c AND c <= y AND polynomial(p(i), n(i))(c) = 0 IMPLIES c = b) AND (FORALL (c:real): x<=c AND c<=y AND polynomial(p(0),n(0))(c)=0 IMPLIES (polynomial(p(1),n(1))(c)/=0)) AND j + 1 <= m AND polynomial(p(j + 1), n(j + 1))(b) /= 0 AND sturm_sequence?(p, n, m) IMPLIES LET nsc = LAMBDA (xyz: real, pj: nat): number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(xyz), pj) IN sign_ext(nsc(x, j + 1)`lastnz) = sign_ext(nsc(y, j + 1)`lastnz) AND nsc(x, j + 1)`num - nsc(x, 1)`num = nsc(y, j + 1)`num - nsc(y, 1)`num") (("1" (skeep) (("1" (inst - "b" "j" "j" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -5) (("1" (replace -6) (("1" (propax) nil))))))))))) ("2" (hide 2) (("2" (induct "dd") (("1" (assert) nil) ("2" (skeep) (("2" (assert) (("2" (case "NOT j = 0") (("1" (assert) nil) ("2" (hide -2) (("2" (replaces -1) (("2" (expand "number_sign_changes") (("2" (expand "number_sign_changes") (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (case "NOT sign_ext(polynomial(p(1), n(1))(y)) = sign_ext(polynomial(p(1), n(1))(x))") (("1" (hide 3) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(1)" "0" "n(1)" "x" "y") (("1" (assert) (("1" (skeep -) (("1" (inst - "cc" "1") (("1" (assert) nil))))))))))) ("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(1)" "0" "n(1)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "1") (("2" (assert) nil))))))))))) ("3" (lemma "poly_intermediate_value_inc") (("3" (inst - "p(1)" "0" "n(1)" "x" "y") (("3" (assert) (("3" (skeep -1) (("3" (inst - "cc" "1") (("3" (assert) nil))))))))))) ("4" (lemma "poly_intermediate_value_inc") (("4" (inst - "p(1)" "0" "n(1)" "x" "y") (("4" (assert) (("4" (skeep -1) (("4" (inst - "cc" "1") (("4" (assert) nil))))))))))) ("5" (lemma "poly_intermediate_value_dec") (("5" (inst - "p(1)" "0" "n(1)" "x" "y") (("5" (assert) (("5" (skeep -) (("5" (inst - "cc" "1") (("5" (assert) nil))))))))))))))))))))))))))) ("2" (assert) (("2" (case "polynomial(p(1), n(1))(x) = 0") (("1" (inst - "x" "1") (("1" (assert) nil))) ("2" (case "polynomial(p(0), n(0))(x) = 0") (("1" (inst - "x" "0") (("1" (assert) nil))) ("2" (case "polynomial(p(0), n(0))(y) = 0") (("1" (inst - "y" "0") (("1" (assert) nil))) ("2" (case "polynomial(p(1), n(1))(y) = 0") (("1" (inst - "y" "1") (("1" (assert) nil))) ("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))) ("3" (skolem 1 "jj") (("3" (flatten) (("3" (skeep) (("3" (assert) (("3" (case "NOT j = 1+jj") (("1" (inst - "b" "j" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -6) (("1" (replace -7) (("1" (propax) nil))))))))) ("2" (replace -1) (("2" (assert) (("2" (inst-cp - "x" "1+jj") (("2" (assert) (("2" (inst-cp - "y" "1+jj") (("2" (assert) (("2" (inst-cp - "x" "2+jj") (("2" (assert) (("2" (inst-cp - "y" "2+jj") (("2" (assert) (("2" (case "polynomial(p(1+jj),n(1+jj))(b)/=0") (("1" (flatten) (("1" (inst - "b" "j-1" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -7) (("1" (replace -8) (("1" (flatten) (("1" (split +) (("1" (replace -1) (("1" (assert) (("1" (expand "number_sign_changes" +) (("1" (assert) (("1" (hide (-2 -3)) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(2+jj)" "0" "n(2+jj)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "2+jj") (("1" (assert) nil))))))))))) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(2+jj)" "0" "n(2+jj)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "2+jj") (("2" (assert) nil))))))))))))))))))))))))))))))))) ("2" (expand "number_sign_changes" + (1 3)) (("2" (assert) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lemma "number_sign_changes_lastnz_nonzero") (("1" (copy -2) (("1" (rewrite -2 -1) (("1" (inst-cp - "0") (("1" (inst - "1") (("1" (assert) (("1" (inst -13 "y") (("1" (assert) nil))))))))))))))) ("2" (expand "number_sign_changes" 2) (("2" (lift-if) (("2" (assert) (("2" (expand "number_sign_changes" -1) (("2" (lift-if) (("2" (case "FORALL (pj:nat): pj=1+jj OR pj = 2+jj IMPLIES sign_ext(polynomial(p(pj), n(pj))(x)) = sign (("1" (inst-cp - "1+jj") (("1" (inst - "2+jj") (("1" (assert) nil))))) ("2" (hide (-1 -2 -3 -4 2 3)) (("2" (skeep) (("2" (expand "sign_ext" 1) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (split +) (("1" (propax) nil) ("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(pj)" "0" "n(pj)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "pj") (("2" (ground) nil))))))))))))))) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (split +) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(pj)" "0" "n(pj)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "pj") (("1" (ground) nil))))))))))) ("2" (flatten) (("2" (split +) (("1" (propax) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(pj)" "0" "n(pj)" "x" "y") (("2" (assert) nil))))))))))))) ("2" (flatten) (("2" (split +) (("1" (ground) nil) ("2" (flatten) (("2" (ground) nil))))))))))))))))))))))))))))))))))))))))))) ("3" (lemma "number_sign_changes_lastnz_nonzero") (("3" (copy -2) (("3" (rewrite -2 -1) (("3" (inst-cp - "0") (("3" (inst - "1") (("3" (assert) (("3" (inst -13 "x") (("3" (assert) nil))))))))))))))) ("4" (expand "number_sign_changes" 2) (("4" (lift-if) (("4" (expand "number_sign_changes" -1) (("4" (lift-if) (("4" (case "FORALL (pj:nat): pj=1+jj OR pj = 2+jj IMPLIES sign_ext(polynomial(p(pj), n(pj))(x)) = sign (("1" (inst-cp - "1+jj") (("1" (inst - "2+jj") (("1" (ground) nil))))) ("2" (hide (-1 -2 -3 -4 2 3)) (("2" (skeep) (("2" (expand "sign_ext" 1) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (split +) (("1" (propax) nil) ("2" (lemma "poly_intermediate_value_inc") (("2" (inst - "p(pj)" "0" "n(pj)" "x" "y") (("2" (assert) (("2" (skeep -1) (("2" (inst - "cc" "pj") (("2" (ground) nil))))))))))))))) ("2" (flatten) (("2" (assert) (("2" (split +) (("1" (flatten) (("1" (split +) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(pj)" "0" "n(pj)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "pj") (("1" (ground) nil))))))))))) ("2" (flatten) (("2" (split +) (("1" (propax) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(pj)" "0" "n(pj)" "x" "y") (("2" (assert) nil))))))))))))) ("2" (flatten) (("2" (split +) (("1" (ground) nil) ("2" (flatten) (("2" (ground) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (flatten) (("2" (label "hyplem" -3) (("2" (hide "hyplem") (("2" (copy -10) (("2" (expand "sturm_sequence?" -1) (("2" (flatten) (("2" (hide (-1 -2 -4)) (("2" (inst - "b" "1+jj") (("2" (assert) (("2" (case "polynomial(p(jj), n(jj))(b) = 0") (("1" (replaces -1) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (assert) nil))))))) ("2" (inst-cp - "x" "jj") (("2" (inst-cp - "y" "jj") (("2" (assert) (("2" (case "FORALL (pj:nat,x1,x2:real): ((pj=jj OR pj = 2+jj) AND (x<=x1 AND x1<=y AND x<=x2 AND x2<=y)) IMPLI (("1" (inst-cp - "jj" "x" "b") (("1" (inst-cp - "jj" "b" "y") (("1" (inst-cp - "2+jj" "x" "b") (("1" (inst - "2+jj" "b" "y") (("1" (assert) (("1" (split +) (("1" (expand "number_sign_changes" 1) (("1" (lift-if) (("1" (assert) nil))))) ("2" (case "jj = 0") (("1" (replaces -1) (("1" (assert) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (case "polynomial(p(1), n(1))(x) > 0") (("1" (case "polynomial(p(1), n(1))(y) < 0") (("1" (case "NOT number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), 1)`num = 0") (("1" (expand "number_sign_changes" 1) (("1" (assert) (("1" (expand "number_sign_changes" 1) (("1" (expand "sign_ext" 1) (("1" (propax) nil))))))))) ("2" (case "NOT number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(y), 1)`num = 1") (("1" (expand "number_sign_changes" 1) (("1" (expand "number_sign_changes" 1) (("1" (expand "sign_ext" 1) (("1" (assert) nil))))))) ("2" (case "NOT number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(x), 2)`num = 1") (("1" (expand "number_sign_changes" 1) (("1" (expand "number_sign_changes" 1) (("1" (expand "number_sign_changes" 1) (("1" (expand "sign_ext" 1) (("1" (assert) nil))))))))) ("2" (case "NOT number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(y), 2)`num = 1") (("1" (expand "number_sign_changes" 1) (("1" (expand "number_sign_changes" 1) (("1" (expand "number_sign_changes" 1) (("1" (expand "sign_ext" 1) (("1" (assert) nil))))))))) ("2" (assert) (("2" (postpone) nil))))))))))) ("2" (postpone) nil))) ("2" (postpone) nil))) ("2" (postpone) nil))))))))))))))))) ("2" (postpone) nil))))))))))))))) ("2" (postpone) nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) nil) nil nil)) (sturm_lem_edge_root 0 (sturm_lem_edge_root-1 nil 3587920247 ("" (case "FORALL (dd,j, m: nat, n: [nat -> nat], p: [nat -> [nat -> real]], x, y: real): j<=dd AND x < y AND (FORALL (c: real, i: nat): i <= m AND x <= c AND c <= y AND polynomial(p(i), n(i))(c) = 0 IMPLIES c = y) AND (FORALL (c: real): x <= c AND c <= y AND polynomial(p(0), n(0))(c) = 0 IMPLIES (polynomial(p(1), n(1))(c) /= 0)) AND j<= m AND polynomial(p(j), n(j))(y) /= 0 AND sturm_sequence?(p, n, m) AND p(1) = poly_deriv(p(0)) AND n(1) = n(0) - 1 IMPLIES LET nsc = LAMBDA (xyz: real, pj: nat): number_sign_changes(LAMBDA (i): polynomial(p(i), n(i))(xyz), pj) IN sign_ext(nsc(x, j)`lastnz) = sign_ext(nsc(y, j)`lastnz) AND nsc(x, j)`num = nsc(y, j)`num + (IF polynomial(p(0), n(0))(y) = 0 THEN 1 ELSE 0 ENDIF)") (("1" (skeep) (("1" (inst - "j" "j" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -3) (("1" (replace -4) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "dd") (("1" (assert) nil nil) ("2" (skeep) (("2" (assert) (("2" (case "NOT j = 0") (("1" (assert) nil nil) ("2" (hide -2) (("2" (replaces -1) (("2" (expand "number_sign_changes") (("2" (expand "sign_ext" 2) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(0)" "0" "n(0)" "x" "y") (("1" (assert) (("1" (skeep -) (("1" (inst - "cc" "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(0)" "0" "n(0)" "x" "y") (("2" (assert) (("2" (skeep -) (("2" (inst - "cc" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "x" "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem 1 "jj") (("3" (flatten) (("3" (skeep) (("3" (assert) (("3" (case "NOT j = 1+jj") (("1" (inst - "j" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -4) (("1" (replace -5) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (replaces -1) (("2" (assert) (("2" (inst-cp - "x" "jj") (("2" (assert) (("2" (inst-cp - "x" "1+jj") (("2" (assert) (("2" (case "polynomial(p(jj),n(jj))(y)/=0") (("1" (flatten) (("1" (inst - "jj" "m" "n" "p" "x" "y") (("1" (assert) (("1" (replace -4) (("1" (replace -5) (("1" (flatten) (("1" (split +) (("1" (assert) (("1" (expand "number_sign_changes" +) (("1" (assert) (("1" (hide -2) (("1" (expand "sign_ext" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("1" (assert) (("1" (skeep -1) (("1" (inst - "cc" "1+jj") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_intermediate_value_dec") (("2" (inst - "p(1+jj)" "0" "n(1+jj)" "x" "y") (("2" (assert) (("2" (skeep -1) --> -------------------- --> maximum size reached --> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.738Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26