Quelle  monad_def.prf

(monad_def
 (monad?_TCC1 0
  (monad?_TCC1-1 nil 3301141427
   ("" (expand "member") (("" (skosimp) nil nil)) nil)
   ((member const-decl "bool" sets nil)) shostak))
 (monad?_TCC2 0
  (monad?_TCC2-1 nil 3301141427
   ("" (expand "groupoid?")
    (("" (expand "star_closed?")
      (("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil))
    nil)
   ((member const-decl "bool" sets nil)
    (star_closed? const-decl "bool" groupoid_def nil))
   shostak))
 (commutative_monad?_TCC1 0
  (commutative_monad?_TCC1-1 nil 3301141427
   ("" (expand "monad?")
    (("" (expand "groupoid?")
      (("" (expand "star_closed?")
        (("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil))
      nil))
    nil)
   ((star_closed? const-decl "bool" groupoid_def nil)
    (member const-decl "bool" sets nil)
    (monad? const-decl "bool" monad_def nil))
   shostak))
 (finite_commutative_monad?_TCC1 0
  (finite_commutative_monad?_TCC1-1 nil 3301141427
   ("" (expand "finite_monad?")
    (("" (expand "monad?")
      (("" (expand "groupoid?")
        (("" (expand "star_closed?")
          (("" (expand "member") (("" (skosimp*) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((monad? const-decl "bool" monad_def nil)
    (member const-decl "bool" sets nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (finite_monad? const-decl "bool" monad_def nil))
   shostak)))