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