TRS: { p(m, n, s(r)) -> p(m, r, n), p(m, s(n), 0()) -> p(0(), n, m), p(m, 0(), 0()) -> m} POP*: Quasi-Precedence: empty Normal: pi(p) = [1,2,3] Safe: pi(s) = [1] Predicative System: { p(m,n,s(;r);) -> p(m,r,n;), p(m,s(;n),0();) -> p(0(),n,m;), p(m,0(),0();) -> m} Qed