Consider the TRS R consisting of the rewrite rules

1: 0 - y -> 0
2: x - 0 -> x
3: x - s(y) -> if(greater(x,s(y)),s(x - p(s(y))),0)
4: p(0) -> 0
5: p(s(x)) -> x

There are 2 dependency pairs:

6: x -# s(y) -> x -# p(s(y))
7: x -# s(y) -> P(s(y))

The approximated dependency graph contains one SCC:
{6}.

- Consider the SCC {6}.
The usable rules are {4,5}.
By taking the polynomial interpretation
[0] = 0,
[s](x) = x + 1,
[p](x) = x - 1
and [-#](x,y) = y,
we obtain a quasi-model of the usable rules.
Furthermore, dependency pair 6
is strictly decreasing.

Hence the TRS is terminating.