0 QTRS
p(s(x)) → x fact(0) → s(0) fact(s(x)) → *(s(x), fact(p(s(x)))) *(0, y) → 0 *(s(x), y) → +(*(x, y), y) +(x, 0) → x +(x, s(y)) → s(+(x, y))