Consider the TRS R consisting of the rewrite rules

1: rev(nil) -> nil
2: rev(cons(x,l)) -> cons(rev1(x,l),rev2(x,l))
3: rev1(0,nil) -> 0
4: rev1(s(x),nil) -> s(x)
5: rev1(x,cons(y,l)) -> rev1(y,l)
6: rev2(x,nil) -> nil
7: rev2(x,cons(y,l)) -> rev(cons(x,rev2(y,l)))

There are 5 dependency pairs:

8: REV(cons(x,l)) -> REV1(x,l)
9: REV(cons(x,l)) -> REV2(x,l)
10: REV1(x,cons(y,l)) -> REV1(y,l)
11: REV2(x,cons(y,l)) -> REV(cons(x,rev2(y,l)))
12: REV2(x,cons(y,l)) -> REV2(y,l)

The approximated dependency graph contains 2 SCCs:
{10}
and {9,11,12}.

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

- Consider the SCC {9,11,12}.
By taking the polynomial interpretation
[0] = [rev1](x,y) = [s](x) = 0,
[nil] = 1,
[rev](x) = x,
[REV](x) = x + 1,
[rev2](x,y) = x + y
and [cons](x,y) = [REV2](x,y) = x + y + 1,
the rules in {1-7,11}
are weakly decreasing and
the rules in {9,12}
are strictly decreasing.

Hence the TRS is terminating.