|
(number_sign_changes
(number_sign_changes_TCC1 0
(number_sign_changes_TCC1-1 nil 3583752897 ("" (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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(number_sign_changes_TCC2 0
(number_sign_changes_TCC2-1 nil 3583752897
("" (termination-tcc) nil nil) nil nil))
(sign_changes_TCC1 0
(sign_changes_TCC1-1 nil 3623871525 ("" (subtype-tcc) nil nil) nil
nil))
(sign_changes_TCC2 0
(sign_changes_TCC2-1 nil 3623871525 ("" (subtype-tcc) nil nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(sign_changes_TCC3 0
(sign_changes_TCC3-1 nil 3623871525 ("" (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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(sign_changes_TCC4 0
(sign_changes_TCC4-1 nil 3623871525 ("" (termination-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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(/= const-decl "boolean" notequal nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/"))
nil))
(sign_changes_TCC5 0
(sign_changes_TCC5-1 nil 3623871525
("" (skeep) (("" (assert) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(sign_changes_TCC6 0
(sign_changes_TCC6-1 nil 3623871525
("" (skeep)
(("" (typepred "v(a, n, i + 1, num + 1, a(i))")
(("1" (assert)
(("1" (hide 6)
(("1" (expand "number_sign_changes" +)
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(subrange type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(NSC type-eq-decl nil number_sign_changes 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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(sign_changes_TCC7 0
(sign_changes_TCC7-1 nil 3623871525 ("" (termination-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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
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)
(/= const-decl "boolean" notequal nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/"))
nil))
(sign_changes_TCC8 0
(sign_changes_TCC8-1 nil 3623871525 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(sign_changes_TCC9 0
(sign_changes_TCC9-1 nil 3623871525
("" (skeep)
(("" (typepred "v(a, n, i + 1, num, a(i))")
(("1" (assert)
(("1" (hide 5)
(("1" (expand "number_sign_changes" +)
(("1" (assert)
(("1" (lift-if)
(("1" (assert)
(("1" (split)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(subrange type-eq-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(NSC type-eq-decl nil number_sign_changes nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(sign_changes_TCC10 0
(sign_changes_TCC10-1 nil 3623871525 ("" (termination-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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
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)
(/= const-decl "boolean" notequal nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/"))
nil))
(sign_changes_TCC11 0
(sign_changes_TCC11-1 nil 3623871525 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(sign_changes_TCC12 0
(sign_changes_TCC12-1 nil 3623872259
("" (skeep)
(("" (typepred "v(a, n, i + 1, num,lastnz)")
(("1" (assert)
(("1" (hide 4)
(("1" (expand "number_sign_changes" +)
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(subrange type-eq-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(NSC type-eq-decl nil number_sign_changes nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(num_sign_changes_def_TCC1 0
(num_sign_changes_def_TCC1-1 nil 3623929782
("" (subtype-tcc) nil nil) nil nil))
(num_sign_changes_def 0
(num_sign_changes_def-1 nil 3623929808
("" (skeep)
(("" (typepred "sign_changes(a, i, 1, 0, a(0))")
(("" (assert)
(("" (hide 2)
(("" (expand "number_sign_changes") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((sign_changes def-decl "{m: nat |
LET nsci = number_sign_changes(a, i - 1),
nscn = number_sign_changes(a, n)
IN num = nsci`num AND lastnz = nsci`lastnz IMPLIES m = nscn`num}"
number_sign_changes nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(subrange type-eq-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(<= const-decl "bool" reals nil)
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(NSC type-eq-decl nil number_sign_changes nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(number_sign_changes_lastnz_nonzero 0
(number_sign_changes_lastnz_nonzero-1 nil 3587474296
("" (induct "i")
(("1" (skeep) (("1" (grind) nil nil)) nil)
("2" (skolem 1 "jj")
(("2" (flatten)
(("2" (skeep)
(("2" (inst - "a")
(("2" (flatten)
(("2" (assert)
(("2" (split +)
(("1" (flatten)
(("1" (expand "number_sign_changes" -1)
(("1" (lift-if)
(("1" (assert)
(("1" (split -)
(("1" (propax) nil nil)
("2" (flatten)
(("2"
(skeep)
(("2"
(split -)
(("1" (propax) nil nil)
("2"
(flatten)
(("2"
(assert)
(("2"
(inst - "j")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "number_sign_changes" 1)
(("2" (lift-if)
(("2" (lift-if)
(("2" (assert)
(("2" (split +)
(("1"
(flatten)
(("1"
(assert)
(("1"
(skeep)
(("1"
(inst - "j")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(inst-cp - "1+jj")
(("2"
(assert)
(("2"
(assert)
(("2"
(skeep)
(("2"
(inst - "j")
(("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)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat_induction formula-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(NSC type-eq-decl nil number_sign_changes nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types 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))
shostak))
(number_sign_changes_lastnz 0
(number_sign_changes_lastnz-1 nil 3617963493
("" (skeep)
(("" (expand "number_sign_changes")
(("" (lift-if) (("" (lift-if) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((number_sign_changes def-decl "NSC" number_sign_changes nil))
shostak))
(number_sign_changes_eq 0
(number_sign_changes_eq-1 nil 3618670663
("" (induct "i")
(("1" (assert) nil nil) ("2" (grind) nil nil)
("3" (skolem 1 "jj")
(("3" (flatten)
(("3" (skeep)
(("3" (inst - "a" "b")
(("3" (assert)
(("3" (split -)
(("1" (flatten)
(("1" (case "a(1+jj) /= 0 IFF b(1+jj) /= 0")
(("1" (expand "number_sign_changes" +)
(("1" (replace -1)
(("1" (lift-if)
(("1" (assert)
(("1" (lift-if)
(("1"
(assert)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(assert)
(("1"
(lift-if)
(("1"
(assert)
(("1"
(replace -3)
(("1"
(inst-cp -4 "1+jj")
(("1"
(assert)
(("1"
(ground)
(("1"
(expand
"sign_ext"
-3)
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil)
("2"
(expand
"sign_ext"
-4)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst - "1+jj")
(("2" (expand "sign_ext" -3)
(("2" (lift-if)
(("2" (assert)
(("2" (lift-if)
(("2"
(assert)
(("2"
(lift-if)
(("2"
(assert)
(("2"
(lift-if)
(("2"
(assert)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep) (("2" (inst - "j") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(IFF const-decl "[bool, bool -> bool]" booleans 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(NSC type-eq-decl nil number_sign_changes nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types 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))
nil))
(number_sign_changes_easy 0
(number_sign_changes_easy-1 nil 3609153569 ("" (grind) nil nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(testseqaa1 const-decl "real" number_sign_changes nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(testseqaa2 const-decl "sequence[real]" number_sign_changes nil))
shostak))
(number_sign_changes_test1 0
(number_sign_changes_test1-1 nil 3583753506
("" (induct "i")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (assert)
(("2" (expand "number_sign_changes" +)
(("2" (assert)
(("2" (lift-if)
(("2" (split +)
(("1" (flatten)
(("1" (replace -1)
(("1" (assert)
(("1" (expand "testseqaa1")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replaces -1)
(("2" (hide-all-but 1)
(("2" (split)
(("1" (grind) nil nil)
("2" (expand "testseqaa1")
(("2" (expand "^")
(("2" (expand "expt" - 1)
(("2" (grind :exclude "expt") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(int_minus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(expt def-decl "real" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(int_expt application-judgement "int" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_exp application-judgement "int" exponentiation nil)
(nat_induction formula-decl nil naturalnumbers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(testseqaa1 const-decl "real" number_sign_changes nil)
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NSC type-eq-decl nil number_sign_changes nil)
(pred type-eq-decl nil defined_types 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
shostak))
(number_sign_changes_test2 0
(number_sign_changes_test2-1 nil 3583754297 ("" (grind) nil nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(testseqaa1 const-decl "real" number_sign_changes nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(testseqaa2 const-decl "sequence[real]" number_sign_changes nil))
shostak))
(number_sign_changes_test3 0
(number_sign_changes_test3-1 nil 3583754329 ("" (grind) nil nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(testseqaa1 const-decl "real" number_sign_changes nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(testseqaa2 const-decl "sequence[real]" number_sign_changes nil))
shostak))
(number_sign_changes_test4 0
(number_sign_changes_test4-1 nil 3583754381 ("" (grind) nil nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(testseqaa1 const-decl "real" number_sign_changes nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(testseqaa3 const-decl "sequence[real]" number_sign_changes nil)
(testseqaa2 const-decl "sequence[real]" number_sign_changes nil))
shostak))
(number_sign_changes_test5 0
(number_sign_changes_test5-1 nil 3583754416 ("" (grind) nil nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(testseqaa1 const-decl "real" number_sign_changes nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(testseqaa3 const-decl "sequence[real]" number_sign_changes nil)
(testseqaa2 const-decl "sequence[real]" number_sign_changes nil))
shostak))
(number_sign_changes_test6 0
(number_sign_changes_test6-1 nil 3583754487 ("" (grind) nil nil)
((int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(testseqaa1 const-decl "real" number_sign_changes nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(testseqaa4 const-decl "sequence[real]" number_sign_changes nil))
shostak))
(number_sign_changes_test7 0
(number_sign_changes_test7-1 nil 3583754626 ("" (grind) nil nil)
((int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sign_ext const-decl
"{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}"
sign "reals/")
(number_sign_changes def-decl "NSC" number_sign_changes nil)
(testseqaa5 const-decl "real" number_sign_changes nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil))
shostak))
(nsc_regular_swap_TCC1 0
(nsc_regular_swap_TCC1-1 nil 3589123618 ("" (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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(nsc_regular_swap 0
(nsc_regular_swap-2 nil 3589189259
("" (induct "d")
(("1" (assert) nil nil)
("2" (skeep)
(("2" (assert)
(("2" (case "NOT k = 0")
(("1" (assert) nil nil)
("2" (replaces -1)
(("2" (expand "number_sign_changes" +)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (skolem 1 "dd")
(("3" (flatten)
(("3" (skeep)
(("3" (case "NOT k = dd+1")
(("1" (inst - "a" "b" "k")
(("1" (assert)
(("1" (replace -3)
(("1" (replace -5) (("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (assert)
(("2" (replace -1)
(("2" (assert)
(("2" (label "abnz" -6)
(("2" (label "abeq" -5)
(("2" (hide -3)
(("2" (invoke (case "NOT %1") (! 1 1))
(("1" (hide 2)
(("1" (expand "number_sign_changes" +)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(assert)
(("1"
(ground)
(("1"
(expand
"sign_ext"
"abeq")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil)
("2"
(expand
"sign_ext"
"abeq")
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil)
("3"
(copy "abnz")
(("3"
(inst - "dd")
(("3"
(assert)
(("3"
(flatten)
(("3"
(assert)
(("3"
(expand
"number_sign_changes"
+)
(("3"
(lift-if)
(("3"
(case
"sign_ext(a(dd)) = sign_ext(b(dd))")
(("1"
(assert)
nil
nil)
("2"
(hide
4)
(("2"
(assert)
(("2"
(inst
-7
"dd")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4"
(expand
"sign_ext"
"abeq")
(("4"
(lift-if)
(("4"
(ground)
nil
nil))
nil))
nil)
("5"
(copy "abnz")
(("5"
(inst - "dd")
(("5"
(assert)
(("5"
(flatten)
(("5"
(expand
"number_sign_changes"
-2)
(("5"
(assert)
(("5"
(lift-if)
(("5"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("6"
(expand
"sign_ext"
"abeq")
(("6"
(lift-if)
(("6"
(ground)
nil
nil))
nil))
nil)
("7"
(replace -1)
(("7"
(expand
"sign_ext"
-2
1)
(("7"
(copy
"abnz")
(("7"
(inst
-
"dd")
(("7"
(assert)
(("7"
(flatten)
(("7"
(expand
"number_sign_changes"
-2)
(("7"
(assert)
(("7"
(lift-if)
(("7"
(expand
"sign_ext"
-2)
(("7"
(lift-if)
(("7"
(lift-if)
(("7"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("8"
(expand
"sign_ext"
"abeq")
(("8"
(lift-if)
(("8"
(ground)
nil
nil))
nil))
nil)
("9"
(copy "abnz")
(("9"
(inst - "dd")
(("9"
(assert)
(("9"
(flatten)
(("9"
(expand
"number_sign_changes"
-4)
(("9"
(assert)
(("9"
(lift-if)
(("9"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("10"
(expand
"sign_ext"
"abeq")
(("10"
(lift-if)
(("10"
(ground)
nil
nil))
nil))
nil)
("11"
(copy "abnz")
(("11"
(inst - "dd")
(("11"
(assert)
(("11"
(flatten)
(("11"
(assert)
(("11"
(replace
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.117 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.
|
