| products/sources/formale sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: csequence_subsequence.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(csequence_subsequence
(subsequence?_TCC1 0 (subsequence?_TCC1-1 nil 3513623233 ("" (subtype-tcc) nil nil) ((indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth 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) (number nonempty-type-decl nil numbers nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (subsequence?_empty_left 0 (subsequence?_empty_left-1 nil 3513623678 ("" (expand "subsequence?") (("" (propax) nil nil)) nil) ((subsequence? coinductive-decl "bool" csequence_subsequence nil)) shostak)) (subsequence?_empty_right 0 (subsequence?_empty_right-1 nil 3513623690 ("" (skolem!) (("" (expand "subsequence?") (("" (ground) (("" (skosimp :preds? t) (("" (expand "index?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((subsequence? coinductive-decl "bool" csequence_subsequence nil) (indexes type-eq-decl nil csequence_nth nil) (empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (index? def-decl "bool" csequence_nth 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) (number nonempty-type-decl nil numbers nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence 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)) shostak)) (subsequence?_rest1 0 (subsequence?_rest1-1 nil 3513623724 ("" (skosimp) (("" (lemma "subsequence?_coinduction") (("" (inst - "LAMBDA cseq1, cseq2: EXISTS nseq1, nseq2: cseq1 = rest(nseq1) AND cseq2 = rest( (("" (split) (("1" (inst - "rest(nseq1!1)" "rest(nseq2!1)") (("1" (assert) (("1" (inst + "nseq1!1" "nseq2!1") nil nil)) nil)) nil) ("2" (delete -1 2) (("2" (skosimp*) (("2" (expand "subsequence?" -) (("2" (skosimp :preds? t) (("2" (expand "subsequence?" -) (("2" (assert) (("2" (skosimp :preds? t) (("2" (rewrite "suffix_nth") (("2" (rewrite "suffix_suffix") (("2" (rewrite "suffix_index") (("2" (expand "index?" -1) (("2" (assert) (("2" (inst + "n!1 + n!2") (("2" (expand "nth" -6) (("2" (ground) (("2" (replace -4) (("2" (rewrite "suffix_rest1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subsequence?_coinduction formula-decl nil csequence_subsequence nil) (indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (suffix_nth formula-decl nil csequence_suffix nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (suffix_index formula-decl nil csequence_suffix nil) (nth def-decl "T" csequence_nth nil) (suffix_rest1 formula-decl nil csequence_suffix nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (suffix_suffix formula-decl nil csequence_suffix nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (suffix? inductive-decl "bool" csequence_suffix nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence nil)) shostak)) (subsequence?_rest2 0 (subsequence?_rest2-1 nil 3513623860 ("" (skosimp) (("" (lemma "subsequence?_coinduction") (("" (inst - "LAMBDA cseq1, cseq2: nonempty?(cseq2) AND subsequence?(cseq1, rest(cseq2))") (("" (split) (("1" (inst - "cseq!1" "nseq!1") (("1" (assert) nil nil)) nil) ("2" (delete -1 2) (("2" (skosimp) (("2" (expand "subsequence?" -) (("2" (assert) (("2" (skosimp) (("2" (inst + "1 + n!1") (("1" (rewrite "suffix_rest1") (("1" (expand "nth" +) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "index?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subsequence?_coinduction formula-decl nil csequence_subsequence nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (n!1 skolem-const-decl "indexes[T](rest(cseq2!1))" csequence_subsequence nil) (indexes type-eq-decl nil csequence_nth nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cseq2!1 skolem-const-decl "csequence[T]" csequence_subsequence nil) (index? def-decl "bool" csequence_nth 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) (number nonempty-type-decl nil numbers nil) (nth def-decl "T" csequence_nth nil) (suffix_rest1 formula-decl nil csequence_suffix nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence nil)) shostak)) (subsequence?_extensionality 0 (subsequence?_extensionality-1 nil 3513623921 ("" (skosimp) (("" (expand "subsequence?" +) (("" (inst + 0) (("1" (expand* "nth" "suffix" "suffix") (("1" (assert) nil nil)) nil) ("2" (expand "index?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((subsequence? coinductive-decl "bool" csequence_subsequence nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (nth def-decl "T" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (T formal-type-decl nil csequence_subsequence nil) (csequence type-decl nil csequence_codt 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) (index? def-decl "bool" csequence_nth nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (nseq2!1 skolem-const-decl "nonempty_csequence[T]" csequence_subsequence nil)) shostak)) (subsequence?_finite 0 (subsequence?_finite-1 nil 3513623956 ("" (measure-induct+ "length(fseq)" ("fseq")) (("" (skosimp) (("" (expand "subsequence?" -2) (("" (expand "is_finite" +) (("" (prop) (("" (skosimp :preds? t) (("" (inst - "suffix(x!1, 1 + n!1)") (("" (inst - "rest(cseq!1)") (("" (rewrite "suffix_length") (("" (expand "max") (("" (rewrite "index?_finite") (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (index? def-decl "bool" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (index?_finite formula-decl nil csequence_nth nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (suffix_length formula-decl nil csequence_suffix nil) (suffix? inductive-decl "bool" csequence_suffix nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (suffix_is_finite application-judgement "finite_csequence" csequence_subsequence nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (naturalnumber 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) (number nonempty-type-decl nil numbers nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (subsequence?_nth 0 (subsequence?_nth-1 nil 3513624052 ("" (skosimp) (("" (induct "n") (("1" (assert) nil nil) ("2" (flatten) (("2" (expand "index?") (("2" (expand "subsequence?" -) (("2" (assert) (("2" (skosimp) (("2" (inst + "n!1") (("2" (expand "nth" 1 1) (("2" (assert) (("2" (rewrite "suffix_1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) (("3" (lemma "index?_lt") (("3" (inst - "cseq1!1" "1 + j!1" "j!1") (("3" (assert) (("3" (skosimp) (("3" (expand "subsequence?" -3) (("3" (split) (("1" (rewrite "length_empty?_rew") (("1" (flatten) (("1" (rewrite "suffix_is_infinite") (("1" (rewrite "suffix_length") (("1" (rewrite "index?_finite" -6) (("1" (expand "max") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp :preds? t) (("2" (rewrite "suffix_rest2") (("2" (rewrite "suffix_suffix") (("2" (rewrite "suffix_index") (("2" (rewrite "suffix_nth") (("2" (use "index?_nonempty" ("cseq" "cseq1!1")) (("2" (rewrite "suffix_first") (("2" (inst + "1 + m!1 + n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" 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) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil csequence_subsequence nil) (csequence type-decl nil csequence_codt nil) (index? def-decl "bool" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (nth def-decl "T" csequence_nth nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (suffix? inductive-decl "bool" csequence_suffix nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat_induction formula-decl nil naturalnumbers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (suffix_1 formula-decl nil csequence_suffix nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (suffix_length formula-decl nil csequence_suffix nil) (int_minus_int_is_int application-judgement "int" integers nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (index?_finite formula-decl nil csequence_nth nil) (suffix_is_infinite judgement-tcc nil csequence_suffix nil) (NOT const-decl "[bool -> bool]" booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (infinite_csequence type-eq-decl nil csequence_props nil) (length_empty?_rew formula-decl nil csequence_length nil) (suffix_rest2 formula-decl nil csequence_suffix nil) (suffix_index formula-decl nil csequence_suffix nil) (index?_nonempty formula-decl nil csequence_nth nil) (suffix_first formula-decl nil csequence_suffix nil) (suffix_nth formula-decl nil csequence_suffix nil) (suffix_suffix formula-decl nil csequence_suffix nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (index?_lt formula-decl nil csequence_nth nil)) shostak)) (subsequence?_concatenate_left 0 (subsequence?_concatenate_left-1 nil 3513624227 ("" (skosimp) (("" (induct "fseq" :name "is_finite_induction") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (expand "subsequence?" (-3 +)) (("3" (ground) (("1" (rewrite "o_empty_left") (("1" (skosimp :preds? t) (("1" (inst + "n!1") (("1" (assert) nil nil) ("2" (rewrite "o_index") (("2" (flatten) (("2" (rewrite "index?_finite") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp :preds? t) (("2" (case "index?(cseq!1 o cseq2!1)(length(cseq!1) + n!1)") (("1" (inst + "length(cseq!1) + n!1") (("1" (rewrite "o_nth") (("1" (assert) (("1" (rewrite "suffix_concatenate") (("1" (lift-if) (("1" (ground) (("1" (rewrite "index?_finite") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "o_index") (("2" (flatten) (("2" (rewrite "index?_finite") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (O const-decl "csequence" csequence_concatenate nil) (T formal-type-decl nil csequence_subsequence nil) (is_finite_induction formula-decl nil csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (n!1 skolem-const-decl "indexes[T](cseq2!1)" csequence_subsequence nil) (suffix_concatenate formula-decl nil csequence_suffix nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (o_nth formula-decl nil csequence_concatenate nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (o_empty_left formula-decl nil csequence_concatenate nil) (cseq!1 skolem-const-decl "csequence[T]" csequence_subsequence nil) (cseq2!1 skolem-const-decl "csequence[T]" csequence_subsequence nil) (n!1 skolem-const-decl "indexes[T](cseq2!1)" csequence_subsequence nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (index?_finite formula-decl nil csequence_nth nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (o_index formula-decl nil csequence_concatenate 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (index? def-decl "bool" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil)) shostak)) (subsequence?_concatenate_right 0 (subsequence?_concatenate_right-1 nil 3513624405 ("" (measure-induct+ "IF is_finite(cseq2) THEN length(cseq2) ELSE 0 ENDIF" ("cseq2")) (("" (skosimp*) (("" (rewrite "o_infinite") (("" (expand "subsequence?" (-3 +)) (("" (ground) (("" (skosimp :preds? t) (("" (inst + "n!1") (("1" (rewrite "o_nth") (("1" (lift-if) (("1" (rewrite "index?_finite") (("1" (ground) (("1" (inst - "suffix(x!1, 1 + n!1)") (("1" (inst - "rest(cseq1!1)") (("1" (use "suffix_is_finite" ("fseq" "x!1")) (("1" (assert) (("1" (rewrite "suffix_length") (("1" (expand "max") (("1" (lift-if) (("1" (assert) (("1" (inst - "cseq!1") (("1" (rewrite "suffix_concatenate") (("1" (use "suffix_empty") (("1" (lift-if) (("1" (ground) (("1" (rewrite "o_empty_left") (("1" (rewrite "index?_finite") (("1" (expand "suffix") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "o_index") (("2" (rewrite "index?_finite") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "index?_prop") (("2" (rewrite "index?_finite") (("2" (flatten) (("2" (forward-chain "o_finiteness") (("2" (rewrite "o_length") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((index? def-decl "bool" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (index?_prop formula-decl nil csequence_nth nil) (o_length formula-decl nil csequence_concatenate nil) (o_finiteness formula-decl nil csequence_concatenate nil) (o_nth formula-decl nil csequence_concatenate nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (index?_finite formula-decl nil csequence_nth nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (suffix? inductive-decl "bool" csequence_suffix nil) (suffix_is_finite judgement-tcc nil csequence_suffix nil) (suffix_length formula-decl nil csequence_suffix 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) (suffix_empty formula-decl nil csequence_suffix nil) (int_plus_int_is_int application-judgement "int" integers nil) (o_empty_left formula-decl nil csequence_concatenate nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (suffix_concatenate formula-decl nil csequence_suffix nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (o_index formula-decl nil csequence_concatenate nil) (n!1 skolem-const-decl "indexes[T](x!1)" csequence_subsequence nil) (cseq!1 skolem-const-decl "csequence[T]" csequence_subsequence nil) (x!1 skolem-const-decl "csequence[T]" csequence_subsequence nil) (o_infinite formula-decl nil csequence_concatenate nil) (NOT const-decl "[bool -> bool]" booleans nil) (infinite_csequence type-eq-decl nil csequence_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (O const-decl "csequence" csequence_concatenate nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (naturalnumber 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) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (subsequence?_prefix 0 (subsequence?_prefix-1 nil 3513624596 ("" (lemma "subsequence?_coinduction") (("" (inst - "LAMBDA cseq1, cseq2: EXISTS cseq, n, m: n <= m AND cseq1 = prefix(cseq, n) AND cseq2 = prefix(cseq, m)") (("" (split) (("1" (skosimp) (("1" (inst - "prefix(cseq!1, n!1)" "prefix(cseq!1, m!1)") (("1" (assert) (("1" (inst + "cseq!1" "n!1" "m!1") nil nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skosimp*) (("2" (case "n!1 = 0") (("1" (expand "prefix" -) (("1" (ground) nil nil)) nil) ("2" (assert) (("2" (inst + 0) (("1" (expand "nth") (("1" (replace*) (("1" (hide -2 -3) (("1" (expand "prefix" 2) (("1" (expand "prefix" 3 2) (("1" (expand "prefix" 3 1) (("1" (lift-if) (("1" (ground) (("1" (inst + "rest(cseq!1)" "n!1 - 1" "m!1 - 1") (("1" (assert) (("1" (rewrite "prefix_rest") (("1" (rewrite "suffix_1") (("1" (rewrite "prefix_rest") nil nil) ("2" (expand "prefix" (1 5)) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "index?" "prefix") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_subsequence nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil 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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (prefix def-decl "{fseq | prefix?(fseq, cseq)}" csequence_prefix nil) (index? def-decl "bool" csequence_nth nil) (cseq2!1 skolem-const-decl "csequence[T]" csequence_subsequence nil) (indexes type-eq-decl nil csequence_nth nil) (add_finite application-judgement "nonempty_finite_csequence[T]" csequence_subsequence nil) (int_minus_int_is_int application-judgement "int" integers nil) (suffix_is_finite application-judgement "finite_csequence" csequence_subsequence nil) (suffix_1 formula-decl nil csequence_suffix nil) (int_plus_int_is_int application-judgement "int" integers nil) (prefix_rest formula-decl nil csequence_prefix nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nth def-decl "T" csequence_nth nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subsequence?_coinduction formula-decl nil csequence_subsequence nil)) shostak)) (subsequence?_suffix 0 (subsequence?_suffix-1 nil 3513624766 ("" (lemma "subsequence?_coinduction") (("" (inst - "LAMBDA cseq1, cseq2: EXISTS cseq, n, m: n <= m AND cseq1 = suffix(cseq, m) AND cseq2 = suffix(cseq, n)") (("" (split) (("1" (skosimp) (("1" (inst - "suffix(cseq!1, m!1)" "suffix(cseq!1, n!1)") (("1" (assert) (("1" (inst + "cseq!1" "n!1" "m!1") nil nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skosimp*) (("2" (inst + "m!1 - n!1") (("1" (replace*) (("1" (hide -2 -3) (("1" (prop) (("1" (rewrite "suffix_nth") (("1" (rewrite "suffix_first") (("1" (expand "suffix" 3) (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst + "cseq!1" "m!1 + 1" "m!1 + 1") (("2" (assert) (("2" (rewrite "suffix_suffix") (("2" (rewrite "suffix_rest2") (("2" (use "suffix_empty") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace*) (("2" (hide -2 -3) (("2" (rewrite "suffix_index") (("2" (use "suffix_empty") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_subsequence nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil 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) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (suffix? inductive-decl "bool" csequence_suffix nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (m!1 skolem-const-decl "nat" csequence_subsequence nil) (n!1 skolem-const-decl "nat" csequence_subsequence nil) (index? def-decl "bool" csequence_nth nil) (cseq2!1 skolem-const-decl "csequence[T]" csequence_subsequence nil) (indexes type-eq-decl nil csequence_nth nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (suffix_suffix formula-decl nil csequence_suffix nil) (suffix_empty formula-decl nil csequence_suffix nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (suffix_rest2 formula-decl nil csequence_suffix nil) (suffix_nth formula-decl nil csequence_suffix nil) (int_plus_int_is_int application-judgement "int" integers nil) (suffix_first formula-decl nil csequence_suffix nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (suffix_index formula-decl nil csequence_suffix nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (subsequence?_coinduction formula-decl nil csequence_subsequence nil)) shostak)) (subsequence?_length 0 (subsequence?_length-1 nil 3513624909 ("" (measure-induct+ "length(fseq1) + length(fseq2)" ("fseq1" "fseq2") :skolem-typepreds? t) (("" (expand "is_finite" -1) (("" (expand "subsequence?" -4) (("" (rewrite "length_empty?_rew") (("" (ground) (("" (skosimp :preds? t) (("" (use "index?_nonempty") (("" (lemma "suffix_is_finite" ("fseq" "x!2" "n" "1 + n!1")) (("" (inst - "rest(x!1)" "suffix(x!2, 1 + n!1)") (("" (expand "length" -8 3) (("" (rewrite "suffix_length") (("" (expand "max") (("" (expand "length" 1 1) (("" (lift-if) (("" (lift-if) (("" (lift-if) (("" (ground) (("" (lemma "length_empty?_rew" ("cseq" "x!2")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((length_empty?_rew formula-decl nil csequence_length nil) (index? def-decl "bool" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (suffix_is_finite judgement-tcc nil csequence_suffix nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (suffix_length formula-decl nil csequence_suffix nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (suffix? inductive-decl "bool" csequence_suffix nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (suffix_is_finite application-judgement "finite_csequence" csequence_subsequence nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (index?_nonempty formula-decl nil csequence_nth nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (<= const-decl "bool" reals nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (naturalnumber 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) (number nonempty-type-decl nil numbers nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence nil) (measure_induction formula-decl nil measure_induction nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (subsequence?_length_eq 0 (subsequence?_length_eq-1 nil 3513625045 ("" (measure-induct+ "length(fseq1) + length(fseq2)" ("fseq1" "fseq2") :skolem-typepreds? t) (("" (expand "subsequence?" -4) (("" (lemma "length_empty?_rew") (("" (inst-cp - "x!2") (("" (inst - "x!1") (("" (ground) (("" (skosimp :preds? t) (("" (lemma "suffix_is_finite" ("fseq" "x!2" "n" "1 + n!1")) (("" (expand "is_finite" -5) (("" (inst - "rest(x!1)" "suffix(x!2, 1 + n!1)") (("" (expand "length" -7 3) (("" (forward-chain "subsequence?_length") (("" (rewrite "suffix_length") (("" (expand "max") (("" (expand "length" -9 1) (("" (lift-if) (("" (ground) (("1" (expand* "nth" "suffix" "suffix") (("1" (forward-chain "csequence_add_extensionality") nil nil)) nil) ("2" (rewrite "index?_finite") (("2" (expand* "nth" "suffix" "suffix") (("2" (use "csequence_add_extensionality") (("2" (ground) 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) (suffix_is_finite judgement-tcc nil csequence_suffix nil) (suffix_is_finite application-judgement "finite_csequence" csequence_subsequence nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (x!1 skolem-const-decl "finite_csequence[T]" csequence_subsequence nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (suffix? inductive-decl "bool" csequence_suffix nil) (subsequence?_length formula-decl nil csequence_subsequence nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (index?_finite formula-decl nil csequence_nth nil) (nth def-decl "T" csequence_nth nil) (csequence_add_extensionality formula-decl nil csequence_codt nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers nil) (suffix_length formula-decl nil csequence_suffix nil) (indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth nil) (length_empty?_rew formula-decl nil csequence_length nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (= const-decl "[T, T -> boolean]" equalities nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (has_length def-decl "bool" csequence_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (naturalnumber 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) (number nonempty-type-decl nil numbers nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence nil) (measure_induction formula-decl nil measure_induction nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) shostak)) (subsequence?_is_preorder 0 (subsequence?_is_preorder-1 nil 3513623233 ("" (expand* "preorder?" "reflexive?" "transitive?") (("" (split) (("1" (skolem!) (("1" (lemma "subsequence?_suffix") (("1" (inst - "x!1" 0 0) (("1" (expand "suffix") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "subsequence?_weak_coinduction") (("2" (inst - "LAMBDA cseq1, cseq2: EXISTS (cseq3: csequence): subsequence?(cseq1, cseq3) AND (("2" (split) (("1" (skosimp) (("1" (inst - "x!1" "z!1") (("1" (assert) (("1" (inst + "y!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skosimp*) (("2" (lemma "subsequence?_nth" ("cseq1" "cseq3!1" "cseq2" "cseq2!1")) (("2" (assert) (("2" (expand "subsequence?" -2) (("2" (skosimp) (("2" (inst - "n!1") (("2" (skosimp) (("2" (inst + "m!1") (("2" (assert) (("2" (inst + "suffix(cseq3!1, 1 + n!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((subsequence?_suffix formula-decl nil csequence_subsequence nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix 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) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_subsequence nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (subsequence?_nth formula-decl nil csequence_subsequence nil) (index? def-decl "bool" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (suffix? inductive-decl "bool" csequence_suffix nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (subsequence?_weak_coinduction formula-decl nil csequence_subsequence nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (reflexive? const-decl "bool" relations nil)) nil)) (subsequence?_finite_antisymmetric 0 (subsequence?_finite_antisymmetric-1 nil 3513625250 ("" (lemma "subsequence?_is_preorder") (("" (use "preorder_restrict[csequence, finite_csequence]") (("" (expand "partial_order?") (("" (hide -1 -2) (("" (expand* "restrict" "antisymmetric?") (("" (skosimp) (("" (lemma "subsequence?_length") (("" (inst-cp - "y!1" "x!1") (("" (inst - "x!1" "y!1") (("" (use "subsequence?_length_eq") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((preorder_restrict judgement-tcc nil restrict_order_props nil) (T formal-type-decl nil csequence_subsequence nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (pred type-eq-decl nil defined_types nil) (preorder? const-decl "bool" orders nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (subsequence?_is_preorder name-judgement "(preorder?[csequence])" csequence_subsequence nil) (preorder_restrict application-judgement "(preorder?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (reflexive_restrict application-judgement "(reflexive?[S])" restrict_order_props nil) (subsequence?_length_eq formula-decl nil csequence_subsequence nil) (subsequence?_length formula-decl nil csequence_subsequence nil) (restrict const-decl "R" restrict nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (subsequence?_is_preorder judgement-tcc nil csequence_subsequence nil)) shostak)) (prefix?_is_subsequence? 0 (prefix?_is_subsequence?-1 nil 3513623233 ("" (lemma "subsequence?_weak_coinduction") (("" (inst - "prefix?") (("" (split) (("1" (skolem!) (("1" (inst - "x!1" "cseq!1") (("1" (assert) nil nil)) nil)) nil) ("2" (delete 2) (("2" (skosimp) (("2" (expand "prefix?" -) (("2" (ground) (("2" (lemma "suffix_1" ("nseq" "cseq2!1")) (("2" (rewrite "index?_0") (("2" (inst + 0) (("2" (expand "nth") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil csequence_subsequence nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (suffix_1 formula-decl nil csequence_suffix nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (cseq2!1 skolem-const-decl "csequence[T]" csequence_subsequence nil) (index? def-decl "bool" csequence_nth 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) (number nonempty-type-decl nil numbers nil) (indexes type-eq-decl nil csequence_nth nil) (nth def-decl "T" csequence_nth nil) (index?_0 formula-decl nil csequence_nth nil) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_subsequence nil) (subsequence?_is_preorder name-judgement "(preorder?[csequence])" csequence_subsequence nil) (subsequence?_weak_coinduction formula-decl nil csequence_subsequence nil)) nil)) (suffix?_is_subsequence? 0 (suffix?_is_subsequence?-1 nil 3513623233 ("" (skolem-typepred) (("" (lemma "suffix?_induction") (("" (inst - "x!1" "LAMBDA cseq: subsequence?(x!1, cseq)") (("" (split) (("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil) ("2" (delete -1 2) (("2" (skosimp) (("2" (prop) (("1" (lemma "subsequence?_is_preorder") (("1" (expand* "preorder?" "reflexive?") (("1" (flatten) (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (forward-chain "subsequence?_rest2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((suffix?_induction formula-decl nil csequence_suffix nil) (subsequence?_is_preorder name-judgement "(preorder?[csequence])" csequence_subsequence nil) (suffix?_is_preorder name-judgement "(preorder?[csequence])" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.44 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 |
