Consider the TRS R consisting of the rewrite rule

1: f(a,f(a,x)) -> f(a,f(f(a,a),f(a,x)))

There are 3 dependency pairs:

2: F(a,f(a,x)) -> F(a,f(f(a,a),f(a,x)))
3: F(a,f(a,x)) -> F(f(a,a),f(a,x))
4: F(a,f(a,x)) -> F(a,a)

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

- Consider the SCC {2,3}.
By taking the polynomial interpretation
[f](x,y) = 0,
[a] = 1
and [F](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
[a] = 2,
[f](x,y) = x - 1
and [F](x,y) = y,
we obtain a quasi-model of RR.
Furthermore, dependency pair 2
is strictly decreasing.


Hence the TRS is terminating.