Consider the TRS R consisting of the rewrite rules

1: sum(cons(s(n),x),cons(m,y)) -> sum(cons(n,x),cons(s(m),y))
2: sum(cons(0,x),y) -> sum(x,y)
3: sum(nil,y) -> y
4: weight(cons(n,cons(m,x))) -> weight(sum(cons(n,cons(m,x)),cons(0,x)))
5: weight(cons(n,nil)) -> n

There are 4 dependency pairs:

6: SUM(cons(s(n),x),cons(m,y)) -> SUM(cons(n,x),cons(s(m),y))
7: SUM(cons(0,x),y) -> SUM(x,y)
8: WEIGHT(cons(n,cons(m,x))) -> WEIGHT(sum(cons(n,cons(m,x)),cons(0,x)))
9: WEIGHT(cons(n,cons(m,x))) -> SUM(cons(n,cons(m,x)),cons(0,x))

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

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

- Consider the SCC {6}.
By taking the polynomial interpretation
[s](x) = [SUM](x,y) = x + 1
and [cons](x,y) = x + y + 1,
rule 6
is strictly decreasing.


- Consider the SCC {8}.
The usable rules are {1-3}.
By taking the polynomial interpretation
[0] = 0,
[nil] = 1,
[s](x) = x,
[WEIGHT](x) = x + 1,
[cons](x,y) = x + y + 1
and [sum](x,y) = y,
the rules in {1-3}
are weakly decreasing and
rule 8
is strictly decreasing.

Hence the TRS is terminating.