|
(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_pred(sigma(i1,i2,abc))")
(("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)
(("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)
(("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)
(("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)
(("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"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.126 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
