Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_map_composition.prf Sprache: Lisp

Original von: PVS^©

(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)))

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.