|
(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)
(("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)
(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)
(("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 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
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.45 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.
|
