Consider the TRS R consisting of the rewrite rules

1: app(nil,k) -> k
2: app(l,nil) -> l
3: app(cons(x,l),k) -> cons(x,app(l,k))
4: sum(cons(x,nil)) -> cons(x,nil)
5: sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
6: sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
7: plus(0,y) -> y
8: plus(s(x),y) -> s(plus(x,y))

There are 7 dependency pairs:

9: APP(cons(x,l),k) -> APP(l,k)
10: SUM(cons(x,cons(y,l))) -> SUM(cons(plus(x,y),l))
11: SUM(cons(x,cons(y,l))) -> PLUS(x,y)
12: SUM(app(l,cons(x,cons(y,k)))) -> SUM(app(l,sum(cons(x,cons(y,k)))))
13: SUM(app(l,cons(x,cons(y,k)))) -> APP(l,sum(cons(x,cons(y,k))))
14: SUM(app(l,cons(x,cons(y,k)))) -> SUM(cons(x,cons(y,k)))
15: PLUS(s(x),y) -> PLUS(x,y)

The approximated dependency graph contains 4 SCCs:
{9},
{15},
{10}
and {12}.

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

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

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

- Consider the SCC {12}.
By taking the polynomial interpretation
[nil] = 0,
[0] = [sum](x) = 1,
[s](x) = [SUM](x) = x + 1,
[app](x,y) = [plus](x,y) = x + y + 1
and [cons](x,y) = y + 1,
the rules in {3-6,8}
are weakly decreasing and
the rules in {1,2,7,12}
are strictly decreasing.

Hence the TRS is terminating.