Consider the TRS R consisting of the rewrite rules

1: p(0) -> 0
2: p(s(x)) -> x
3: le(0,y) -> true
4: le(s(x),0) -> false
5: le(s(x),s(y)) -> le(x,y)
6: minus(x,0) -> x
7: minus(x,s(y)) -> if(le(x,s(y)),0,p(minus(x,p(s(y)))))
8: if(true,x,y) -> x
9: if(false,x,y) -> y

There are 6 dependency pairs:

10: LE(s(x),s(y)) -> LE(x,y)
11: MINUS(x,s(y)) -> IF(le(x,s(y)),0,p(minus(x,p(s(y)))))
12: MINUS(x,s(y)) -> LE(x,s(y))
13: MINUS(x,s(y)) -> P(minus(x,p(s(y))))
14: MINUS(x,s(y)) -> MINUS(x,p(s(y)))
15: MINUS(x,s(y)) -> P(s(y))

The approximated dependency graph contains 2 SCCs:
{10}
and {14}.

- Consider the SCC {10}.
There are no usable rules.
By taking the polynomial interpretation
[s](x) = x + 1
and [LE](x,y) = x + y + 1,
rule 10
is strictly decreasing.

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

Hence the TRS is terminating.