| products/Sources/formale Sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: fundamental_theorem.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.82 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.Bot Zugriff |
