0 QTRS
plus(x, 0) → x plus(x, s(y)) → s(plus(x, y)) times(0, y) → 0 times(x, 0) → 0 times(s(x), y) → plus(times(x, y), y) p(s(s(x))) → s(p(s(x))) p(s(0)) → 0 fac(s(x)) → times(fac(p(s(x))), s(x))