Consider the TRS R consisting of the rewrite rule

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

There are 4 dependency pairs:

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

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

- Consider the SCC {2,3}.
By taking the polynomial interpretation
[a] = 2,
[F](x,y) = x
and [f](x,y) = x - 1,
we obtain a quasi-model of RR.
Furthermore, dependency pair 3
is weakly decreasing and
dependency pair 2
is strictly decreasing.
There is one new SCC.

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


Hence the TRS is terminating.