Consider the TRS R consisting of the rewrite rules

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

There are 17 dependency pairs:

15: 0(x) +# 0(y) -> 0#(x + y)
16: 0(x) +# 0(y) -> x +# y
17: 0(x) +# 1(y) -> x +# y
18: 1(x) +# 0(y) -> x +# y
19: 1(x) +# 1(y) -> 0#((x + y) + 1(#))
20: 1(x) +# 1(y) -> (x + y) +# 1(#)
21: 1(x) +# 1(y) -> x +# y
22: 0(x) *# y -> 0#(x * y)
23: 0(x) *# y -> x *# y
24: 1(x) *# y -> 0(x * y) +# y
25: 1(x) *# y -> 0#(x * y)
26: 1(x) *# y -> x *# y
27: SUM(nil) -> 0#(#)
28: SUM(cons(x,l)) -> x +# sum(l)
29: SUM(cons(x,l)) -> SUM(l)
30: PROD(cons(x,l)) -> x *# prod(l)
31: PROD(cons(x,l)) -> PROD(l)

The approximated dependency graph contains 4 SCCs:
{16-18,20,21},
{23,26},
{31}
and {29}.

- Consider the SCC {16-18,20,21}.
The usable rules are {1-7}.
By taking the polynomial interpretation
[#] = 0,
[0](x) = x,
[1](x) = x + 1
and [+](x,y) = [+#](x,y) = x + y + 1,
the rules in {1,4-7,16,20}
are weakly decreasing and
the rules in {2,3,17,18,21}
are strictly decreasing.
There are 2 new SCCs.

- Consider the SCC {20}.
By taking the polynomial interpretation
[#] = 0,
[0](x) = [1](x) = x + 1,
[+](x,y) = x + y
and [+#](x,y) = x + y + 1,
the rules in {2,3,7}
are weakly decreasing and
the rules in {1,4-6,20}
are strictly decreasing.

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


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

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

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

Hence the TRS is terminating.