Consider the TRS R consisting of the rewrite rule

1: (x . y) . z -> x . (y . z)

There are 2 dependency pairs:

2: (x . y) .# z -> x .# (y . z)
3: (x . y) .# z -> y .# z

The approximated dependency graph contains one SCC:
{2,3}.

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

- Consider the SCC {2}.
By taking the polynomial interpretation
[.#](x,y) = x + 1
and [.](x,y) = x + y + 1,
rule 1
is weakly decreasing and
rule 2
is strictly decreasing.


Hence the TRS is terminating.