Quelle commutative_groupoid.prf Sprache: Lisp

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

quality100%

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