(VAR x y z)
(RULES
p(s(x)) -> x
s(p(x)) -> x
+(0,y) -> y
+(s(x),y) -> s(+(x,y))
+(p(x),y) -> p(+(x,y))
minus(0) -> 0
minus(s(x)) -> p(minus(x))
minus(p(x)) -> s(minus(x))
*(0,y) -> 0
*(s(x),y) -> +(*(x,y),y)
*(p(x),y) -> +(*(x,y),minus(y))
)
(COMMENT Example 4.14 in \cite{SK90})