(VAR x y)
(RULES
  nats -> :(0,inc(nats))
  inc(:(x,y)) -> :(s(x),inc(y))
  inc(tl(nats)) -> tl(inc(nats))
  hd(:(x,y)) -> x
  tl(:(x,y)) -> y
  d(:(x,y)) -> :(x,:(x,d(y)))
)
(COMMENT
doi:10.1007/s10817-011-9238-x
[33] Example 3
)