(VAR x y)
(RULES
  nats -> :(0,inc(nats))
  inc(:(x,y)) -> :(s(x),inc(y))
  hd(:(x,y)) -> x
  tl(:(x,y)) -> y
  inc(tl(nats)) -> tl(inc(nats))
)
(COMMENT Example 2 of \cite{GL06})