Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: csequence_append.prf Sprache: Lisp

Original von: PVS^©

(csequence_append
(append_struct_TCC1 0
  (append_struct_TCC1-1 nil 3513600229 ("" (subtype-tcc) nil nil) nil
   nil))
(append_TCC1 0
  (append_TCC1-1 nil 3513600229
   ("" (expand* "append_struct" "coreduce") (("" (reduce) nil nil))
    nil)
   ((append_struct const-decl "csequence_struct" csequence_append 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))
   nil))
(append_finite 0
  (append_finite-1 nil 3513600229
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (skolem!) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
     ("2" (assert) nil nil) ("3" (assert) nil nil)
     ("4" (skosimp*)
      (("4" (expand "is_finite" +)
        (("4" (expand* "append" "append_struct")
          (("4" (expand "coreduce" +) (("4" (reduce) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((append_struct const-decl "csequence_struct" csequence_append 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)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_append nil)
    (append const-decl "nonempty_csequence" csequence_append nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (IMPLIES 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))
   nil))
(append_first_TCC1 0
  (append_first_TCC1-1 nil 3513600229 ("" (subtype-tcc) nil nil) nil
   nil))
(append_first 0
  (append_first-1 nil 3513600683
   ("" (expand* "append" "append_struct" "coreduce")
    (("" (reduce) nil nil)) nil)
   ((append const-decl "nonempty_csequence" csequence_append 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)
    (append_struct const-decl "csequence_struct" csequence_append nil))
   shostak))
(append_rest 0
  (append_rest-1 nil 3513600699
   ("" (skolem!)
    (("" (lemma "coinduction")
      ((""
        (inst -
         "LAMBDA (cseq1, cseq2: csequence): (empty?(cseq1) AND empty?(cseq2)) OR (EXISTS nseq: cseq1 = append(t!1, rest(nseq)) AND cseq2 = rest(append(t!1, nseq)))"
         "append(t!1, rest(nseq!1))" "rest(append(t!1, nseq!1))")
        (("1" (assert) (("1" (inst?) nil nil)) nil)
         ("2" (delete 2)
          (("2" (expand "bisimulation?")
            (("2" (skosimp* t)
              (("2" (smash)
                (("1" (grind) nil nil)
                 ("2" (skosimp)
                  (("2" (inst + "rest(nseq!2)")
                    (("1" (expand* "append" "append_struct" "coreduce")
                      (("1" (grind) nil nil)) nil)
                     ("2" (grind) nil nil))
                    nil))
                  nil)
                 ("3" (skosimp)
                  (("3" (inst + "rest(nseq!2)")
                    (("1" (expand* "append" "append_struct" "coreduce")
                      (("1" (grind) nil nil)) nil)
                     ("2" (grind) nil nil))
                    nil))
                  nil)
                 ("4" (grind) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_append nil)
    (coinduction formula-decl nil csequence_codt nil)
    (nseq!2 skolem-const-decl "nonempty_csequence[T]" csequence_append
     nil)
    (nseq!2 skolem-const-decl "nonempty_csequence[T]" csequence_append
     nil)
    (append_struct const-decl "csequence_struct" csequence_append 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (csequence type-decl nil 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)
    (bisimulation? adt-def-decl "boolean" csequence_codt nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (append const-decl "nonempty_csequence" csequence_append nil)
    (t!1 skolem-const-decl "T" csequence_append nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil))
   shostak))
(append_finite_def 0
  (append_finite_def-1 nil 3513600841
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (use "length_empty?_rew")
        (("3" (reduce)
          (("1"
            (expand* "insert" "append" "append_struct" "coreduce"
             "coreduce")
            (("1" (assert) nil nil)) nil)
           ("2" (decompose-equality 3)
            (("1" (rewrite "append_first")
              (("1" (rewrite "insert_first") nil nil)) nil)
             ("2" (rewrite "append_rest")
              (("2" (rewrite "insert_rest")
                (("2" (expand "length" 1) (("2" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((append_struct const-decl "csequence_struct" csequence_append 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)
    (append_rest formula-decl nil csequence_append nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (insert_rest formula-decl nil csequence_insert nil)
    (append_first formula-decl nil csequence_append nil)
    (insert_first formula-decl nil csequence_insert nil)
    (csequence_add_extensionality formula-decl nil csequence_codt nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_append nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (insert def-decl "nonempty_csequence" csequence_insert 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)
    (append const-decl "nonempty_csequence" csequence_append nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (IMPLIES 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))
   shostak))
(append_infinite_def 0
  (append_infinite_def-1 nil 3513601029
   ("" (skolem!)
    (("" (lemma "coinduction")
      ((""
        (inst -
         "LAMBDA (cseq1, cseq2: csequence): is_infinite(cseq2) AND cseq1 = append(t!1, cseq2)"
         "append(t!1, iseq!1)" "iseq!1")
        (("1" (assert) nil nil)
         ("2" (delete 2)
          (("2" (expand "bisimulation?")
            (("2" (skosimp)
              (("2" (expand "is_finite" 1)
                (("2" (grind :rewrites ("append_rest")) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil csequence_append nil)
    (coinduction formula-decl nil csequence_codt nil)
    (append_struct const-decl "csequence_struct" csequence_append 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)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (csequence type-decl nil 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)
    (bisimulation? adt-def-decl "boolean" csequence_codt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (append const-decl "nonempty_csequence" csequence_append nil)
    (t!1 skolem-const-decl "T" csequence_append nil))
   shostak))
(append_length 0
  (append_length-1 nil 3513601102
   ("" (induct "fseq" :name "is_finite_induction")
    (("1" (assert) nil nil) ("2" (assert) nil nil)
     ("3" (skosimp*)
      (("3" (expand "length" +)
        (("3" (reduce)
          (("1"
            (expand* "append" "append_struct" "coreduce" "coreduce"
             "length")
            nil nil)
           ("2"
            (expand* "append" "append_struct" "coreduce" "coreduce"
             "length")
            nil nil)
           ("3" (rewrite "append_rest") nil nil))
          nil))
        nil))
      nil)
     ("4" (skosimp*)
      (("4" (use "append_finite" ("fseq" "fseq!2")) nil nil)) nil))
    nil)
   ((append_finite judgement-tcc nil csequence_append nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers 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)
    (append_struct const-decl "csequence_struct" csequence_append nil)
    (append_rest formula-decl nil csequence_append nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (T formal-type-decl nil csequence_append nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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 "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)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers 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)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (append const-decl "nonempty_csequence" csequence_append nil))
   shostak))
(append_index 0
  (append_index-1 nil 3513601245
   ("" (induct "n")
    (("1" (skolem!)
      (("1" (use "length_empty?_rew")
        (("1" (expand "index?") (("1" (ground) nil nil)) nil)) nil))
      nil)
     ("2" (skosimp*)
      (("2" (case "empty?(cseq!1)")
        (("1" (hide -2)
          (("1" (use "length_empty?_rew")
            (("1"
              (expand* "append" "append_struct" "coreduce" "coreduce"
               "index?" "index?")
              (("1" (ground) nil nil)) nil))
            nil))
          nil)
         ("2" (assert)
          (("2" (inst - "t!1" "rest(cseq!1)")
            (("2" (auto-rewrite "index?_prop")
              (("2" (assert)
                (("2" (expand* "append" "append_struct")
                  (("2" (expand "coreduce" +)
                    (("2" (expand "is_finite" +)
                      (("2" (expand "length" +)
                        (("2" (reduce) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((index?_prop formula-decl nil csequence_nth nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (append_struct const-decl "csequence_struct" csequence_append nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt
     nil)
    (length_empty?_rew formula-decl nil csequence_length nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (append const-decl "nonempty_csequence" csequence_append nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (index? def-decl "bool" csequence_nth nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_append nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(append_nth_TCC1 0
  (append_nth_TCC1-1 nil 3513600229
   ("" (skolem!) (("" (rewrite "append_index") nil nil)) nil)
   ((append_index formula-decl nil csequence_append nil)
    (T formal-type-decl nil csequence_append 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)
    (indexes type-eq-decl nil csequence_nth nil))
   nil))
(append_nth 0
  (append_nth-1 nil 3513601432
   ("" (skolem-typepred)
    (("" (rewrite "index?_prop")
      (("" (split)
        (("1" (rewrite "append_finite_def")
          (("1" (use "insert_nth")
            (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil))
          nil)
         ("2" (rewrite "append_infinite_def") nil nil))
        nil))
      nil))
    nil)
   ((index?_prop formula-decl nil csequence_nth nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (append_infinite_def formula-decl nil csequence_append nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (append_finite_def formula-decl nil csequence_append nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (has_length def-decl "bool" csequence_props nil)
    (insert_nth formula-decl nil csequence_insert 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_append nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(append_add 0
  (append_add-1 nil 3513601483
   ("" (expand* "append" "append_struct" "coreduce")
    (("" (expand "coreduce" 1 2) (("" (propax) nil nil)) nil)) nil)
   ((append const-decl "nonempty_csequence" csequence_append 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)
    (append_struct const-decl "csequence_struct" csequence_append nil))
   shostak))
(append_last 0
  (append_last-1 nil 3513601569
   ("" (skolem + ("t!1" "_"))
    (("" (induct "fseq" :name "is_finite_induction")
      (("1" (assert) nil nil) ("2" (assert) nil nil)
       ("3" (skosimp)
        (("3" (ground)
          (("1"
            (expand* "append" "append_struct" "coreduce" "coreduce"
             "last" "length" "length" "nth")
            nil nil)
           ("2" (lemma "last_rest" ("nfseq" "append(t!1, cseq!1)"))
            (("2" (rewrite "append_rest") (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("4" (skosimp)
        (("4" (use "append_finite" ("fseq" "fseq!2")) nil nil)) nil))
      nil))
    nil)
   ((t!1 skolem-const-decl "T" csequence_append nil)
    (append const-decl "nonempty_csequence" csequence_append nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (is_finite inductive-decl "bool" csequence_props nil)
    (IMPLIES 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (nonempty_finite_csequence type-eq-decl nil csequence_props nil)
    (last const-decl "T" csequence_nth nil)
    (T formal-type-decl nil csequence_append nil)
    (is_finite_induction formula-decl nil csequence_props nil)
    (nth def-decl "T" csequence_nth nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length 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)
    (append_struct const-decl "csequence_struct" csequence_append nil)
    (append_rest formula-decl nil csequence_append nil)
    (last_rest formula-decl nil csequence_nth nil)
    (append_finite application-judgement "nonempty_finite_csequence"
     csequence_append nil)
    (append_finite judgement-tcc nil csequence_append nil))
   shostak))
(append_extensionality 0
  (append_extensionality-1 nil 3513601717
   ("" (skosimp)
    (("" (case "is_finite(cseq1!1) AND is_finite(cseq2!1)")
      (("1" (flatten)
        (("1" (assert)
          (("1" (rewrite "append_finite_def")
            (("1" (rewrite "append_finite_def")
              (("1" (lemma "append_length")
                (("1" (inst-cp - "t!1" "cseq2!1")
                  (("1" (inst - "t!1" "cseq1!1")
                    (("1" (assert)
                      (("1" (use "insert_extensionality")
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (split)
        (("1" (rewrite "append_infinite_def")
          (("1" (rewrite "append_infinite_def")
            (("1" (use "append_finite" ("fseq" "cseq2!1"))
              (("1" (assert) nil nil)) nil))
            nil))
          nil)
         ("2" (rewrite "append_infinite_def")
          (("1" (rewrite "append_infinite_def") nil nil)
           ("2" (use "append_finite" ("fseq" "cseq1!1"))
            (("2" (use "append_infinite_def") (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_finite inductive-decl "bool" csequence_props nil)
    (csequence type-decl nil csequence_codt nil)
    (T formal-type-decl nil csequence_append nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers 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)
    (has_length def-decl "bool" csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (insert_extensionality formula-decl nil csequence_insert nil)
    (append_length formula-decl nil csequence_append nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (append_finite_def formula-decl nil csequence_append nil)
    (append_infinite_def formula-decl nil csequence_append nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (append_finite judgement-tcc nil csequence_append nil))
   shostak))
(append_some 0
  (append_some-1 nil 3513601925
   ("" (skolem!)
    (("" (case "is_finite(cseq!1)")
      (("1" (rewrite "append_finite_def")
        (("1" (rewrite "insert_some") (("1" (prop) nil nil)) nil)) nil)
       ("2" (rewrite "append_infinite_def") (("2" (prop) nil nil))
        nil))
      nil))
    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_append nil)
    (insert_some formula-decl nil csequence_insert nil)
    (pred type-eq-decl nil defined_types 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)
    (has_length def-decl "bool" csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (append_finite_def formula-decl nil csequence_append nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (append_infinite_def formula-decl nil csequence_append nil))
   shostak))
(append_every 0
  (append_every-1 nil 3513602032
   ("" (skolem!)
    (("" (case "is_finite(cseq!1)")
      (("1" (rewrite "append_finite_def")
        (("1" (rewrite "insert_every") (("1" (prop) nil nil)) nil))
        nil)
       ("2" (rewrite "append_infinite_def") (("2" (prop) nil nil))
        nil))
      nil))
    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_append nil)
    (insert_every formula-decl nil csequence_insert nil)
    (pred type-eq-decl nil defined_types 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)
    (has_length def-decl "bool" csequence_props nil)
    (length def-decl "{n | has_length(fseq, n)}" csequence_length nil)
    (finite_csequence nonempty-type-eq-decl nil csequence_props nil)
    (append_finite_def formula-decl nil csequence_append nil)
    (infinite_csequence type-eq-decl nil csequence_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (append_infinite_def formula-decl nil csequence_append nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.