0 QTRS
minus(x, 0) → x minus(s(x), s(y)) → minus(x, y) le(0, y) → true le(s(x), 0) → false le(s(x), s(y)) → le(x, y) quot(0, s(y)) → 0 quot(s(x), s(y)) → s(quot(minus(s(x), s(y)), s(y)))