| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/Sturm/ (Beweissystem der NASA Version 6.0.9©) Datei vom 8.10.2014 mit Größe 1 MB |
|
Quelle compute_sturm.prfSprache: Lisp |
|||||||||||||||
|
(compute_sturm (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) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (x skolem-const-decl "real" compute_sturm nil) (A skolem-const-decl "set[real]" compute_sturm 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 nil) (injective? const-decl "bool" functions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (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 nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (ii skolem-const-decl "below(m)" compute_sturm nil) (/= const-decl "boolean" notequal nil) (bij skolem-const-decl "[below(m) -> (A)]" compute_sturm 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 nil) (i skolem-const-decl "below(m)" compute_sturm nil) (A skolem-const-decl "set[real]" compute_sturm nil) (bij skolem-const-decl "[below(m) -> (A)]" compute_sturm nil) (x skolem-const-decl "real" compute_sturm nil) (y skolem-const-decl "real" compute_sturm nil) (j skolem-const-decl "below(m)" compute_sturm 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 nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (surjective? const-decl "bool" functions nil) (y skolem-const-decl "real" compute_sturm nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (injective? const-decl "bool" functions nil) (x skolem-const-decl "real" compute_sturm nil) (A skolem-const-decl "set[real]" compute_sturm 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 ("" (subtype-tcc) nil nil) ((mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (int_plus_int_is_int application-judgement "int" integers nil) (poly_deriv const-decl "real" polynomials "reals/") (/= const-decl "boolean" notequal 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) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (/= const-decl "boolean" notequal nil) (poly_deriv const-decl "real" polynomials "reals/")) 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) (>= 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) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (/= 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 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) ((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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division 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) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (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) (/= 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 nil) (int_minus_int_is_int application-judgement "int" 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) (>= 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) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (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) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (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) (/= 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 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, poly_deriv(a), n - 1)") (("" (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) (("3" (both-sides "-" "length(sl)-1" 1) (("3" (simplify 1) (("3" (case "i=0") (("1" (typepred "array2list[int](1 + n)(a)") (("1" (replace -4 +) (("1" (simplify) (("1" (replace -6 +) (("1" (replace -2 +) (("1" (simplify +) (("1" (hide (-1 -2 -3)) (("1" (case "j=1") (("1" (replace -1 +) (("1" (simplify) (("1" (replace -5 +) (("1" (typepred "array2list[int](n)(poly_deriv(a))") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (inst -2 "length(sl) -1 -j") (("2" (assert) (("2" (ground) (("2" (reveal -6) (("2" (inst -1 "length(sl) - 1 - j" "length(sl) -2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) 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" (expand "P" 1) (("1" (assert) (("1" (replace -3) (("1" (replace -4) (("1" (decompose-equality 1) (("1" (lemma "list2array_sound[int]") (("1" (inst?) (("1" (replace -1) (("1" (assert) (("1" (lift-if) (("1" (split +) (("1" (flatten) (("1" (typepred "array2list[int](n)(poly_deriv(a))") (("1" (replace -2) (("1" (assert) (("1" (typepred "array2list[int](n)(poly_deriv(a))") (("1" (inst - "x!1") (("1" (replace -3 :dir rl) (("1" (assert) (("1" (expand "poly_deriv" 1) (("1" (hide (-1 -2 -3 -4 -5)) (("1" (lemma "list2array_sound[int]") (("1" (inst?) (("1" (assert) (("1" (replace -1 +) (("1" (typepred "array2list[int](1+n)(a)") (("1" (inst - "1+x!1") (("1" (replaces -2) (("1" (replace -3 :dir rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (typepred "array2list[int](n)(poly_deriv(a))") (("2" (hide -1) (("2" (replace -1) (("2" (expand "poly_deriv" 2) (("2" (lemma "list2array_sound[int]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "poly_deriv" 1) (("2" (propax) 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" (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) ("2" (assert) (("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") (("2" (assert) (("2" (hide 2) (("2" (expand "N" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "N" 1) (("3" (assert) nil 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" (reveal "frizzy2") (("3" (inst - "j-2" "j-1") (("3" (assert) (("3" (hide 2) (("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) (("3" (typepred "sl") (("3" (hide -1) (("3" (expand "is_neg_remainder_list?") (("3" (flatten) (("3" (inst-cp - "length(sl) - j + 1 -1" "length(sl)-j+1") (("3" (inst-cp - "length(sl)-j+1-2" "length(sl) - j + 1 -1") (("3" (assert) (("3" (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) (("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)) 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 -6 -1) (("3" (reveal "frizzy6") (("3" (replace -7 -1) (("3" (assert) (("3" (replace -4 -1) (("3" (inst - "0") (("3" (assert) (("3" (expand "poly_deriv" -1) (("3" (assert) 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" (reveal "frizzy2") (("7" (inst - "j-2" "j-1") (("1" (assert) (("1" (assert) (("1" (expand "N" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("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)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (expand "N" 1) (("3" (assert) 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) (numfield nonempty-type-eq-decl nil number_fields nil) (poly_deriv const-decl "real" polynomials "reals/") (sequence type-eq-decl nil sequences 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 nil) (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 nil) (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_minus_int_is_int application-judgement "int" integers nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (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" sturm nil) (both_sides_minus_le2 formula-decl nil real_props nil) (both_sides_minus_lt2 formula-decl nil real_props nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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/") (n skolem-const-decl "posnat" compute_sturm nil) (a skolem-const-decl "[nat -> int]" compute_sturm nil) (int_plus_int_is_int application-judgement "int" integers nil) (max_nnreal_0 formula-decl nil min_max "reals/") (j skolem-const-decl "nat" compute_sturm nil) (sl skolem-const-decl "{crem: (is_neg_remainder_list?(a, n, poly_deriv(a), n - 1)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" compute_sturm nil) (j skolem-const-decl "nat" compute_sturm nil) (adjusted_remainder_empty formula-decl nil polynomial_pseudo_divide nil) (polynomial_n0 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (real_times_real_is_real application-judgement "real" reals nil) (subrange type-eq-decl nil integers nil) (adjusted_remainder const-decl "list[int]" polynomial_pseudo_divide nil) (thispoly skolem-const-decl "[nat -> int]" compute_sturm nil) (thisdeg skolem-const-decl "int" compute_sturm nil) (thisrem skolem-const-decl "list[int]" compute_sturm nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (adjusted_remainder_def formula-decl nil polynomial_pseudo_divide nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (<= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (DivType type-eq-decl nil polynomial_division nil) (poly_divide def-decl "DivType" polynomial_division nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (M skolem-const-decl "int" compute_sturm nil) (max_npreal_0 formula-decl nil min_max "reals/") (P skolem-const-decl "[nat -> [nat -> int]]" compute_sturm nil) (list2array_sound formula-decl nil array2list "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (N skolem-const-decl "[nat -> int]" compute_sturm nil) (NOT const-decl "[bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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 ("" (subtype-tcc) nil nil) ((poly_deriv const-decl "real" polynomials "reals/") (int_plus_int_is_int application-judgement "int" integers nil)) nil)) (Eq_computed_remainder?_TCC3 0 (Eq_computed_remainder?_TCC3-1 nil 3595179342 ("" (subtype-tcc) nil nil) ((poly_deriv const-decl "real" polynomials "reals/")) nil)) (roots_closed_int_TCC1 0 (roots_closed_int_TCC1-1 nil 3594568781 ("" (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) (< const-decl "bool" reals 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 nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_lt_is_strict_total_order name-judgement "(strict_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 nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (roots_closed_int_TCC2 0 (roots_closed_int_TCC2-1 nil 3594568781 ("" (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) (< const-decl "bool" reals 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 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 nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division 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) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (roots_closed_int_TCC3 0 (roots_closed_int_TCC3-1 nil 3594568781 ("" (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) (< const-decl "bool" reals 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 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 nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (roots_closed_int_TCC4 0 (roots_closed_int_TCC4-1 nil 3594568781 ("" (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) (< const-decl "bool" reals 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 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 nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (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)) (roots_closed_int_TCC5 0 (roots_closed_int_TCC5-1 nil 3594568781 ("" (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) (< const-decl "bool" reals 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 nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division 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) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (remainder_seq const-decl "{crem: (is_neg_remainder_list?(g, n, h, m)) | length(crem) > 1 AND length(nth(crem, 0)) = 0}" remainder_sequence nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (rat_exp application-judgement "rat" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (^ 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) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (roots_closed_int_TCC6 0 (roots_closed_int_TCC6-1 nil 3594568781 ("" (subtype-tcc) nil nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals 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 nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (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) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Eq_computed_remainder? const-decl "bool" compute_sturm nil) (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 "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (> 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) (/= const-decl "boolean" notequal nil) (poly_rootless_width const-decl "posreal" more_polynomial_props "reals/") (poly_n_deriv const-decl "real" polynomials "reals/") (C const-decl "posnat" binomial "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (^ const-decl "real" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (roots_closed_int_def_truetrue 0 (roots_closed_int_def_truetrue-1 nil 3595067092 ("" (skeep) (("" (typepred "sl") (("" (hide -1) (("" (label "slname" -1) (("" (expand "Eq_computed_remainder?") (("" (label "xlty" -2) (("" (skoletin 2) (("" (label "rootnamename" -1) (("" (skoletin 1) (("" (label "Asetname" -1) (("" (label "final" 1) (("" (hide "final") (("" (expand "roots_closed_int" :assert? none) (("" (skoletin -2) (("" (label "newaname" -2) (("" (replace "newaname" :dir rl) (("" (skoletin -1) (("" (label "Pname" -2) (("" (skoletin -1) (("" (label "Nname" -2) (("" (skoletin -1) (("" (label "Mname" -2) (("" (skoletin -1) (("" (label "nscnormname" -2) (("" (skoletin -1) (("" (label "nschighlowname" -2) (("" (skoletin -1) (("" (label "newlowname" -2) (("" (skoletin -1) (("" (label "newhighname" -2) (("" (skoletin -1) (("" (label "Nrootsname" -2) (("" (skoletin -1) (("" (label "adjlowname" -2) (("" (case "NOT polynomial(a,n) = polynomial(newa,n)") (("1" (hide -) (("1" (decompose-equality) (("1" (lemma "poly_eq_le_degree") (("1" (inst?) (("1" (assert) (("1" (skeep) (("1" (expand "newa" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "computed_sturm_spec") (("2" (inst - "newa" "n") (("2" (assert) (("2" (replace "slname" :dir rl) (("2" (replace "Pname" :dir rl) (("2" (replace "Nname" :dir rl) (("2" (assert) (("2" (label "polyeq" -2) (("2" (split -) (("1" (flatten) (("1" (label "css" -1) (("1" (case "NOT (P(0) = newa AND N(0) = n)") (("1" (expand "P" 1) (("1" (expand "N" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (case "NOT (P(1) = poly_deriv(newa) AND N(1) = n-1)") (("1" (expand "constructed_sturm_sequence?" "css") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (lemma "sturm") (("2" (inst - "M" "N" "P" "newlow" "newhigh") (("1" (split -) (("1" (replace "nscnormname" :dir rl) (("1" (assert) (("1" (replace "Nrootsname" :dir rl) (("1" (flatten) (("1" (reveal "final") (("1" (case "NOT rootnum>=0") (("1" (hide 2) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lift-if "adjlowname") (("2" (split "adjlowname") (("1" (flatten) (("1" (replaces -2) (("1" (assert) (("1" (skeep -4) (("1" (inst + "LAMBDA (i:below(rootnum)): IF i=Nroots THEN x ELSE bij(i) ENDIF") (("1" (assert) (("1" (expand "bijective?") (("1" (flatten) (("1" (split +) (("1" (expand "injective?") (("1" (skeep) (("1" (lift-if -1) (("1" (lift-if -1) (("1" (lift-if -1) (("1" (assert) (("1" (ground) (("1" (inst - "x1" "x2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (case "y!1 = x") (("1" (inst + "Nroots") (("1" (assert) nil nil)) nil) ("2" (inst - "y!1") (("1" (skosimp*) (("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide "final") (("2" (case "NOT polynomial(P(0),N(0))(y!1)=0") (("1" (hide 2) (("1" (assert) (("1" (expand "Aset" -1) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "y!1") (("2" (lift-if) (("2" (expand "Aset" -1) (("2" (flatten) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (assert) (("2" (typepred "i") (("2" (typepred "bij(i)") (("2" (assert) (("2" (lemma "poly_rootless_width_def") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (inst - "bij(i)" "0") (("1" (assert) (("1" (assert) (("1" (expand "Aset" 2) (("1" (assert) (("1" (lemma "poly_n_deriv_def") (("1" (inst - "a") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "abs" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skeep) (("4" (expand "Aset" 1) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (skeep -4) (("2" (inst + "bij") (("1" (assert) (("1" (expand "bijective?") (("1" (flatten) (("1" (split 2) (("1" (expand "injective?") (("1" (skeep) (("1" (inst - "x1" "x2") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skeep) (("2" (inst - "y!1") (("1" (skeep) (("1" (inst + "x!1") nil nil)) nil) ("2" (assert) (("2" (typepred "y!1") (("2" (lift-if) (("2" (expand "Aset" -1) (("2" (flatten) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split +) (("1" (skosimp*) (("1" (ground) nil nil)) nil) ("2" (skeep) (("2" (expand "Aset" 1) (("2" (assert) (("2" (typepred "bij(x1)") (("2" (assert) (("2" (split +) (("1" (expand "newlow" -1) (("1" (lift-if -1) (("1" (assert) (("1" (split -1) (("1" (propax) nil nil) ("2" (flatten) (("2" (lemma "poly_rootless_width_def") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (inst - "bij(x1)" "0") (("1" (assert) (("1" (assert) (("1" (split 1) (("1" (lemma "poly_n_deriv_def") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "newhigh" -2) (("2" (lift-if -2) (("2" (split -2) (("1" (flatten) nil nil) ("2" (assert) (("2" (flatten) (("2" (assert) (("2" (lemma "poly_rootless_width_def") (("2" (inst?) (("2" (assert) (("2" (split -) (("1" (inst - "bij(x1)" "0") (("1" (assert) (("1" (assert) (("1" (split +) (("1" (lemma "poly_n_deriv_def") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n") (("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) ("2" (expand "newlow" 1) (("2" (expand "newhigh" 1) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil) ("4" (flatten) (("4" (assert) (("4" (expand "newlow" (-1 -2)) (("4" (lift-if (-1 -2)) (("4" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (lemma "poly_rootless_width_def") (("2" (inst?) (("2" (split -) (("1" (assert) (("1" (inst - "x - poly_rootless_width(a, n, x, TRUE) / 2" "0") (("1" (assert) (("1" (assert) (("1" (lemma "poly_n_deriv_def") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (expand "abs" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (flatten) (("5" (assert) (("5" (expand "newhigh" (-1 -2)) (("5" (lift-if (-1 -2)) (("5" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (flatten) (("2" (assert) (("2" (lemma "poly_rootless_width_def") (("2" (inst?) (("2" (split -) (("1" (assert) (("1" (inst - "y+ poly_rootless_width(a, n, y, TRUE) / 2" "0") (("1" (assert) (("1" (assert) (("1" (lemma "poly_n_deriv_def") (("1" (inst?) (("1" (flatten) (("1" (assert) (("1" (expand "abs" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "newhigh" 1) (("2" (propax) nil nil)) nil)) nil) ("3" (expand "newlow" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "newa" 1) (("2" (propax) nil nil)) nil) ("3" (hide -) (("3" (expand "newa") (("3" (grind) 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)) nil)) nil)) nil)) nil)) nil)) nil) ((Eq_computed_remainder? const-decl "bool" compute_sturm nil) (/= const-decl "boolean" notequal nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (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) (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) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (minus_odd_is_odd application-judgement "odd_int" integers 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) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (id const-decl "(bijective?[T, T])" identity nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (length def-decl "nat" list_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (list2array def-decl "T" array2list "structures/") (below type-eq-decl nil nat_types nil) (nth def-decl "T" list_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (NSC type-eq-decl nil number_sign_changes nil) (number_sign_changes def-decl "NSC" number_sign_changes nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (- const-decl "[numfield -> numfield]" number_fields nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (poly_rootless_width const-decl "posreal" more_polynomial_props "reals/") (naturalnumber type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (lt_realorder name-judgement "RealOrder" real_orders "reals/") (computed_sturm_spec formula-decl nil compute_sturm nil) (newlow skolem-const-decl "numfield" compute_sturm nil) (newhigh skolem-const-decl "numfield" compute_sturm nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (poly_n_deriv_def formula-decl nil polynomials "reals/") (minus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (poly_rootless_width_def formula-decl nil more_polynomial_props "reals/") (surjective? const-decl "bool" functions nil) (y!1 skolem-const-decl "(Aset)" compute_sturm nil) (injective? const-decl "bool" functions nil) (bij skolem-const-decl "[below(nscnorm(newlow)`num - nscnorm(newhigh)`num) -> {xr: real | newlow < xr AND xr <= newhigh AND polynomial(P(0), N(0))(xr) = 0}]" compute_sturm nil) (nscnorm skolem-const-decl "[real -> NSC]" compute_sturm nil) (x skolem-const-decl "real" compute_sturm nil) (Aset skolem-const-decl "[real -> boolean]" compute_sturm nil) (Nroots skolem-const-decl "int" compute_sturm nil) (rootnum skolem-const-decl "int" compute_sturm nil) (y!1 skolem-const-decl "(Aset)" compute_sturm nil) (bij skolem-const-decl "[below(nscnorm(newlow)`num - nscnorm(newhigh)`num) -> {xr: real | newlow < xr AND xr <= newhigh AND polynomial(P(0), N(0))(xr) = 0}]" compute_sturm nil) (sturm formula-decl nil sturm nil) (constructed_sturm_sequence? const-decl "bool" sturm nil) (poly_deriv const-decl "real" polynomials "reals/") (P skolem-const-decl "[nat -> [nat -> int]]" compute_sturm nil) (listn_0 name-judgement "listn[int](0)" gcd_coeff nil) (listn_0 name-judgement "listn[real](0)" polynomial_division nil) (N skolem-const-decl "[nat -> int]" compute_sturm nil) (gt_realorder name-judgement "RealOrder" real_orders "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (poly_eq_le_degree formula-decl nil polynomials "reals/") (newa skolem-const-decl "[nat -> int]" compute_sturm nil) (le_realorder name-judgement "RealOrder" real_orders "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (rat_exp application-judgement "rat" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (ge_realorder name-judgement "RealOrder" real_orders "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (bijective? const-decl "bool" functions nil) (below type-eq-decl nil naturalnumbers nil) (TRUE const-decl "bool" booleans nil) (roots_closed_int const-decl "int" compute_sturm nil) (= const-decl "[T, T -> boolean]" equalities nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (< const-decl "bool" reals nil)) nil)) (roots_closed_int_def_falsetrue 0 (roots_closed_int_def_falsetrue-1 nil 3595068138 ("" (skeep) (("" (typepred "sl") (("" (hide -1) (("" (label "slname" -1) (("" (expand "Eq_computed_remainder?") (("" (label "xlty" -2) (("" (skoletin 2) (("" (label "rootnamename" -1) (("" (skoletin 1) (("" (label "Asetname" -1) (("" (label "slname" -4) (("" (label "final" 1) (("" (hide "final") (("" (expand "roots_closed_int" :assert? none) (("" (skoletin -2) (("" (label "newaname" -2) (("" (skoletin -1) (("" (replace -3 :dir rl) (("" (label "Pname" -2) (("" (skoletin -1) (("" (label "Nname" -2) (("" (skoletin -1) (("" (label "Mname" -2) (("" (skoletin -1) (("" (label "nscnormname" -2) (("" (skoletin -1) (("" (label "nschighlowname" -2) (("" (skoletin -1) (("" (label "newlowname" -2) (("" (skoletin -1) (("" (label "newhighname" -2) (("" (skoletin -1) (("" (label "Nrootsname" -2) (("" (skoletin -1) (("" (label "adjlowname" -2) (("" (replace -2) (("" (assert) (("" (case "NOT polynomial(a,n) = polynomial(newa,n)") (("1" (hide -) (("1" (decompose-equality) (("1" (lemma "poly_eq_le_degree") (("1" (inst?) (("1" (assert) (("1" (skeep) (("1" (expand "newa" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "computed_sturm_spec") (("2" (inst - "newa" "n") (("2" (assert) (("2" (replace "slname" :dir rl) (("2" (replace "Pname" :dir rl) (("2" (replace "Nname" :dir rl) (("2" (label "polyeq" -2) (("2" (split -) (("1" (flatten) (("1" (label "css" -1) (("1" (replace "Mname" :dir rl) (("1" (assert) (("1" (case "NOT (P(0) = newa AND N(0) = n)") (("1" (expand "P" 1) (("1" (expand "N" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (case "NOT (P(1) = poly_deriv(newa) AND N(1) = n-1)") (("1" (expand "constructed_sturm_sequence?" "css") --> -------------------- --> maximum size reached --> --------------------
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.661Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-02) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26