*** The following is the specification of (small) categories

fmod CATEG is
  sorts Object Arrow .
  subsort Object < Arrow .
  ops s t : Arrow -> Object .
  op _;_ : Arrow Arrow -> [Arrow] .
  var O : Object .  vars A A' A'' : Arrow .
  eq s(O) = O .
  eq t(O) = O .
 ceq O ; A = A if s(A) = O .
 ceq A ; O = A if t(A) = O .
 cmb A ; A' : Arrow if t(A) = s(A') .
 ceq t(A) = s(A') if A ; A' : Arrow .
 ceq s(A ; A') = s(A)  if t(A) = s(A') .
 ceq t(A ; A') = t(A') if t(A) = s(A') .
 ceq (A ; A') ; A'' = A ; (A' ; A'') if t(A) = s(A') /\ t(A') = s(A'') .
endfm

*** The following is its envelope

fmod ENV-CATEG is
  sorts Object Arrow .
  subsort Object < Arrow .
  ops s t : Arrow -> Object .
  op _;_ : Arrow Arrow -> [Arrow] .
  var O : Object .  vars A A' A'' : Arrow .
  eq s(O) = O .
  mb s(O) : Arrow .
  eq t(O) = O .
  mb t(O) : Arrow .
 ceq O ; A = A     if s(A) = O /\ s(A) : Arrow .
 cmb O ; A : Arrow if s(A) = O /\ s(A) : Arrow .
 ceq A ; O = A if t(A) = O /\ t(A) : Arrow .
 cmb A ; O : Arrow if t(A) = O /\ t(A) : Arrow .
 cmb A ; A' : Arrow if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow .
 ceq t(A) = s(A')  if A ; A' : Arrow .
 cmb t(A)  : Arrow if A ; A' : Arrow .
 cmb s(A') : Arrow if A ; A' : Arrow .
 ceq s(A ; A') = s(A)  if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow .
 cmb s(A ; A') : Arrow if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow .
 cmb s(A) : Arrow      if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow .
 ceq t(A ; A') = t(A') if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow .
 cmb t(A ; A') : Arrow if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow .
 cmb t(A') : Arrow     if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow .
 ceq (A ; A') ; A'' = A ; (A' ; A'')
    if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow
    /\ t(A') = s(A'') /\ t(A') : Arrow /\ s(A'') : Arrow .
 cmb (A ; A') ; A'' : Arrow
    if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow
    /\ t(A') = s(A'') /\ t(A') : Arrow /\ s(A'') : Arrow .
 cmb A ; (A' ; A'') : Arrow
    if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow
    /\ t(A') = s(A'') /\ t(A') : Arrow /\ s(A'') : Arrow .
 cmb A ; A' : Arrow
    if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow
    /\ t(A') = s(A'') /\ t(A') : Arrow /\ s(A'') : Arrow .
 cmb A' ; A'' : Arrow
    if t(A) = s(A') /\ t(A) : Arrow /\ s(A') : Arrow
    /\ t(A') = s(A'') /\ t(A') : Arrow /\ s(A'') : Arrow .
endfm


*** We next show that CATEG => ENV-CATEG
*** By the theorems of constants and of implication we add the
*** following module, which can be generated automatically.

fmod CATEG-CONST is
  pr CATEG .
  op o : -> Object .
  ops a1 a2 a3 a4 a5 a6 a7 : -> Arrow .
  eq s(a1) = o .
  mb s(a1) : Arrow .
  eq t(a2) = o .
  mb t(a2) : Arrow .
  eq t(a3) = s(a4) .
  mb t(a3) : Arrow .
  mb s(a4) : Arrow .
  mb a5 ; a6 : Arrow .
  eq t(a4) = s(a7) .
  mb t(a4) : Arrow .
  mb s(a7) : Arrow .
endfm

red s(o) == o .
red s(o) :: Arrow .
red t(o) == o .
red t(o) :: Arrow .
red o ; a1 == a1 .
red o ; a1 :: Arrow .
red a2 ; o == a2 .
red a2 ; o :: Arrow .
red a3 ; a4 :: Arrow .
red t(a5) == s(a6) .
red t(a5) :: Arrow .
red s(a6) :: Arrow .
red s(a3 ; a4) == s(a3) .
red s(a3 ; a4) :: Arrow .
red s(a3) :: Arrow .
red t(a3 ; a4) == t(a4) .
red t(a3 ; a4) :: Arrow .
red t(a4) :: Arrow .
red (a3 ; a4) ; a7 == a3 ; (a4 ; a7) .
red (a3 ; a4) ; a7 :: Arrow .
red a3 ; (a4 ; a7) :: Arrow .
red a3 ; a4 :: Arrow .
red a4 ; a7 :: Arrow .

*** All the reductions above but the 10th return true.
*** The tenth returns false because the 6th axiom in CATEG
*** cannot be compiled by Maude (because A' doesn't appear in the left
*** hand side term).

*** We next show that ENV-CATEG => CATEG
*** By the theorems of constants and of implication we add the
*** following module, which can also be generated automatically.

fmod ENV-CATEG-CONST is
  pr ENV-CATEG .
  op o : -> Object .
  ops a1 a2 a3 a4 a5 a6 a7 : -> Arrow .
  eq s(a1) = o .
  eq t(a2) = o .
  eq t(a3) = s(a4) .
  mb a5 ; a6 : Arrow .
  eq t(a4) = s(a7) .
endfm

red s(o) == o .
red t(o) == o .
red o ; a1 == a1 .
red a2 ; o == a2 .
red a3 ; a4 :: Arrow .
red t(a5) == s(a6) .
red s(a3 ; a4) == s(a3) .
red t(a3 ; a4) == t(a4) .
red (a3 ; a4) ; a7 == a3 ; (a4 ; a7) .

*** The reduction above are also true, with the same exception as above

*** Therefore, CATEG <=> ENV-CATEG
*** See http://ase.arc.nasa.gov/grosu/download/categ.html
*** for a different approach and more comments.