0 QTRS
pred(s(x)) → x minus(x, 0) → x minus(x, s(y)) → pred(minus(x, y)) quot(0, s(y)) → 0 quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))