|
(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(nseq2) AND subsequence?(nseq1, nseq2)")
(("" (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 subsequence?(cseq3, cseq2)")
(("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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.89Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
