Consider the TRS R consisting of the rewrite rules

1: sum(0) -> 0
2: sum(s(x)) -> sum(x) + s(x)
3: sum1(0) -> 0
4: sum1(s(x)) -> s(sum1(x) + (x + x))

There are 2 dependency pairs:

5: SUM(s(x)) -> SUM(x)
6: SUM1(s(x)) -> SUM1(x)

The approximated dependency graph contains 2 SCCs:
{5}
and {6}.

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

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

Hence the TRS is terminating.