Quelle csequence_map_composition.prf Sprache: Lisp

(csequence_map_composition
(map_composition 0
  (map_composition-1 nil 3513552853
   ("" (skolem!)
    (("" (lemma "coinduction[T3]")
      ((""
        (inst -
         "LAMBDA (cseq1, cseq2: csequence[T3]): EXISTS (cseq: csequence[T1]): map[T2, T3](f23!1)(map[T1, T2](f12!1)(cseq)) = cseq1 AND map[T1, T3](f23!1 o f12!1)(cseq) = cseq2"
         "map[T2, T3](f23!1)(map[T1, T2](f12!1)(cseq!1))"
         "map[T1, T3](f23!1 o f12!1)(cseq!1)")
        (("1" (assert) (("1" (inst + "cseq!1") nil nil)) nil)
         ("2" (delete 2)
          (("2" (expand "bisimulation?")
            (("2" (skosimp*)
              (("2" (expand "map" -)
                (("2" (expand "o")
                  (("2" (smash)
                    (("1" (inst + "rest(cseq!2)")
                      (("1" (decompose-equality)
                        (("1" (decompose-equality -3)
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil)
                     ("2" (decompose-equality)
                      (("2" (decompose-equality -3)
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T3 formal-type-decl nil csequence_map_composition nil)
    (coinduction formula-decl nil csequence_codt nil)
    (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt
          nil)
    (nonempty? adt-recognizer-decl "[csequence -> boolean]"
               csequence_codt nil)
    (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil)
    (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]"
     csequence_codt 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)
    (T1 formal-type-decl nil csequence_map_composition nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T2 formal-type-decl nil csequence_map_composition nil)
    (map adt-def-decl "csequence[T1]" csequence_codt_map nil)
    (f23!1 skolem-const-decl "[T2 -> T3]" csequence_map_composition
     nil)
    (f12!1 skolem-const-decl "[T1 -> T2]" csequence_map_composition
     nil)
    (O const-decl "T3" function_props nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.20 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.