(VAR x y)
(RULES
double(0) -> 0
double(s(x)) -> s(s(double(x)))
+(x,0) -> x
+(x,s(y)) -> s(+(x,y))
+(s(x),y) -> s(+(x,y))
double(x) -> +(x,x)
)
(COMMENT Example 2.13 in \cite{SK90})