Consider the TRS R consisting of the rewrite rules

1: rev(nil) -> nil
2: rev(rev(x)) -> x
3: rev(x ++ y) -> rev(y) ++ rev(x)
4: nil ++ y -> y
5: x ++ nil -> x
6: (x . y) ++ z -> x . (y ++ z)
7: x ++ (y ++ z) -> (x ++ y) ++ z
8: make(x) -> x . nil

There are 6 dependency pairs:

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

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

- Consider the SCC {12-14}.
The usable rules are {4-7}.
By taking the polynomial interpretation
[nil] = 1
and [++](x,y) = [++#](x,y) = [.](x,y) = x + y + 1,
the rules in {6,7,13}
are weakly decreasing and
the rules in {4,5,12,14}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {13}.
By taking the polynomial interpretation
[nil] = 1,
[++](x,y) = [.](x,y) = x + y + 1
and [++#](x,y) = y + 1,
the rules in {6,7}
are weakly decreasing and
the rules in {4,5,13}
are strictly decreasing.


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

Hence the TRS is terminating.