Consider the TRS R consisting of the rewrite rules
1: g(a) -> g(b)
2: b -> f(a,a)
3: f(a,a) -> g(d)
There are 4 dependency pairs:
4: G(a) -> G(b)
5: G(a) -> B
6: B -> F(a,a)
7: F(a,a) -> G(d)
The approximated dependency graph contains one SCC:
{4}.
- Consider the SCC {4}.
By taking the polynomial interpretation
[b] = [f](x,y) = [g](x) = 0,
[a] = [d] = 1
and [G](x) = x + 1,
the rules in {1-3}
are weakly decreasing and
rule 4
is strictly decreasing.
Hence the TRS is terminating.