| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Tarski/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 416 kB |
|
SSL compute_sturm_tarski.prfSprache: Lisp |
|||||||||||||||
|
(compute_sturm_tarski (der_prod_TCC1 0 (der_prod_TCC1-1 nil 3619442978 ("" (subtype-tcc) nil nil) nil nil)) (der_prod_TCC2 0 (der_prod_TCC2-1 nil 3619442978 ("" (skeep) (("" (expand "polynomial_prod") (("" (assert) (("" (case "FORALL (abc:[nat->int],i1,i2:nat): rational_pred(sigma(i1,i2,abc)) AND integer_ (("1" (inst?) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "poly_deriv") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (induct "i2") (("1" (skeep) (("1" (expand "sigma") (("1" (lift-if) (("1" (assert) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "abc" "i1") (("2" (flatten) (("2" (expand "sigma" +) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lemma "integers.closed_plus") (("2" (inst?) (("2" (assert) (("2" (lemma "rationals.closed_plus") (("2" (inst?) (("2" (assert) 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) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (polynomial_prod const-decl "real" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (a skolem-const-decl "[nat -> int]" compute_sturm_tarski nil) (g skolem-const-decl "[nat -> int]" compute_sturm_tarski nil) (i skolem-const-decl "nat" compute_sturm_tarski nil) (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (poly_deriv const-decl "real" polynomials "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (real_times_real_is_real application-judgement "real" reals nil) (closed_plus formula-decl nil integers nil) (rat nonempty-type-eq-decl nil rationals nil) (closed_plus formula-decl nil rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (finite_bij_real_remove_one 0 (finite_bij_real_remove_one-1 nil 3594487196 ("" (skeep) (("" (case "NOT m-1>=0") (("1" (hide 2) (("1" (expand "bijective?") (("1" (flatten) (("1" (expand "surjective?") (("1" (inst - "x") (("1" (assert) (("1" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (copy -2) (("2" (expand "bijective?" -1) (("2" (flatten) (("2" (copy -2) (("2" (expand "surjective?" -1) (("2" (inst - "x") (("2" (skolem -1 "ii") (("2" (inst + "LAMBDA (i:below(m-1)): IF i<ii THEN bij(i) ELSE bij(i+1) ENDIF") (("1" (expand "bijective?" +) (("1" (split +) (("1" (expand "injective?" 1) (("1" (skeep) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (expand "injective?" -3) (("1" (ground) (("1" (inst - "x1" "x2") (("1" (assert) nil nil)) nil) ("2" (inst - "x1" "1+x2") (("2" (assert) nil nil)) nil) ("3" (inst - "1+x1" "x2") (("3" (assert) nil nil)) nil) ("4" (inst - "1+x1" "1+x2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skeep) (("2" (typepred "y") (("2" (inst - "y") (("2" (assert) (("2" (skolem - "jj") (("2" (case "ii = jj") (("1" (expand "injective?") (("1" (inst - "ii" "jj") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (case "jj<ii") (("1" (inst + "jj") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (inst + "jj-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "injective?") (("2" (skeep) (("2" (inst - "1+i" "ii") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "injective?") (("3" (skeep) (("3" (inst - "i" "ii") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nat nonempty-type-eq-decl nil naturalnumbers 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (x skolem-const-decl "real" compute_sturm_tarski nil) (A skolem-const-decl "set[real]" compute_sturm_tarski nil) (set type-eq-decl nil sets nil) (int_plus_int_is_int application-judgement "int" integers nil) (jj skolem-const-decl "below(m)" compute_sturm_tarski nil) (injective? const-decl "bool" functions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (m skolem-const-decl "nat" compute_sturm_tarski nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (ii skolem-const-decl "below(m)" compute_sturm_tarski nil) (/= const-decl "boolean" notequal nil) (bij skolem-const-decl "[below(m) -> (A)]" compute_sturm_tarski nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (finite_bij_real_remove_two 0 (finite_bij_real_remove_two-1 nil 3594488379 ("" (case "FORALL (x, y: real, m: nat, A: set[real], bij: [below(m) -> (A)],i,j:below(m)): bijective?(bij) AND A(x) AND A(y) AND x /= y AND i<j AND bij(i)=x AND bij(j)=y IMPLIES m - 2 >= 0 AND (EXISTS (bijec: [below(m - 2) -> {r: (A) | r /= x AND r /= y}]): bijective?(bijec))") (("1" (skeep) (("1" (copy -2) (("1" (expand "bijective?" -1) (("1" (flatten) (("1" (expand "surjective?" -2) (("1" (inst-cp - "x") (("1" (inst - "y") (("1" (skosimp*) (("1" (case "x!1 < x!2") (("1" (inst - "y" "x" "m" "A" "bij" "x!1" "x!2") (("1" (assert) (("1" (skosimp*) (("1" (inst + "bijec!1") (("1" (assert) (("1" (expand "bijective?" (-5 2)) (("1" (flatten) (("1" (split) (("1" (expand "injective?" (-5 1)) (("1" (propax) nil nil)) nil) ("2" (expand "surjective?" (-6 1)) (("2" (skosimp*) (("2" (inst - "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "x" "y" "m" "A" "bij" "x!2" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (case "NOT m-2>=0") (("1" (hide 3) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (inst + "LAMBDA (ii:below(m-2)): IF ii<i THEN bij(ii) ELSIF ii+1 < j THEN bij(ii+1) ELSE bij(ii+2) ENDIF (("1" (expand "bijective?") (("1" (flatten) (("1" (split) (("1" (expand "injective?") (("1" (skosimp*) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (inst - "x1!1" "x2!1") (("1" (assert) nil nil)) nil) ("2" (inst - "x1!1" "1+x2!1") (("2" (assert) nil nil)) nil) ("3" (inst - "x1!1" "2+x2!1") (("3" (assert) nil nil)) nil) ("4" (inst - "1+x1!1" "x2!1") (("4" (assert) nil nil)) nil) ("5" (inst - "1+x1!1" "1+x2!1") (("5" (assert) nil nil)) nil) ("6" (inst - "1+x1!1" "2+x2!1") (("6" (assert) nil nil)) nil) ("7" (inst - "2+x1!1" "x2!1") (("7" (assert) nil nil)) nil) ("8" (inst - "2+x1!1" "1+x2!1") (("8" (assert) nil nil)) nil) ("9" (inst - "2+x1!1" "2+x2!1") (("9" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (inst - "y!1") (("2" (skosimp*) (("2" (case "x!1 = i OR x!1 = j") (("1" (ground) nil nil) ("2" (flatten) (("2" (name "ii" "x!1") (("2" (replaces -1) (("2" (assert) (("2" (case "ii < i") (("1" (inst + "ii") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (case "ii-1<j") (("1" (inst + "ii-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (inst + "ii-2") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "bijective?") (("2" (flatten) (("2" (assert) (("2" (expand "injective?") (("2" (inst-cp - "i" "2+ii!1") (("2" (assert) (("2" (assert) (("2" (inst-cp - "j" "2+ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skeep) (("3" (expand "bijective?") (("3" (flatten) (("3" (expand "injective?") (("3" (inst-cp - "1+ii" "i") (("3" (assert) (("3" (assert) (("3" (inst-cp - "1+ii" "j") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "bijective?") (("4" (flatten) (("4" (expand "injective?") (("4" (skeep) (("4" (inst-cp - "ii" "i") (("4" (assert) (("4" (assert) (("4" (inst - "ii" "j") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (m skolem-const-decl "nat" compute_sturm_tarski nil) (i skolem-const-decl "below(m)" compute_sturm_tarski nil) (A skolem-const-decl "set[real]" compute_sturm_tarski nil) (bij skolem-const-decl "[below(m) -> (A)]" compute_sturm_tarski nil) (x skolem-const-decl "real" compute_sturm_tarski nil) (y skolem-const-decl "real" compute_sturm_tarski nil) (j skolem-const-decl "below(m)" compute_sturm_tarski nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (int_plus_int_is_int application-judgement "int" integers nil) (ii skolem-const-decl "below(m)" compute_sturm_tarski nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (surjective? const-decl "bool" functions nil) (y skolem-const-decl "real" compute_sturm_tarski nil) (real_ge_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) (injective? const-decl "bool" functions nil) (x skolem-const-decl "real" compute_sturm_tarski nil) (A skolem-const-decl "set[real]" compute_sturm_tarski nil) (int_minus_int_is_int application-judgement "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) (set type-eq-decl nil sets nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bijective? const-decl "bool" functions nil) (/= const-decl "boolean" notequal nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (computed_sturm_spec_TCC1 0 (computed_sturm_spec_TCC1-1 nil 3593788550 ("" (skeep) (("" (assert) (("" (expand "der_prod") (("" (expand "polynomial_prod") (("" (expand "max") (("" (expand "sigma") (("" (expand "sigma") (("" (expand "poly_deriv") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (polynomial_prod const-decl "real" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (poly_deriv const-decl "real" polynomials "reals/") (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (der_prod const-decl "int" compute_sturm_tarski nil)) nil)) (computed_sturm_spec_TCC2 0 (computed_sturm_spec_TCC2-1 nil 3593788550 ("" (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 "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide "Sturm/") (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (nonzero_version const-decl "list[int]" gcd_coeff "Sturm/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (der_prod const-decl "int" compute_sturm_tarski nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence "Sturm/") (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (/= const-decl "boolean" notequal nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (computed_sturm_spec_TCC3 0 (computed_sturm_spec_TCC3-1 nil 3593788550 ("" (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 "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (nonzero_version const-decl "list[int]" gcd_coeff "Sturm/") (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide "Sturm/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (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_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (der_prod const-decl "int" compute_sturm_tarski nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence "Sturm/") (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (/= const-decl "boolean" notequal nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (computed_sturm_spec_TCC4 0 (computed_sturm_spec_TCC4-1 nil 3593788550 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (computed_sturm_spec_TCC5 0 (computed_sturm_spec_TCC5-1 nil 3593790499 ("" (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 "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide "Sturm/") (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (nonzero_version const-decl "list[int]" gcd_coeff "Sturm/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (der_prod const-decl "int" compute_sturm_tarski nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence "Sturm/") (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (/= const-decl "boolean" notequal nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (computed_sturm_spec 0 (computed_sturm_spec-1 nil 3593788956 ("" (skeep) (("" (name "sl" "remainder_seq(a, n, der_prod(a, n, g, k), n - 1 + k)") (("" (replace -1) (("" (name "P" "LAMBDA (j: nat): IF j < length(sl) THEN list2array[int](0)(nth(sl, length(sl) - 1 - j)) ELSE (LAMBDA (i: nat): 0) ENDIF") (("1" (replaces -1) (("1" (name "N" " LAMBDA (j: nat): IF j < length(sl) THEN max(length(nth(sl, length(sl) - 1 - j)) - 1, 0) ELSE 0 ENDIF") (("1" (name "M" "length(sl)-1") (("1" (replace -1) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (replace -3) (("1" (split +) (("1" (copy 2) (("1" (hide 3) (("1" (expand "constructed_sturm_sequence?") (("1" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (skeep) (("1" (expand "P" -1) (("1" (expand "N" -1) (("1" (assert) (("1" (expand "max" -1) (("1" (lift-if) (("1" (assert) (("1" (split -) (("1" (flatten) (("1" (case "NOT length(sl)-1-i = 0") (("1" (assert) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (inst - "0" "length(sl)-1-i") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (typepred "sl") (("2" (hide -1) (("2" (expand "is_neg_remainder_list?") (("2" (flatten) (("2" (inst - "length(sl)-1-i") (("2" (assert) (("2" (lemma "list2array_sound[int]") (("2" (inst - "nth(sl,length(sl)-1-i)" "0" "length(nth(sl, length(sl) - 1 - i)) - 1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "frizzy1" -1) (("2" (assert) (("2" (replace -1) (("2" (hide "frizzy1") (("2" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (skeep) (("1" (expand "N" 1) (("1" (expand "max" 1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?" -1) (("1" (flatten) (("1" (inst - "length(sl)-1-j" "length(sl)-1-i") (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sl") (("2" (hide -1) (("2" (expand "is_neg_remainder_list?" -1) (("2" (flatten) (("2" (inst - "0" "length(sl)-1-j") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "sl") (("3" (hide -1) (("3" (expand "is_neg_remainder_list?" -1) (("3" (flatten) (("3" (inst - "length(sl)-1-j" "length(sl)-1-i") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (label "frizzy2" -1) (("2" (hide "frizzy2") (("2" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?" -1) (("1" (flatten) (("1" (assert) (("1" (expand "N" 1) (("1" (expand "max" 1) (("1" (replace -3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (label "frizzy2" -1) (("2" (hide "frizzy2") (("2" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?" -1) (("1" (flatten) (("1" (expand "P" 1) (("1" (replace -4) (("1" (replace -3) (("1" (decompose-equality 1) (("1" (lemma "list2array_sound[int]") (("1" (inst?) (("1" (replace -1) (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (expand "der_prod") (("1" (typepred "array2list[int] (k + n) (LAMBDA (i: nat): polynomial_prod(g, k, poly_deriv(a), n - 1)(i))") (("1" (replace -2) (("1" (inst - "x!1") (("1" (replace -3 :dir rl) (("1" (assert) (("1" (expand "poly_deriv" 1) (("1" (expand "polynomial_prod" 1) (("1" (case "NOT N(0)=n") (("1" (hide 2) (("1" (expand "N" 1) (("1" (expand "max" 1) (("1" (replace -8) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (rewrite "sigma_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (lemma "list2array_sound[int]") (("1" (case "NOT 1 - n!1 + x!1 >= 0") (("1" (assert) nil nil) ("2" (inst?) (("2" (assert) (("2" (replace -2 +) (("2" (typepred "array2list[int](1+n)(a)") (("2" (inst - "1-n!1+x!1") (("2" (replaces -2) (("2" (replaces -3) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide (-1 -2 -3 -4 -5)) (("2" (skeep) (("2" (typepred "der_prod(a,n,g,k)(i)") (("2" (expand "der_prod" -1) (("2" (assert) (("2" (case "FORALL (jj:int): rational_pred(jj)") (("1" (inst - "der_prod(a,n,g,k)(i)") (("1" (expand "der_prod") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (case "x!1 < k+n") (("1" (assert) nil nil) ("2" (case "NOT N(0)=n") (("1" (expand "N" 1) (("1" (expand "max" 1) (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "polynomial_prod" +) (("2" (rewrite "sigma_restrict_eq_0" +) (("1" (hide 4) (("1" (skeep) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 -5)) (("2" (skeep) (("2" (assert) (("2" (typepred "der_prod((list2array[int] (0)(array2list[int](1 + n)(a))),n,g,k)(x1)") (("2" (typepred "der_prod((list2array[int] (0)(array2list[int](1 + n)(a))),n,g,k)(x1)") (("2" (expand "der_prod" -1) (("2" (assert) (("2" (case "NOT N(0)=n") (("1" (expand "N" 1) (("1" (expand "max") (("1" (replace -3) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "FORALL (jj:int): rational_pred(jj)") (("1" (inst - "der_prod((list2array[int] (0)(array2list[int](1 + n)(a))),n,g,k)(x1)") (("1" (expand "der_prod" -1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "N" 1) (("3" (expand "max" 1) (("3" (replace -3) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (label "frizzy3" -1) (("2" (hide "frizzy3") (("2" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (assert) (("1" (expand "N" 1) (("1" (assert) (("1" (expand "max" 1) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (label "frizzy4" -1) (("2" (hide "frizzy4") (("2" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (expand "N" 1) (("1" (expand "M" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (label "frizzy5" -1) (("2" (hide "frizzy5") (("2" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (expand "P" 1) (("1" (expand "M" 1) (("1" (assert) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (assert) (("1" (case "nth(sl,0) = null") (("1" (replaces -1) (("1" (hide -) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but (-7 1)) (("2" (grind :exclude "nth") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "frizzy6" -1) (("2" (replace "frizzy6") (("2" (hide "frizzy6") (("2" (invoke (case "NOT %1") (! 2 1)) (("1" (hide 3) (("1" (skeep) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (inst -5 "length(sl)-1-j") (("1" (assert) (("1" (case "NOT P(j-2) = list2array[int](0)(nth(sl, 1 + length(sl) - j))") (("1" (hide 2) (("1" (decompose-equality 1) (("1" (name "ii" "x!1") (("1" (replaces -1) (("1" (expand "P" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT N(j-2) = length(nth(sl, 1 + length(sl) - j)) - 1") (("1" (expand "N" 1) (("1" (assert) (("1" (expand "max") (("1" (lift-if) (("1" (ground) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (inst - "0" "1+length(sl)-j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT P(j-1) = list2array[int](0)(nth(sl, length(sl) - j))") (("1" (expand "P" 1) (("1" (propax) nil nil)) nil) ("2" (case "NOT N(j-1) = length(nth(sl, length(sl) - j)) - 1") (("1" (expand "N" 1) (("1" (expand "max" 1) (("1" (lift-if) (("1" (ground) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (inst - "0" "length(sl)-j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 :dir rl) (("2" (replace -2 :dir rl) (("2" (replace -3 :dir rl) (("2" (replace -4 :dir rl) (("2" (assert) (("2" (case "NOT P(j) = list2array[int](0)(nth(sl, length(sl) - j-1))") (("1" (expand "P" 1) (("1" (propax) nil nil)) nil) ("2" (case "NOT N(j) = length(nth(sl, length(sl) - j - 1)) - 1") (("1" (expand "N" 1) (("1" (expand "max" 1) (("1" (lift-if) (("1" (assert) (("1" (ground) (("1" (case "NOT j = M") (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (inst - "0" "M-j") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "M" -1) (("2" (assert) (("2" (replace -1 -3) (("2" (assert) (("2" (case "NOT length(adjusted_remainder(P(j - 2), N(j - 2))(P(j - 1), N(j - 1))) = 0") (("1" (assert) nil nil) ("2" (lemma "adjusted_remainder_empty") (("2" (inst?) (("1" (assert) (("1" (split -) (("1" (assert) (("1" (inst + "1") (("1" (assert) (("1" (decompose-equality 1) (("1" (invoke (case "NOT %1 = 0") (! 1 1)) (("1" (hide 2) (("1" (case "NOT N(j)=0") (("1" (assert) (("1" (expand "N" 1) (("1" (expand "max" 1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "P(j)(0)=0") (("1" (assert) (("1" (replace -2) (("1" (rewrite "polynomial_n0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "list2array_sound[int]") (("2" (inst - "nth(sl,0)" "0" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (hide (-11 -12)) (("2" (hide (-21 -22)) (("2" (expand "polynomial" 1) (("2" (rewrite "sigma_restrict_eq_0") (("2" (hide 2) (("2" (skosimp*) (("2" (inst - "i!1") (("2" (assert) (("2" (expand "*") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "N") (("3" (expand "max") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "N") (("2" (ground) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "N") (("3" (ground) nil nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand "N") (("4" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -) (("2" (hide 2) (("2" (skeep) (("2" (expand "P") (("2" (expand "N") (("2" (assert) (("2" (lemma "list2array_sound[int]") (("2" (inst?) (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (inst-cp - "length(sl) - j + 1 -1" "length(sl)-j+1") (("1" (inst-cp - "length(sl)-j+1-2" "length(sl) - j + 1 -1") (("1" (assert) (("1" (case "NOT FORALL (ab1,ab2,ab3:nat): ab1 < ab2 AND ab2 < ab3 IMPLIES (NOT ab3-1<0)") (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil) ("2" (inst - "length(nth(sl, length(sl) - 1 - j))" "length(nth(sl, length(sl) - j))" "length(nth(sl, 1 + length(sl) - j))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (ab3:nat): NOT (i>ab3-1 AND i<ab3)") (("1" (inst?) (("1" (assert) 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)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide -) (("3" (skeep) (("3" (expand "P") (("3" (expand "N") (("3" (assert) (("3" (lemma "list2array_sound[int]") (("3" (inst?) (("3" (assert) (("3" (lift-if) (("3" (ground) (("3" (expand "max") (("3" (lift-if) (("3" (ground) (("1" (replace -4 +) (("1" (case "i < 0") (("1" (assert) nil nil) ("2" (case "FORALL (pjk:nat): pjk-1<0 IMPLIES pjk = 0") (("1" (inst - "length(nth(sl,length(sl)-j))") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (aa:int): NOT (i>aa-1 AND i<aa)") (("1" (inst?) (("1" (assert) 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)) nil)) nil) ("4" (assert) (("4" (reveal "frizzy1") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "frizzy2") (("2" (inst - "j-2" "j-1") (("1" (assert) (("1" (hide 2) (("1" (expand "N" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (replace -3 1) (("2" (assert) (("2" (replace -3) (("2" (assert) (("2" (assert) (("2" (case "NOT length(sl)=3") (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (reveal 1) (("2" (hide 2) (("2" (expand "N" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "N" 1) (("3" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "N" 1) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (expand "N" 1) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "mini" -) (("2" (label "mini" -) (("2" (lemma "adjusted_remainder_def") (("2" (inst?) (("1" (hide "mini") (("1" (split -) (("1" (skoletin -) (("1" (skoletin -) (("1" (skoletin -) (("1" (skoletin -) (("1" (case "thispoly = P(j) AND thisdeg = N(j)") (("1" (flatten) (("1" (case "NOT N(j)>=0") (("1" (expand "N" 1) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (flatten) (("2" (replace -7 :dir rl) (("2" (replace -2) (("2" (replace -3) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (- 2)) (("2" (reveal "mini") (("2" (split +) (("1" (replace -2 1) (("1" (expand "thispoly" +) (("1" (expand "thisrem" +) (("1" (replace -11 :dir rl) (("1" (expand "thisdeg" 1) (("1" (expand "thisrem" 1) (("1" (replace -11 :dir rl) (("1" (hide -) (("1" (decompose-equality) (("1" (lemma "list2array_sound[int]") (("1" (inst?) (("1" (replaces -1) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "thisdeg" 1) (("2" (expand "thisrem" 1) (("2" (replace -11 :dir rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "frizzy1") (("2" (inst?) nil nil)) nil)) nil) ("3" (hide 2) (("3" (skeep) (("3" (expand "P") (("3" (expand "N") (("3" (expand "max") (("3" (lift-if) (("3" (ground) (("1" (expand "list2array") (("1" (lift-if) (("1" (ground) (("1" (expand "length" -1 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "list2array_sound[int]") (("2" (inst?) (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (case "FORALL (ab3:nat): NOT (ii>ab3-1 AND ii<ab3)") (("1" (inst?) (("1" (assert) 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) ("4" (hide 2) (("4" (hide 2) (("4" (skeep) (("4" (expand "P") (("4" (expand "N") (("4" (assert) (("4" (lemma "list2array_sound[int]") (("4" (inst?) (("4" (assert) (("4" (lift-if) (("4" (ground) (("4" (expand "max") (("4" (lift-if) (("4" (ground) (("1" (replace -4 +) (("1" (case "ii < 0") (("1" (assert) nil nil) ("2" (case "FORALL (pjk:nat): pjk-1<0 IMPLIES pjk = 0") (("1" (inst - "length(nth(sl,length(sl)-j))") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (aa:int): NOT (ii>aa-1 AND ii<aa)") (("1" (inst?) (("1" (assert) 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)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "N") (("2" (assert) nil nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "N") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (label "frizzydizzy" -1) (("2" (hide "frizzydizzy") (("2" (case "NOT (M=-1 OR M=0 OR M=1)") (("1" (assert) nil nil) ("2" (split -) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) (("3" (reveal "frizzy1") (("3" (reveal "frizzy2") (("3" (reveal "frizzy3") (("3" (reveal "frizzy4") (("3" (reveal "frizzy5") (("3" (replace -7 -1) (("3" (reveal "frizzy6") (("3" (replace -8 -1) (("3" (assert) (("3" (inst - "0") (("3" (assert) (("3" (replace -4 -1) (("3" (expand "polynomial_prod" -1) (("3" (case "NOT N(0) = n") (("1" (expand "N" 1) (("1" (hide -1) (("1" (expand "max" 1) (("1" (assert) (("1" (lift-if) (("1" (typepred "sl") (("1" (hide -1) (("1" (expand "is_neg_remainder_list?") (("1" (flatten) (("1" (replace -3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (expand "sigma") (("2" (expand "sigma") (("2" (expand "poly_deriv") (("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) ("3" (skeep) (("3" (expand "N" 1) (("3" (lift-if) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (assert) (("4" (skeep) (("4" (assert) nil nil)) nil)) nil) ("5" (skeep) (("5" (assert) (("5" (split 1) (("1" (expand "N" 1) (("1" (assert) nil nil)) nil) ("2" (reveal "frizzy1") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("6" (skeep) (("6" (assert) nil nil)) nil) ("7" (skeep) (("7" (expand "N" 1) (("7" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "N" 1) (("3" (assert) (("3" (expand "max" 1) (("3" (assert) (("3" (typepred "sl") (("3" (assert) (("3" (expand "is_neg_remainder_list?") (("3" (hide -1) (("3" (flatten) (("3" (replace -3) (("3" (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) ("3" (hide 3) (("3" (assert) (("3" (skeep) (("3" (expand "N" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "sl") (("2" (hide -1) (("2" (expand "is_neg_remainder_list?") (("2" (flatten) (("2" (assert) (("2" (expand "M" 1) (("2" (replace -3) (("2" (decompose-equality +) (("2" (name "ii" "x!1") (("2" (replace -1) (("2" (lemma "list2array_sound[int]") (("2" (inst?) (("2" (replaces -1) (("2" (assert) (("2" (lift-if) (("2" (ground) (("1" (typepred "array2list[int](1+n)(a)") (("1" (inst - "ii") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "ii") (("2" (inst - "ii") (("2" (inst - "ii") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "sl") (("3" (hide -1) (("3" (expand "is_neg_remainder_list?") (("3" (flatten) (("3" (expand "max") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (der_prod const-decl "int" compute_sturm_tarski nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (> const-decl "bool" reals nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence "Sturm/") (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (/= const-decl "boolean" notequal 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) (list type-decl nil list_adt nil) (number nonempty-type-decl nil numbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (list2array def-decl "T" array2list "structures/") (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (constructed_sturm_sequence? const-decl "bool" sturmtarski nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (poly_deriv const-decl "real" polynomials "reals/") (polynomial_prod const-decl "real" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (max_nnreal_0 formula-decl nil min_max "reals/") (real_times_real_is_real application-judgement "real" reals nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (x!1 skolem-const-decl "nat" compute_sturm_tarski nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_eq formula-decl nil sigma "reals/") (n!1 skolem-const-decl "subrange(max(1 - n + x!1, 0), k)" compute_sturm_tarski nil) (a skolem-const-decl "[nat -> int]" compute_sturm_tarski nil) (n skolem-const-decl "posnat" compute_sturm_tarski nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (listn type-eq-decl nil listn "structures/") (k skolem-const-decl "nat" compute_sturm_tarski nil) (g skolem-const-decl "[nat -> int]" compute_sturm_tarski nil) (max_npreal_0 formula-decl nil min_max "reals/") (M skolem-const-decl "int" compute_sturm_tarski nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (null adt-constructor-decl "(null?)" list_adt nil) (poly_divide def-decl "DivType" polynomial_division "Sturm/") (DivType type-eq-decl nil polynomial_division "Sturm/") (- const-decl "[numfield -> numfield]" number_fields nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (adjusted_remainder_def formula-decl nil polynomial_pseudo_divide "Sturm/") (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (thisrem skolem-const-decl "list[int]" compute_sturm_tarski nil) (thisdeg skolem-const-decl "int" compute_sturm_tarski nil) (thispoly skolem-const-decl "[nat -> int]" compute_sturm_tarski nil) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide "Sturm/") (^ const-decl "real" exponentiation nil) (polynomial_n0 formula-decl nil polynomials "reals/") (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (adjusted_remainder_empty formula-decl nil polynomial_pseudo_divide "Sturm/") (j skolem-const-decl "nat" compute_sturm_tarski nil) (sl skolem-const-decl "{crem: (is_neg_remainder_list?(a, n, der_prod(a, n, g, k), n - 1 + k)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" compute_sturm_tarski nil) (sigma def-decl "real" sigma "reals/") (P skolem-const-decl "[nat -> [nat -> int]]" compute_sturm_tarski nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (list2array_sound formula-decl nil array2list "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (N skolem-const-decl "[nat -> int]" compute_sturm_tarski nil) (NOT const-decl "[bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (Eq_computed_remainder?_TCC1 0 (Eq_computed_remainder?_TCC1-1 nil 3595179342 ("" (subtype-tcc) nil nil) nil nil)) (Eq_computed_remainder?_TCC2 0 (Eq_computed_remainder?_TCC2-1 nil 3595179342 ("" (skeep) (("" (assert) (("" (expand "der_prod") (("" (expand "polynomial_prod") (("" (expand "max") (("" (expand "sigma") (("" (expand "sigma") (("" (expand "poly_deriv") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (polynomial_prod const-decl "real" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (poly_deriv const-decl "real" polynomials "reals/") (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (der_prod const-decl "int" compute_sturm_tarski nil)) nil)) (compute_TQ_param_TCC1 0 (compute_TQ_param_TCC1-1 nil 3619438219 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Eq_computed_remainder? const-decl "bool" compute_sturm_tarski nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (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) (int_plus_int_is_int application-judgement "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)) nil)) (compute_TQ_param_TCC2 0 (compute_TQ_param_TCC2-1 nil 3619438219 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Eq_computed_remainder? const-decl "bool" compute_sturm_tarski 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) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (compute_TQ_param_TCC3 0 (compute_TQ_param_TCC3-1 nil 3619438219 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Eq_computed_remainder? const-decl "bool" compute_sturm_tarski nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (compute_TQ_param_TCC4 0 (compute_TQ_param_TCC4-1 nil 3619438219 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Eq_computed_remainder? const-decl "bool" compute_sturm_tarski nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs 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) (int_plus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (compute_TQ_param_TCC5 0 (compute_TQ_param_TCC5-1 nil 3619438219 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Eq_computed_remainder? const-decl "bool" compute_sturm_tarski nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs 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) (int_plus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (TQ_TCC1 0 (TQ_TCC1-1 nil 3619438219 ("" (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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_gt_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) (/= const-decl "boolean" notequal nil)) nil)) (TQ_TCC2 0 (TQ_TCC2-1 nil 3619438219 ("" (skeep) (("" (assert) (("" (expand "der_prod") (("" (expand "polynomial_prod") (("" (replaces -1) (("" (expand "max") (("" (expand "sigma") (("" (expand "sigma") (("" (expand "poly_deriv") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (polynomial_prod const-decl "real" polynomials "reals/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (poly_deriv const-decl "real" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (der_prod const-decl "int" compute_sturm_tarski nil)) nil)) (TQ_TCC3 0 (TQ_TCC3-1 nil 3619438219 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (/= const-decl "boolean" notequal nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (nonzero_version const-decl "list[int]" gcd_coeff "Sturm/") (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide "Sturm/") (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_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (der_prod const-decl "int" compute_sturm_tarski nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence "Sturm/") (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (list type-decl nil list_adt nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (Eq_computed_remainder? const-decl "bool" compute_sturm_tarski nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (TQ_def 0 (TQ_def-1 nil 3619451118 ("" (skeep) (("" (expand "TQ") (("" (name "sl" "remainder_seq(LAMBDA (i: nat): IF i <= n THEN a(i) ELSE 0 ENDIF, n, der_prod (LAMBDA (i: nat): IF i <= n THEN a(i) ELSE 0 ENDIF, n, g, k), k - 1 + n)") (("" (replace -1) (("" (expand "compute_TQ_param" :assert? none) (("" (skoletin 3) (("" (skoletin 1) (("" (skoletin 1) (("" (skoletin 1) (("" (skoletin 1) (("" (replace -2 -1) (("" (assert) (("" (hide -2) (("" (lemma "sturm_tarski_unbounded") (("" (inst - "g" "k" "M" "N" "P") (("1" (split -1) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (case "FORALL (relo:[[real,real]->bool]): NSol(P(0),N(0),g,k,relo) = NSol(a,n,g,k,relo)") (("1" (inst-cp - ">") (("1" (inst - "<") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (expand "NSol" 1) (("2" (case "Sol(P(0), N(0), g, k, relo) = Sol(a, n, g, k, relo)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (decompose-equality 1) (("1" (expand "Sol" 1) (("1" (case "polynomial(P(0), N(0))(x!1) =polynomial(a, n)(x!1)") (("1" (assert) (("1" (replaces -1) nil nil)) nil) ("2" (hide 2) (("2" (expand "P" 1) (("2" (expand "N" 1) (("2" (lemma "computed_sturm_spec") (("2" (inst?) (("2" (assert) (("2" (replace -7) (("2" (split -) (("1" (flatten) (("1" (replace -2) (("1" (assert) (("1" (replace -3) (("1" (hide -) (("1" (lemma "polynomial_eq_coeff") (("1" (inst - "LAMBDA (i: nat): IF i <= n THEN a(i) ELSE 0 ENDIF" "a" "n") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "N" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "N" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "computed_sturm_spec") (("2" (inst?) (("2" (assert) (("2" (replace -6) (("2" (assert) (("2" (skosimp*) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "N" 1) (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (TQ const-decl "int" compute_sturm_tarski nil) (NOT const-decl "[bool -> bool]" booleans nil) (list2array def-decl "T" array2list "structures/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (NSC type-eq-decl nil number_sign_changes "Sturm/") (FALSE const-decl "bool" booleans nil) (number_sign_changes def-decl "NSC" number_sign_changes "Sturm/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (even? const-decl "bool" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (Sol const-decl "finite_set[real]" sturmtarski nil) (NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski 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) (sturm_tarski_unbounded formula-decl nil sturmtarski nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (P skolem-const-decl "[nat -> [nat -> int]]" compute_sturm_tarski nil) (computed_sturm_spec formula-decl nil compute_sturm_tarski nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff "Sturm/") (listn_0 name-judgement "listn[real](0)" polynomial_division "Sturm/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (polynomial_eq_coeff formula-decl nil polynomials "reals/") (N skolem-const-decl "[nat -> int]" compute_sturm_tarski nil) (compute_TQ_param const-decl "int" compute_sturm_tarski nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (number nonempty-type-decl nil numbers nil) (list type-decl nil list_adt nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities 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) (/= const-decl "boolean" notequal nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (is_neg_remainder_list? const-decl "bool" remainder_sequence "Sturm/") (> const-decl "bool" reals nil) (length def-decl "nat" list_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence "Sturm/") (IF const-decl "[boolean, T, T -> T]" if_def nil) (<= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (der_prod const-decl "int" compute_sturm_tarski nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (TQ_eq_g 0 (TQ_eq_g-1 nil 3620147464 ("" (skeep) (("" (case "polynomial(g1,k)=polynomial(g2,k)") (("1" (rewrite "TQ_def") (("1" (rewrite "TQ_def") (("1" (expand "NSol") (("1" (expand "Sol") (("1" (assert) (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "polynomial_eq_coeff") (("2" (inst?) (("2" (assert) 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) (Sol const-decl "finite_set[real]" sturmtarski nil) (NSol const-decl "{d: nat | EXISTS (enumsol: [below(d) -> (Sol(a, m, g, k, rel))]): bijective?(enumsol)}" sturmtarski nil) (int_minus_int_is_int application-judgement "int" 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) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (TQ_def formula-decl nil compute_sturm_tarski nil) (polynomial_eq_coeff formula-decl nil polynomials "reals/")) shostak)))
¤ Dauer der Verarbeitung: 0.723 Sekunden (vorverarbeitet am 2026-05-05) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26