fmod COUNTER is
   sorts Counter .
   op reset : -> Counter .
   op inc : Counter -> Counter .
   op dec : Counter -> Counter .

   var N : Counter . 
   eq dec(inc(N)) = N .
   eq dec(reset) = reset .
endfm

*** Example usage
red dec(inc(reset)) == reset .