0 QTRS
minus(0, Y) → 0 minus(s(X), s(Y)) → minus(X, Y) geq(X, 0) → true geq(0, s(Y)) → false geq(s(X), s(Y)) → geq(X, Y) div(0, s(Y)) → 0 div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0) if(true, X, Y) → X if(false, X, Y) → Y