0 QTRS
minus(X, 0) → X minus(s(X), s(Y)) → p(minus(X, Y)) p(s(X)) → X div(0, s(Y)) → 0 div(s(X), s(Y)) → s(div(minus(X, Y), s(Y)))