0 QTRS
plus(0, Y) → Y plus(s(X), Y) → s(plus(X, Y)) min(X, 0) → X min(s(X), s(Y)) → min(X, Y) min(min(X, Y), Z) → min(X, plus(Y, Z)) quot(0, s(Y)) → 0 quot(s(X), s(Y)) → s(quot(min(X, Y), s(Y)))