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