Consider the TRS R consisting of the rewrite rules
1: a(b(x)) -> b(a(x))
2: a(c(x)) -> x
There is one dependency pair:
3: A(b(x)) -> A(x)
The approximated dependency graph contains one SCC:
{3}.
- Consider the SCC {3}.
There are no usable rules.
By taking the polynomial interpretation
[A](x) = [b](x) = x + 1,
rule 3
is strictly decreasing.
Hence the TRS is terminating.