Quelle  semigroup.prf

(semigroup
 (fullset_is_semigroup 0
  (fullset_is_semigroup-1 nil 3292838566 ("" (grind) nil nil) nil
   shostak))
 (semigroup_TCC1 0
  (semigroup_TCC1-1 nil 3292760730
   ("" (lemma "fullset_is_semigroup") (("" (propax) nil nil)) nil)
   ((fullset_is_semigroup formula-decl nil semigroup nil)) shostak))
 (associative 0
  (associative-1 nil 3294074066
   ("" (skosimp)
    (("" (lemma "fullset_is_semigroup")
      (("" (expand "semigroup?")
        (("" (flatten)
          (("" (expand "associative?") (("" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((fullset_is_semigroup formula-decl nil semigroup nil)
    (associative? const-decl "bool" operator_defs nil)
    (T formal-nonempty-type-decl nil semigroup nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (restrict const-decl "R" restrict nil)
    (fullset const-decl "set" sets nil))
   shostak)))