(VAR x y)
(RULES
from(x)      -> :(x,from(x))
nat          -> from(0)
inc(:(x,y))  -> :(s(x),inc(y))
hd(:(x,y))   -> x
tl(:(x,y))   -> y
inc(tl(nat)) -> tl(inc(nat))
d(:(x,y))    -> :(x,:(x,d(y)))
)
(COMMENT 
Example 11 in Nao Hirokawa and Aart Middeldorp, Decreasing Diagrams and
Relative Termination, JAR.
)