in nat.maude

fmod NAT-LIST-ASSOC-ID is
  protecting NAT .  
   
  sorts NeList List .
  subsorts Nat < NeList < List .

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

  op tail : NeList -> List .
  op head : NeList -> Nat .
  op length : List -> Nat .
  op reverse : List -> List .
   
  var N : Nat .
  var L : List .
  
  eq tail(N L) = L .
  eq head(N L) = N .
  eq length(nil) = 0 .
  eq length(N L) = s(0) + length(L) .
  eq reverse(nil) = nil .
  eq reverse(N L) = reverse(L) N .
endfm