Consider the TRS R consisting of the rewrite rule

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

There are 4 dependency pairs:

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

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

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

- Consider the SCC {2,3}.
By taking the polynomial interpretation
[a] = 1,
[h](x) = x + 1
and [f](x,y) = [F](x,y) = 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
[h](x) = 0,
[a] = 2,
[f](x,y) = x + 2y - 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.