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