Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ln_exp_series_alt.prf Sprache: Lisp

Original von: PVS^©

(commutative_groupoid
(commutative_groupoid_TCC1 0
  (commutative_groupoid_TCC1-1 nil 3294053873
   ("" (lemma "fullset_is_commutative_groupoid")
    (("" (propax) nil nil)) nil)
   ((fullset_is_commutative_groupoid formula-decl nil
     commutative_groupoid nil))
   shostak))
(commutative 0
  (commutative-1 nil 3294053895
   ("" (skosimp)
    (("" (lemma "fullset_is_commutative_groupoid")
      (("" (expand "commutative_groupoid?")
        (("" (flatten)
          (("" (expand "commutative?")
            (("" (inst - "x!1" "y!1")
              (("1" (expand "restrict") (("1" (propax) nil nil)) nil)
               ("2" (expand "fullset") (("2" (propax) nil nil)) nil)
               ("3" (expand "fullset") (("3" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((fullset_is_commutative_groupoid formula-decl nil
     commutative_groupoid nil)
    (x!1 skolem-const-decl "T" commutative_groupoid nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil commutative_groupoid nil)
    (y!1 skolem-const-decl "T" commutative_groupoid nil)
    (restrict const-decl "R" restrict nil)
    (commutative? const-decl "bool" operator_defs nil)
    (commutative_groupoid? const-decl "bool" groupoid_def nil))
   shostak))
(commutative_groupoid_is_groupoid 0
  (commutative_groupoid_is_groupoid-1 nil 3294053873
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "commutative_groupoid?") (("" (flatten) nil nil))
        nil))
      nil))
    nil)
   ((commutative_groupoid nonempty-type-eq-decl nil
     commutative_groupoid nil)
    (commutative_groupoid? const-decl "bool" groupoid_def nil)
    (* formal-const-decl "[T, T -> T]" commutative_groupoid nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil commutative_groupoid nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.