(VAR x y)
(RULES
 -(x, 0) -> x
 -(s(x), s(y)) -> -(x, y) 
 +(0, y) -> y
 +(s(x), y) -> s(+(x, y))
 *(x, 0) -> 0
 *(x, s(y)) -> +(x, *(x, y))
 p(s(x)) -> x
 f(s(x)) -> f(-(p(*(s(x), s(x))), *(s(x), s(x))))
)