Consider the TRS R consisting of the rewrite rules

1: nil ++ y -> y
2: x ++ nil -> x
3: (x . y) ++ z -> x . (y ++ z)
4: (x ++ y) ++ z -> x ++ (y ++ z)

There are 3 dependency pairs:

5: (x . y) ++# z -> y ++# z
6: (x ++ y) ++# z -> x ++# (y ++ z)
7: (x ++ y) ++# z -> y ++# z

The approximated dependency graph contains one SCC:
{5-7}.

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

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


Hence the TRS is terminating.