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))
9: sum(plus(cons(0,x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
10: pred(cons(s(x),nil)) -> cons(x,nil)

There are 9 dependency pairs:

11: APP(cons(x,l),k) -> APP(l,k)
12: SUM(cons(x,cons(y,l))) -> SUM(cons(plus(x,y),l))
13: SUM(cons(x,cons(y,l))) -> PLUS(x,y)
14: SUM(app(l,cons(x,cons(y,k)))) -> SUM(app(l,sum(cons(x,cons(y,k)))))
15: SUM(app(l,cons(x,cons(y,k)))) -> APP(l,sum(cons(x,cons(y,k))))
16: SUM(app(l,cons(x,cons(y,k)))) -> SUM(cons(x,cons(y,k)))
17: PLUS(s(x),y) -> PLUS(x,y)
18: SUM(plus(cons(0,x),cons(y,l))) -> PRED(sum(cons(s(x),cons(y,l))))
19: SUM(plus(cons(0,x),cons(y,l))) -> SUM(cons(s(x),cons(y,l)))

The approximated dependency graph contains 4 SCCs:
{11},
{17},
{12}
and {14}.

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

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

- Consider the SCC {12}.
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,12}
are strictly decreasing.

- Consider the SCC {14}.
By taking the polynomial interpretation
[nil] = 0,
[0] = [pred](x) = [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-10}
are weakly decreasing and
the rules in {1,2,7,14}
are strictly decreasing.

Hence the TRS is terminating.