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