| products/sources/formale sprachen/PVS/co_structures/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: environment.vdmpp Sprache: LispOriginal von: PVS© |
|
||||||
|
(csequence_flatten
(some_every_empty 0 (some_every_empty-1 nil 3513685323 ("" (skolem!) (("" (rewrite "every_some_rew") (("" (case-replace "pred_NOT(empty?) = nonempty?") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "pred_NOT") (("2" (reduce-with-ext) nil nil)) nil)) nil)) nil)) nil)) nil) ((every_some_rew formula-decl nil csequence_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (pred_NOT const-decl "bool" csequence_props nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (flatten_struct_TCC1 0 (flatten_struct_TCC1-1 nil 3513685291 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (every coinductive-decl "boolean" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_seq_seq type-eq-decl nil csequence_flatten nil)) nil)) (flatten_struct_TCC2 0 (flatten_struct_TCC2-1 nil 3513685291 ("" (skosimp :preds? t) (("" (expand "every") (("" (assert) nil nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (every coinductive-decl "boolean" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_seq_seq type-eq-decl nil csequence_flatten nil)) nil)) (flatten_struct_TCC3 0 (flatten_struct_TCC3-1 nil 3513685291 ("" (skosimp :preds? t) (("" (expand "every" -) (("" (assert) nil nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (every coinductive-decl "boolean" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_seq_seq type-eq-decl nil csequence_flatten nil)) nil)) (flatten_struct_TCC4 0 (flatten_struct_TCC4-1 nil 3513685291 ("" (skosimp :preds? t) (("" (expand "every") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (every coinductive-decl "boolean" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_seq_seq type-eq-decl nil csequence_flatten nil)) nil)) (flatten_TCC1 0 (flatten_TCC1-1 nil 3513685291 ("" (skolem!) (("" (use "filter_def") nil nil)) nil) ((nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (filter_def formula-decl nil csequence_filter nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil)) nil)) (flatten_empty 0 (flatten_empty-1 nil 3513685514 ("" (skolem!) (("" (expand "flatten") (("" (use "filter_nonempty") (("" (rewrite "some_every_empty") (("" (expand* "flatten_struct" "coreduce") (("" (reduce) nil nil)) nil)) nil)) nil)) nil)) nil) ((flatten const-decl "csequence[T]" csequence_flatten nil) (some_every_empty formula-decl nil csequence_flatten nil) (flatten_struct const-decl "csequence_struct[T, nonempty_seq_seq]" csequence_flatten nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (filter_nonempty formula-decl nil csequence_filter nil)) shostak)) (flatten_empty_cseq 0 (flatten_empty_cseq-1 nil 3513685553 ("" (skolem!) (("" (rewrite "flatten_empty") (("" (expand "every") (("" (propax) nil nil)) nil)) nil)) nil) ((flatten_empty formula-decl nil csequence_flatten nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (every coinductive-decl "boolean" csequence_codt nil)) shostak)) (flatten_nonempty 0 (flatten_nonempty-1 nil 3513685578 ("" (skolem!) (("" (use "flatten_empty") (("" (rewrite "some_every_empty") (("" (ground) nil nil)) nil)) nil)) nil) ((flatten_empty formula-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (some_every_empty formula-decl nil csequence_flatten nil)) shostak)) (flatten_filter 0 (flatten_filter-1 nil 3513685605 ("" (skolem!) (("" (expand "flatten") (("" (rewrite "filter_idem") nil nil)) nil)) nil) ((flatten const-decl "csequence[T]" csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (filter_idem formula-decl nil csequence_filter nil)) shostak)) (flatten_reduce_TCC1 0 (flatten_reduce_TCC1-1 nil 3513685291 ("" (subtype-tcc) nil nil) nil nil)) (flatten_reduce 0 (flatten_reduce-1 nil 3513685637 ("" (skosimp) (("" (expand "flatten") (("" (use "filter_rest") (("" (assert) nil nil)) nil)) nil)) nil) ((flatten const-decl "csequence[T]" csequence_flatten nil) (boolean nonempty-type-decl nil booleans nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (filter_rest formula-decl nil csequence_filter nil)) shostak)) (flatten_rest_TCC1 0 (flatten_rest_TCC1-1 nil 3513685291 ("" (skosimp) (("" (expand* "flatten" "flatten_struct" "coreduce") (("" (assert) nil nil)) nil)) nil) ((flatten_struct const-decl "csequence_struct[T, nonempty_seq_seq]" csequence_flatten nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (flatten const-decl "csequence[T]" csequence_flatten nil)) nil)) (flatten_rest_TCC2 0 (flatten_rest_TCC2-1 nil 3513685291 ("" (skosimp) (("" (use "filter_def") (("" (expand* "flatten" "flatten_struct" "coreduce" "every") (("" (reduce) nil nil)) nil)) nil)) nil) ((filter_def formula-decl nil csequence_filter nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (every coinductive-decl "boolean" csequence_codt nil) (flatten_struct const-decl "csequence_struct[T, nonempty_seq_seq]" csequence_flatten nil)) nil)) (flatten_rest 0 (flatten_rest-1 nil 3513685703 ("" (skosimp) (("" (use "filter_def") (("" (lemma "filter_full") (("" (inst-cp - "add(rest(first(filter(cseq!1, nonempty?))), rest(filter(cseq!1, nonempty?)))" "nonempty?") (("" (expand "every" (-2 -3)) (("" (expand* "flatten" "flatten_struct") (("" (expand "coreduce" 1 1) (("" (expand "coreduce" -) (("" (smash) (("" (use "filter_add") (("" (assert) (("" (inst - "rest(filter(cseq!1, nonempty?))" "nonempty?") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((filter_def formula-decl nil csequence_filter nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (filter const-decl "(LAMBDA (cseq1: csequence[T]): subsequence?(cseq1, cseq))" csequence_filter nil) (flatten_struct const-decl "csequence_struct[T, nonempty_seq_seq]" csequence_flatten nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (filter_add formula-decl nil csequence_filter nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (every coinductive-decl "boolean" csequence_codt nil) (filter_full formula-decl nil csequence_filter nil)) shostak)) (flatten_rest2_TCC1 0 (flatten_rest2_TCC1-1 nil 3513685291 ("" (skosimp) (("" (rewrite "flatten_nonempty") (("" (expand "some") (("" (assert) nil nil)) nil)) nil)) nil) ((flatten_nonempty formula-decl nil csequence_flatten nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (some inductive-decl "boolean" csequence_codt nil)) nil)) (flatten_rest2_TCC2 0 (flatten_rest2_TCC2-1 nil 3513685291 ("" (subtype-tcc) nil nil) nil nil)) (flatten_rest2 0 (flatten_rest2-1 nil 3513685831 ("" (skosimp) (("" (expand* "flatten" "flatten_struct") (("" (expand "coreduce" 3 1) (("" (smash) (("1" (use "filter_nonempty") (("1" (expand "some") (("1" (propax) nil nil)) nil)) nil) ("2" (use "filter_first_first") (("2" (assert) (("2" (expand "some") (("2" (use "filter_add") (("2" (assert) (("2" (use "filter_rest") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (use "filter_first_first") (("3" (assert) (("3" (expand "some") (("3" (use "filter_add") (("3" (assert) (("3" (use "filter_rest") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((flatten_struct const-decl "csequence_struct[T, nonempty_seq_seq]" csequence_flatten nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (some inductive-decl "boolean" csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (pred type-eq-decl nil defined_types nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (filter_nonempty formula-decl nil csequence_filter nil) (filter_add formula-decl nil csequence_filter nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (filter_rest formula-decl nil csequence_filter nil) (nonempty_csequence type-eq-decl nil csequence_props nil) (filter_first_first formula-decl nil csequence_filter nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil)) shostak)) (flatten_first 0 (flatten_first-1 nil 3513685921 ("" (expand* "flatten" "flatten_struct" "coreduce") (("" (reduce) nil nil)) nil) ((flatten const-decl "csequence[T]" csequence_flatten nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (flatten_struct const-decl "csequence_struct[T, nonempty_seq_seq]" csequence_flatten nil)) shostak)) (flatten_suffix 0 (flatten_suffix-1 nil 3513685945 ("" (lemma "some_induction[csequence[T]]") (("" (inst - "nonempty?" "LAMBDA cseq: some(nonempty?)(cseq) AND flatten(cseq) = flatten(suffix(cseq, fi (("" (split) (("1" (skosimp) (("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil)) nil) ("2" (delete 2) (("2" (skosimp) (("2" (lift-if) (("2" (ground) (("1" (expand "some") (("1" (propax) nil nil)) nil) ("2" (use "first_p_rest") (("2" (expand* "some" "suffix") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "some" +) (("3" (propax) nil nil)) nil) ("4" (use "first_p_rest") (("4" (expand "some" -1) (("4" (expand "suffix" +) (("4" (lift-if) (("4" (ground) (("4" (use "flatten_reduce") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (some inductive-decl "boolean" csequence_codt nil) (= const-decl "[T, T -> boolean]" equalities nil) (flatten const-decl "csequence[T]" csequence_flatten 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) (suffix? inductive-decl "bool" csequence_suffix nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (pred type-eq-decl nil defined_types nil) (index? def-decl "bool" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (first_p const-decl "indexes(cseq)" csequence_first_p nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (flatten_reduce formula-decl nil csequence_flatten nil) (first_p_rest formula-decl nil csequence_first_p nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (some_induction formula-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil)) shostak)) (flatten_concatenate 0 (flatten_concatenate-1 nil 3513686056 ("" (skosimp) (("" (case "is_finite(first(cseq!1))") (("1" (lemma "is_finite_induction[T]") (("1" (inst - "LAMBDA tseq: FORALL cseq: nonempty?(cseq) AND tseq = first(cseq) IMPLIES flatte (("1" (split) (("1" (inst - "first(cseq!1)") (("1" (assert) (("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (delete -1 -2 2) (("2" (skosimp*) (("2" (case "empty?(cseq!2)") (("1" (rewrite "o_empty_left") (("1" (use "flatten_reduce") (("1" (assert) nil nil)) nil)) nil) ("2" (ground) (("2" (use "flatten_nonempty") (("2" (expand "some") (("2" (replace -5) (("2" (hide -5) (("2" (inst - "add(rest(first(cseq!3)), rest(cseq!3))") (("2" (assert) (("2" (lemma "o_nonempty[T]") (("2" (inst - "first(cseq!3)" "flatten(rest(cseq!3))") (("2" (assert) (("2" (decompose-equality +) (("1" (rewrite "o_first") (("1" (lemma "filter_first_first") (("1" (inst - "cseq!3" "nonempty?") (("1" (assert) (("1" (expand "some") (("1" (forward-chain "flatten_first") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "o_rest") (("2" (use "flatten_rest2") (("2" (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_infinite") (("2" (lemma "coinduction[T]") (("2" (inst - "LAMBDA (tseq1, tseq2: csequence[T]): EXISTS cseq: nonempty?(cseq) AND tseq1 = f "flatten(cseq!1)" "first(cseq!1)") (("1" (assert) (("1" (inst + "cseq!1") nil nil)) nil) ("2" (delete -1 2 3) (("2" (expand "bisimulation?") (("2" (skosimp*) (("2" (replace*) (("2" (hide -2 -3) (("2" (smash) (("1" (rewrite "flatten_empty") (("1" (expand "every") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "is_finite") (("2" (propax) nil nil)) nil) ("3" (lemma "filter_first_first") (("3" (inst - "cseq!2" "nonempty?") (("3" (prop) (("1" (use "flatten_rest") (("1" (assert) (("1" (replace -2) (("1" (inst + "add(rest(first(cseq!2)), rest(filter(cseq!2, nonempty?)))") (("1" (assert) (("1" (expand "is_finite" +) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "some" "is_finite") (("2" (ground) nil nil)) nil) ("3" (expand "is_finite") (("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("4" (rewrite "flatten_first") (("4" (expand "is_finite") (("4" (ground) (("4" (rewrite "filter_first_first") (("4" (expand "some") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt 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_flatten nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (O const-decl "csequence" csequence_concatenate nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (flatten_reduce formula-decl nil csequence_flatten nil) (o_empty_left formula-decl nil csequence_concatenate nil) (empty_csequence nonempty-type-eq-decl nil csequence_props nil) (flatten_nonempty formula-decl nil csequence_flatten nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (o_nonempty formula-decl nil csequence_concatenate nil) (o_rest formula-decl nil csequence_concatenate nil) (flatten_rest2 formula-decl nil csequence_flatten nil) (o_first formula-decl nil csequence_concatenate nil) (pred type-eq-decl nil defined_types nil) (flatten_first formula-decl nil csequence_flatten nil) (filter_first_first formula-decl nil csequence_filter nil) (csequence_add_extensionality formula-decl nil csequence_codt nil) (some inductive-decl "boolean" csequence_codt nil) (is_finite_induction formula-decl nil csequence_props nil) (coinduction formula-decl nil csequence_codt nil) (filter const-decl "(LAMBDA (cseq1: csequence[T]): subsequence?(cseq1, cseq))" csequence_filter nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (flatten_rest formula-decl nil csequence_flatten nil) (flatten_empty formula-decl nil csequence_flatten nil) (every coinductive-decl "boolean" csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (bisimulation? adt-def-decl "boolean" csequence_codt nil) (infinite_csequence type-eq-decl nil csequence_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (o_infinite formula-decl nil csequence_concatenate nil)) shostak)) (flatten_rest_suffix_TCC1 0 (flatten_rest_suffix_TCC1-1 nil 3513685291 ("" (skosimp) (("" (rewrite "flatten_nonempty") nil nil)) nil) ((flatten_nonempty formula-decl nil csequence_flatten nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil)) nil)) (flatten_rest_suffix_TCC2 0 (flatten_rest_suffix_TCC2-1 nil 3513685291 ("" (skosimp*) (("" (expand "first_p") (("" (typepred "min(p_indexes(cseq!1, nonempty?))") (("" (expand "p_indexes" -2 1) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((first_p const-decl "indexes(cseq)" csequence_first_p nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt 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) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (pred type-eq-decl nil defined_types nil) (p_indexes const-decl "set[indexes(cseq)]" csequence_first_p nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil)) nil)) (flatten_rest_suffix 0 (flatten_rest_suffix-1 nil 3513686529 ("" (skosimp) (("" (use "flatten_rest") (("" (assert) (("" (rewrite "flatten_nonempty") (("" (rewrite "filter_first") (("" (use "filter_nonempty") (("" (use "filter_suffix") (("" (ground) (("" (case-replace "flatten(add(rest(nth(cseq!1, first_p(nonempty?, cseq!1))), rest(filter(cseq!1, (("" (hide -4 2) (("" (lemma "flatten_concatenate") (("" (inst-cp - "add(rest(nth(cseq!1, first_p(nonempty?, cseq!1))), suffix(cseq!1, 1 + first_p(n (("" (inst - "add(rest(nth(cseq!1, first_p(nonempty?, cseq!1))), rest(filter(cseq!1, nonempty (("" (assert) (("" (replace*) (("" (rewrite "flatten_filter") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((flatten_rest formula-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (flatten_nonempty formula-decl nil csequence_flatten nil) (filter_nonempty formula-decl nil csequence_filter nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (flatten_filter formula-decl nil csequence_flatten nil) (flatten_concatenate formula-decl nil csequence_flatten 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) (filter const-decl "(LAMBDA (cseq1: csequence[T]): subsequence?(cseq1, cseq))" csequence_filter nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (first_p const-decl "indexes(cseq)" csequence_first_p nil) (some inductive-decl "boolean" csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (nth def-decl "T" csequence_nth 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) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (= const-decl "[T, T -> boolean]" equalities nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (filter_suffix formula-decl nil csequence_filter nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (filter_first formula-decl nil csequence_filter nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (flatten_finite 0 (flatten_finite-1 nil 3513686997 ("" (skolem!) (("" (prop) (("1" (lemma "is_finite_induction[T]") (("1" (inst - "LAMBDA tseq: FORALL cseq: tseq = flatten(cseq) IMPLIES is_finite(filter(cseq, n (("1" (split) (("1" (inst - "flatten(cseq!1)") (("1" (assert) (("1" (inst - "cseq!1") nil nil)) nil)) nil) ("2" (delete -1 2) (("2" (skosimp*) (("2" (replace -2) (("2" (hide -2) (("2" (prop) (("1" (rewrite "flatten_empty") (("1" (rewrite "some_every_empty") (("1" (rewrite "filter_nonempty") (("1" (expand "is_finite") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (use "flatten_rest_suffix") (("2" (assert) (("2" (split) (("1" (inst - "add(rest(nth(cseq!3, first_p(nonempty?, cseq!3))), suffix(cseq!3, 1 + first_p(n (("1" (assert) (("1" (rewrite "filter_add") (("1" (lift-if) (("1" (ground) (("1" (expand "is_finite" -2) (("1" (lemma "filter_suffix") (("1" (inst - "cseq!3" "nonempty?") (("1" (expand "is_finite" +) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "filter_suffix") (("2" (inst - "cseq!3" "nonempty?") (("2" (expand "is_finite" +) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "flatten_nonempty") (("2" (rewrite "filter_nonempty") (("2" (expand "is_finite" +) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "every_coinduction[csequence[T]]") (("2" (inst - "is_finite" "LAMBDA cseq: is_finite(flatten(cseq))") (("2" (split) (("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil) ("2" (delete -1 2) (("2" (skosimp) (("2" (lift-if) (("2" (rewrite "flatten_concatenate") (("2" (ground) (("1" (use "o_infinite1[T]") nil nil) ("2" (use "o_infinite2[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "is_finite_induction[csequence[T]]") (("3" (inst - "LAMBDA (filt: csequence[csequence[T]]): FORALL cseq: filt = filter(cseq, nonemp (("3" (split) (("1" (inst - "filter(cseq!1, nonempty?)") (("1" (assert) (("1" (inst - "cseq!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (delete -1 -2 2) (("2" (skosimp*) (("2" (replace -2) (("2" (hide -2) (("2" (ground) (("1" (use "filter_nonempty") (("1" (use "some_every_empty") (("1" (use "flatten_empty") (("1" (expand "is_finite" +) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "some_every_empty" ("cseq" "cseq!3")) (("2" (prop) (("1" (use "flatten_empty") (("1" (expand "is_finite" +) (("1" (ground) nil nil)) nil)) nil) ("2" (use "filter_suffix") (("2" (use "filter_nonempty") (("2" (assert) (("2" (inst - "suffix(cseq!3, 1 + first_p(nonempty?, cseq!3))") (("2" (ground) (("1" (rewrite "suffix_every") (("1" (rewrite "nth_every" -5) (("1" (skosimp) (("1" (inst - "i!1") nil nil)) nil)) nil)) nil) ("2" (expand "is_finite" +) (("2" (flatten) (("2" (use "flatten_rest_suffix") (("2" (assert) (("2" (replace -1 +) (("2" (hide -1) (("2" (rewrite "flatten_concatenate" 3) (("2" (use "o_finite[T]") (("2" (rewrite "nth_every" -6) (("2" (inst - "first_p(nonempty?, cseq!3)") (("2" (expand "is_finite" -6) (("2" (assert) (("2" (expand "first_p") (("2" (typepred "min(p_indexes(cseq!3, nonempty?))") (("2" (expand "p_indexes" -2 1) (("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)) 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) (= const-decl "[T, T -> boolean]" equalities nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (is_finite inductive-decl "bool" csequence_props nil) (pred type-eq-decl nil defined_types nil) (subsequence? coinductive-decl "bool" csequence_subsequence nil) (filter const-decl "(LAMBDA (cseq1: csequence[T]): subsequence?(cseq1, cseq))" csequence_filter nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (some_every_empty formula-decl nil csequence_flatten nil) (filter_nonempty formula-decl nil csequence_filter nil) (flatten_empty formula-decl nil csequence_flatten nil) (flatten_nonempty formula-decl nil csequence_flatten nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt 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) (nth def-decl "T" csequence_nth nil) (PRED type-eq-decl nil defined_types nil) (some inductive-decl "boolean" csequence_codt nil) (first_p const-decl "indexes(cseq)" csequence_first_p 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) (filter_add formula-decl nil csequence_filter nil) (filter_suffix formula-decl nil csequence_filter nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (flatten_rest_suffix formula-decl nil csequence_flatten nil) (is_finite_induction formula-decl nil csequence_props nil) (T formal-type-decl nil csequence_flatten nil) (o_infinite1 judgement-tcc nil csequence_concatenate nil) (NOT const-decl "[bool -> bool]" booleans nil) (infinite_csequence type-eq-decl nil csequence_props nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (o_infinite2 judgement-tcc nil csequence_concatenate nil) (flatten_concatenate formula-decl nil csequence_flatten nil) (every_coinduction formula-decl nil csequence_codt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (every coinductive-decl "boolean" csequence_codt nil) (p_indexes const-decl "set[indexes(cseq)]" csequence_first_p nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (cseq!3 skolem-const-decl "csequence[csequence[T]]" csequence_flatten nil) (o_finite judgement-tcc nil csequence_concatenate nil) (suffix_every formula-decl nil csequence_suffix nil) (nth_every formula-decl nil csequence_nth nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil)) shostak)) (flatten_infinite 0 (flatten_infinite-1 nil 3513687550 ("" (skolem!) (("" (use "flatten_finite") (("" (rewrite "every_some_rew") (("" (expand "pred_NOT") (("" (ground) nil nil)) nil)) nil)) nil)) nil) ((flatten_finite formula-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (pred_NOT const-decl "bool" csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (every_some_rew formula-decl nil csequence_props nil)) shostak)) (length_of_flatten_TCC1 0 (length_of_flatten_TCC1-1 nil 3513685291 ("" (skolem-typepred) (("" (rewrite "flatten_finite") (("" (flatten) nil nil)) nil)) nil) ((flatten_finite formula-decl nil csequence_flatten nil) (finite_flatten_csequence type-eq-decl nil csequence_flatten nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (is_finite inductive-decl "bool" csequence_props nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_flatten nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (length_of_flatten_TCC2 0 (length_of_flatten_TCC2-1 nil 3513685291 ("" (skosimp) (("" (rewrite "flatten_empty") (("" (rewrite "some_every_empty") nil nil)) nil)) nil) ((flatten_empty formula-decl nil csequence_flatten nil) (T formal-type-decl nil csequence_flatten 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) (flatten const-decl "csequence[T]" csequence_flatten nil) (finite_flatten_csequence type-eq-decl nil csequence_flatten nil) (some_every_empty formula-decl nil csequence_flatten nil)) nil)) (length_of_flatten_TCC3 0 (length_of_flatten_TCC3-1 nil 3513685291 ("" (skosimp :preds? t) (("" (rewrite "flatten_finite") (("" (flatten) (("" (rewrite "nth_every") (("" (inst - "first_p(nonempty?, fseq!1)") nil nil)) nil)) nil)) nil)) nil) ((flatten_finite formula-decl nil csequence_flatten nil) (nth_every formula-decl nil csequence_nth nil) (pred type-eq-decl nil defined_types nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (first_p const-decl "indexes(cseq)" csequence_first_p nil) (some inductive-decl "boolean" csequence_codt nil) (PRED type-eq-decl nil defined_types 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) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (finite_flatten_csequence type-eq-decl nil csequence_flatten nil)) nil)) (length_of_flatten_TCC4 0 (length_of_flatten_TCC4-1 nil 3513685291 ("" (skosimp :preds? t) (("" (rewrite "flatten_finite") (("" (rewrite "flatten_finite") (("" (prop) (("1" (lemma "filter_suffix") (("1" (inst - "fseq!1" "nonempty?") (("1" (expand "is_finite" -2) (("1" (smash) (("1" (rewrite "flatten_empty") (("1" (use "filter_nonempty") (("1" (rewrite "some_every_empty") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "suffix_every") (("2" (rewrite "nth_every") (("2" (skosimp) (("2" (inst - "i!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((flatten_finite formula-decl nil csequence_flatten nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (filter_nonempty formula-decl nil csequence_filter nil) (some_every_empty formula-decl nil csequence_flatten nil) (flatten_empty formula-decl nil csequence_flatten nil) (filter_suffix formula-decl nil csequence_filter nil) (nth_every formula-decl nil csequence_nth nil) (suffix_every formula-decl nil csequence_suffix nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (first_p const-decl "indexes(cseq)" csequence_first_p nil) (indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth nil) (some inductive-decl "boolean" csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (pred type-eq-decl nil defined_types 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) (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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (finite_flatten_csequence type-eq-decl nil csequence_flatten nil)) nil)) (length_of_flatten_TCC5 0 (length_of_flatten_TCC5-1 nil 3513685291 ("" (skosimp :preds? t) (("" (lemma "filter_suffix") (("" (inst - "fseq!1" "nonempty?") (("" (split) (("1" (rewrite "flatten_empty") (("1" (use "filter_nonempty") (("1" (rewrite "some_every_empty") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "length" 2 2) (("2" (lift-if) (("2" (ground) (("2" (use "filter_nonempty") (("2" (rewrite "flatten_empty") (("2" (rewrite "some_every_empty") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((filter_suffix formula-decl nil csequence_filter nil) (filter_nonempty formula-decl nil csequence_filter nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (some_every_empty formula-decl nil csequence_flatten nil) (flatten_empty formula-decl nil csequence_flatten nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (pred type-eq-decl nil defined_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (is_finite inductive-decl "bool" csequence_props nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (finite_flatten_csequence type-eq-decl nil csequence_flatten nil)) nil)) (length_of_flatten_add_TCC1 0 (length_of_flatten_add_TCC1-1 nil 3513685291 ("" (skosimp) (("" (rewrite "flatten_concatenate" +) (("" (rewrite "o_finite") nil nil)) nil)) nil) ((flatten_concatenate formula-decl nil csequence_flatten nil) (T formal-type-decl nil csequence_flatten nil) (csequence type-decl nil csequence_codt nil) (boolean nonempty-type-decl nil booleans nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (bool nonempty-type-eq-decl nil booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (finite_flatten_csequence type-eq-decl nil csequence_flatten nil) (o_finite judgement-tcc nil csequence_concatenate nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil)) nil)) (length_of_flatten_add 0 (length_of_flatten_add-1 nil 3513687927 ("" (skosimp) (("" (expand "length_of_flatten" 1 1) (("" (lift-if) (("" (ground) (("1" (rewrite "flatten_concatenate" -) (("1" (rewrite "o_empty") (("1" (flatten) (("1" (expand* "length" "length_of_flatten") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "nth") (("2" (lift-if) (("2" (ground) (("1" (expand* "suffix" "suffix") nil nil) ("2" (use "first_p_rest") (("2" (assert) (("2" (expand "some") (("2" (ground) (("1" (expand "length" 2 2) (("1" (expand "length_of_flatten" 2 2) (("1" (lift-if) (("1" (lift-if) (("1" (lift-if) (("1" (ground) (("1" (rewrite "flatten_concatenate" 4) (("1" (rewrite "o_empty") nil nil)) nil) ("2" (expand "suffix" 2 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "flatten_concatenate" 5) (("2" (rewrite "o_empty") (("2" (rewrite "flatten_empty") (("2" (rewrite "some_every_empty") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((length_of_flatten def-decl "nat" csequence_flatten nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (o_empty formula-decl nil csequence_concatenate nil) (length def-decl "{n | has_length(fseq, n)}" csequence_length nil) (finite_flatten_csequence type-eq-decl nil csequence_flatten nil) (flatten const-decl "csequence[T]" csequence_flatten nil) (is_finite inductive-decl "bool" csequence_props nil) (bool nonempty-type-eq-decl nil booleans nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt 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_flatten nil) (flatten_concatenate formula-decl nil csequence_flatten nil) (first_p_rest formula-decl nil csequence_first_p nil) (pred type-eq-decl nil defined_types nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (some inductive-decl "boolean" csequence_codt nil) (flatten_empty formula-decl nil csequence_flatten nil) (some_every_empty formula-decl nil csequence_flatten nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (int_minus_int_is_int application-judgement "int" integers nil) (nth def-decl "T" csequence_nth nil)) shostak)) (flatten_length 0 --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.75 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 |
