0 QTRS
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)))