(VAR x y)
(RULES
   s(p(x)) -> x
   p(s(x)) -> x
   +(x,0) -> x
   +(x,s(y)) -> s(+(x,y))
   +(x,p(y)) -> p(+(x,y))
   -(x,0) -> x
   -(x,s(y)) -> p(-(x,y))
   -(x,p(y)) -> s(-(x,y))
   *(x,0) -> 0
   *(x,s(y)) -> +(*(x,y),x)
   *(x,p(y)) -> -(*(x,y),x)
)
(COMMENT Example 7.1 of Becker, TAPSOFT 1993)