(VAR x y ) (RULES plus(s(s(x)), y) -> s(plus(x, s(y))) plus(x, s(s(y))) -> s(plus(s(x), y)) plus(s(0), y) -> s(y) plus(0, y) -> y ack(0, y) -> s(y) ack(s(x), 0) -> ack(x, s(0)) ack(s(x), s(y)) -> ack(x, plus(y, ack(s(x), y))) )