in nat.maude

fmod NAT-LIST-ASSOC is
   protecting NAT .

   sorts NeList List .
   subsorts Nat < NeList < List .

   op nil : -> List .
   op __ : List List -> List [assoc] .
   op __ : NeList NeList -> NeList [assoc] .

   op tail : NeList -> List .
   op head : NeList -> Nat .
   op length : List -> Nat .
   op reverse : List -> List .

   var N : Nat .
   var L : List .

   eq nil L = L .
   eq L nil = L .
   eq tail(N L) = L .
   eq head(N L) = N .
   eq length(nil) = 0 .
   eq length(N) = s(0) .
   eq length(N L) = s(0) + length(L) .
   eq reverse(nil) = nil .
   eq reverse(N) = N .
   eq reverse(N L) = reverse(L) N .
endfm

red reverse(0 s(0) s(s(0)) s(s(s(0))) s(s(s(s(0))))) .
***(
reduce in NAT-LIST-ASSOC : reverse(0 s(0) s(
    s(0)) s(s(s(0))) s(s(s(s(0))))) .
rewrites: 5 in -10ms cpu (0ms real) (~ rewrites/second)
result NeList: s(s(s(s(0)))) s(s(s(0))) s(s(0)) s(0) 0
)

red length(0 s(0) s(s(0)) s(s(s(0))) s(s(s(s(0))))) .
***(
reduce in NAT-LIST-ASSOC : length(0 s(0) s(s(0)) s(s(s(0)))
    s(s(s(s(0))))) .
rewrites: 13 in -10ms cpu (0ms real) (~ rewrites/second)
result NzNat: s(s(s(s(s(0)))))
)