Consider the TRS R consisting of the rewrite rules

1: x + 0 -> x
2: 0 + x -> x
3: s(x) + s(y) -> s(s(x + y))
4: x * 0 -> 0
5: 0 * x -> 0
6: s(x) * s(y) -> s((x * y) + (x + y))
7: sum(nil) -> 0
8: sum(cons(x,l)) -> x + sum(l)
9: prod(nil) -> s(0)
10: prod(cons(x,l)) -> x * prod(l)

There are 8 dependency pairs:

11: s(x) +# s(y) -> x +# y
12: s(x) *# s(y) -> (x * y) +# (x + y)
13: s(x) *# s(y) -> x *# y
14: s(x) *# s(y) -> x +# y
15: SUM(cons(x,l)) -> x +# sum(l)
16: SUM(cons(x,l)) -> SUM(l)
17: PROD(cons(x,l)) -> x *# prod(l)
18: PROD(cons(x,l)) -> PROD(l)

The approximated dependency graph contains 4 SCCs:
{11},
{13},
{18}
and {16}.

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

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

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

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

Hence the TRS is terminating.