Consider the TRS R consisting of the rewrite rules

1: f(a,y) -> f(y,g(y))
2: g(a) -> b
3: g(b) -> b

There are 2 dependency pairs:

4: F(a,y) -> F(y,g(y))
5: F(a,y) -> G(y)

The approximated dependency graph contains one SCC:
{4}.

- Consider the SCC {4}.
The usable rules are {2,3}.
By taking the polynomial interpretation
[b] = [g](x) = 0,
[a] = 1
and [F](x,y) = x + y + 1,
the rules in {2,3}
are weakly decreasing and
rule 4
is strictly decreasing.

Hence the TRS is terminating.