(VAR x y)
(RULES
nat          -> :(0,inc(nat))
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 3 in Nao Hirokawa and Aart Middeldorp, Decreasing Diagrams and
Relative Termination, JAR.
)