Quelle csequence_zip_unzip.prf Sprache: Lisp

(csequence_zip_unzip
(zip_unzip_eta 0
  (zip_unzip_eta-1 nil 3513781677
   ("" (skolem!)
    (("" (lemma "coinduction[[T1, T2]]")
      ((""
        (inst -
         "LAMBDA (cseq1, cseq2: csequence[[T1, T2]]): cseq1 = zip(unzip(cseq2))"
         "zip(unzip(cseq!1))" "cseq!1")
        (("" (delete 2)
          (("" (expand "bisimulation?")
            (("" (skosimp)
              (("" (replace -1)
                (("" (hide -1)
                  (("" (smash)
                    (("1" (use "unzip_nonempty")
                      (("1" (flatten)
                        (("1" (use "zip_nonempty")
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("2"
                      (expand* "unzip" "unzip_left_struct"
                       "unzip_right_struct" "coreduce" "zip"
                       "zip_struct" "coreduce")
                      nil nil)
                     ("3" (use "unzip_nonempty")
                      (("3" (flatten)
                        (("3" (lemma "zip_rest")
                          (("3" (inst - "unzip(y!1)`1" "unzip(y!1)`2")
                            (("3" (lemma "unzip_rest_left")
                              (("3"
                                (inst - "y!1")
                                (("3"
                                  (lemma "unzip_rest_right")
                                  (("3"
                                    (inst - "y!1")
                                    (("3" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("4"
                      (expand* "unzip" "unzip_left_struct"
                       "unzip_right_struct" "coreduce" "zip"
                       "zip_struct" "coreduce")
                      (("4" (smash) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil csequence_zip_unzip nil)
    (T1 formal-type-decl nil csequence_zip_unzip nil)
    (coinduction formula-decl nil csequence_codt nil)
    (zip_rest formula-decl nil csequence_zip nil)
    (unzip_rest_left formula-decl nil csequence_unzip nil)
    (unzip_rest_right formula-decl nil csequence_unzip nil)
    (unzip_left_struct const-decl
     "csequence_struct[T1, csequence[[T1, T2]]]" csequence_unzip nil)
    (unzip_right_struct const-decl
     "csequence_struct[T2, csequence[[T1, T2]]]" csequence_unzip 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)
    (zip_struct const-decl
     "csequence_struct[[T1, T2], [csequence[T1], csequence[T2]]]"
     csequence_zip nil)
    (unzip_nonempty judgement-tcc nil csequence_unzip nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (zip_nonempty judgement-tcc nil csequence_zip nil)
    (y!1 skolem-const-decl "csequence[[T1, T2]]" csequence_zip_unzip
     nil)
    (unzip const-decl "[csequence[T1], csequence[T2]]" csequence_unzip
     nil)
    (zip const-decl "csequence[[T1, T2]]" csequence_zip nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bisimulation? adt-def-decl "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)
    (csequence type-decl nil csequence_codt nil))
   shostak))
(unzip_zip_eta 0
  (unzip_zip_eta-1 nil 3513784473
   ("" (skosimp)
    (("" (decompose-equality)
      (("1" (lemma "coinduction[T1]")
        (("1"
          (inst -
           "LAMBDA (cseq1, cseq2: csequence[T1]): EXISTS (cseq: csequence[T2]):
cseq1 = unzip(zip(cseq2, cseq))`1 AND length_eq(cseq2, cseq)"
           "unzip(zip(cseq1!1, cseq2!1))`1" "cseq1!1")
          (("1" (assert) (("1" (inst + "cseq2!1") nil nil)) nil)
           ("2" (delete -1 2)
            (("2" (expand "bisimulation?")
              (("2" (skosimp*)
                (("2" (replace -1)
                  (("2" (hide -1)
                    (("2" (smash)
                      (("1" (rewrite "unzip_empty_left")
                        (("1" (rewrite "zip_empty")
                          (("1" (use "length_eq_empty")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (use "unzip_empty_left")
                        (("2" (assert)
                          (("2" (rewrite "zip_empty") nil nil)) nil))
                        nil)
                       ("3" (use "unzip_empty_left")
                        (("3" (assert)
                          (("3" (rewrite "zip_empty")
                            (("3" (ground)
                              (("3"
                                (inst + "rest(cseq!1)")
                                (("3"
                                  (use "length_eq_rest")
                                  (("3"
                                    (assert)
                                    (("3"
                                      (rewrite "unzip_rest_left")
                                      (("3"
                                        (rewrite "zip_rest")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("4" (use "unzip_empty_left")
                        (("4" (assert)
                          (("4" (rewrite "zip_empty")
                            (("4" (ground)
                              (("4"
                                (rewrite "unzip_first_left")
                                (("4"
                                  (rewrite "zip_first")
                                  (("4" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "coinduction[T2]")
        (("2"
          (inst -
           "LAMBDA (cseq1, cseq2: csequence[T2]): EXISTS (cseq: csequence[T1]): cseq1 = unzip(zip(cseq, cseq2))`2 AND length_eq(cseq, cseq2)"
           "unzip(zip(cseq1!1, cseq2!1))`2" "cseq2!1")
          (("1" (assert) (("1" (inst + "cseq1!1") nil nil)) nil)
           ("2" (delete -1 2)
            (("2" (expand "bisimulation?")
              (("2" (skosimp*)
                (("2" (replace -1)
                  (("2" (hide -1)
                    (("2" (smash)
                      (("1" (rewrite "unzip_empty_right")
                        (("1" (rewrite "zip_empty")
                          (("1" (use "length_eq_empty")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (use "unzip_empty_right")
                        (("2" (assert)
                          (("2" (rewrite "zip_empty") nil nil)) nil))
                        nil)
                       ("3" (use "unzip_empty_right")
                        (("3" (assert)
                          (("3" (rewrite "zip_empty")
                            (("3" (ground)
                              (("3"
                                (inst + "rest(cseq!1)")
                                (("3"
                                  (use "length_eq_rest")
                                  (("3"
                                    (assert)
                                    (("3"
                                      (rewrite "unzip_rest_right")
                                      (("3"
                                        (rewrite "zip_rest")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("4" (use "unzip_empty_right")
                        (("4" (assert)
                          (("4" (rewrite "zip_empty")
                            (("4" (ground)
                              (("4"
                                (rewrite "unzip_first_right")
                                (("4"
                                  (rewrite "zip_first")
                                  (("4" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((unzip const-decl "[csequence[T1], csequence[T2]]" csequence_unzip
     nil)
    (zip const-decl "csequence[[T1, T2]]" csequence_zip nil)
    (T2 formal-type-decl nil csequence_zip_unzip nil)
    (csequence type-decl nil csequence_codt nil)
    (T1 formal-type-decl nil csequence_zip_unzip nil)
    (length_eq const-decl "bool" csequence_length_comp nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bisimulation? adt-def-decl "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)
    (zip_empty formula-decl nil csequence_zip nil)
    (length_eq_empty formula-decl nil csequence_length_comp nil)
    (unzip_empty_left formula-decl nil csequence_unzip nil)
    (length_eq_rest formula-decl nil csequence_length_comp nil)
    (nonempty_csequence type-eq-decl nil csequence_props nil)
    (unzip_rest_left formula-decl nil csequence_unzip nil)
    (zip_rest formula-decl nil csequence_zip nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (zip_first formula-decl nil csequence_zip nil)
    (unzip_first_left formula-decl nil csequence_unzip nil)
    (coinduction formula-decl nil csequence_codt nil)
    (unzip_empty_right formula-decl nil csequence_unzip nil)
    (unzip_rest_right formula-decl nil csequence_unzip nil)
    (unzip_first_right formula-decl nil csequence_unzip nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.