Consider the TRS R consisting of the rewrite rules
1: f(a) -> f(c(a))
2: f(c(X)) -> X
3: f(c(a)) -> f(d(b))
4: f(a) -> f(d(a))
5: f(d(X)) -> X
6: f(c(b)) -> f(d(a))
7: e(g(X)) -> e(X)
There are 5 dependency pairs:
8: F(a) -> F(c(a))
9: F(c(a)) -> F(d(b))
10: F(a) -> F(d(a))
11: F(c(b)) -> F(d(a))
12: E(g(X)) -> E(X)
The approximated dependency graph contains one SCC:
{12}.
- Consider the SCC {12}.
There are no usable rules.
By taking the polynomial interpretation
[E](x) = [g](x) = x + 1,
rule 12
is strictly decreasing.
Hence the TRS is terminating.