Consider the TRS R consisting of the rewrite rules

1: minus(x,0) -> x
2: minus(s(x),s(y)) -> minus(x,y)
3: double(0) -> 0
4: double(s(x)) -> s(s(double(x)))
5: plus(0,y) -> y
6: plus(s(x),y) -> s(plus(x,y))
7: plus(s(x),y) -> plus(x,s(y))
8: plus(s(x),y) -> s(plus(minus(x,y),double(y)))

There are 7 dependency pairs:

9: MINUS(s(x),s(y)) -> MINUS(x,y)
10: DOUBLE(s(x)) -> DOUBLE(x)
11: PLUS(s(x),y) -> PLUS(x,y)
12: PLUS(s(x),y) -> PLUS(x,s(y))
13: PLUS(s(x),y) -> PLUS(minus(x,y),double(y))
14: PLUS(s(x),y) -> MINUS(x,y)
15: PLUS(s(x),y) -> DOUBLE(y)

The approximated dependency graph contains 3 SCCs:
{10},
{9}
and {11-13}.

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

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

- Consider the SCC {11-13}.
The usable rules are {1-4}.
By taking the polynomial interpretation
[0] = 1,
[double](x) = [PLUS](x,y) = 3x + 1
and [minus](x,y) = [s](x) = x + 3,
rule 13
is weakly decreasing and
the rules in {1-4,11,12}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {13}.
By taking the polynomial interpretation
[0] = 1,
[double](x) = [PLUS](x,y) = 3x + 1,
[minus](x,y) = x + 2
and [s](x) = x + 3,
the rules in {1-4,13}
are strictly decreasing.


Hence the TRS is terminating.