Consider the TRS R consisting of the rewrite rules

1: rev1(0,nil) -> 0
2: rev1(s(X),nil) -> s(X)
3: rev1(X,cons(Y,L)) -> rev1(Y,L)
4: rev(nil) -> nil
5: rev(cons(X,L)) -> cons(rev1(X,L),rev2(X,L))
6: rev2(X,nil) -> nil
7: rev2(X,cons(Y,L)) -> rev(cons(X,rev(rev2(Y,L))))

There are 6 dependency pairs:

8: REV1(X,cons(Y,L)) -> REV1(Y,L)
9: REV(cons(X,L)) -> REV1(X,L)
10: REV(cons(X,L)) -> REV2(X,L)
11: REV2(X,cons(Y,L)) -> REV(cons(X,rev(rev2(Y,L))))
12: REV2(X,cons(Y,L)) -> REV(rev2(Y,L))
13: REV2(X,cons(Y,L)) -> REV2(Y,L)

The approximated dependency graph contains 2 SCCs:
{8}
and {10-13}.

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

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

Hence the TRS is terminating.