Consider the TRS R consisting of the rewrite rules

1: double(0) -> 0
2: double(s(x)) -> s(s(double(x)))
3: x + 0 -> x
4: x + s(y) -> s(x + y)
5: s(x) + y -> s(x + y)
6: double(x) -> x + x

There are 4 dependency pairs:

7: DOUBLE(s(x)) -> DOUBLE(x)
8: x +# s(y) -> x +# y
9: s(x) +# y -> x +# y
10: DOUBLE(x) -> x +# x

The approximated dependency graph contains 2 SCCs:
{8,9}
and {7}.

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

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

Hence the TRS is terminating.