Consider the TRS R consisting of the rewrite rules

1: rev(nil) -> nil
2: rev(x . y) -> rev(y) ++ (x . nil)
3: car(x . y) -> x
4: cdr(x . y) -> y
5: null(nil) -> true
6: null(x . y) -> false
7: nil ++ y -> y
8: (x . y) ++ z -> x . (y ++ z)

There are 3 dependency pairs:

9: REV(x . y) -> rev(y) ++# (x . nil)
10: REV(x . y) -> REV(y)
11: (x . y) ++# z -> y ++# z

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

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

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

Hence the TRS is terminating.