Consider the TRS R consisting of the rewrite rules

1: p(m,n,s(r)) -> p(m,r,n)
2: p(m,s(n),0) -> p(0,n,m)
3: p(m,0,0) -> m

There are 2 dependency pairs:

4: P(m,n,s(r)) -> P(m,r,n)
5: P(m,s(n),0) -> P(0,n,m)

The approximated dependency graph contains one SCC:
{4,5}.

- Consider the SCC {4,5}.
There are no usable rules.
By taking the polynomial interpretation
[0] = 1,
[s](x) = x + 1
and [P](x,y,z) = x + y + z + 1,
the rules in {4,5}
are strictly decreasing.

Hence the TRS is terminating.