Consider the TRS R consisting of the rewrite rules
1: a(c(d(x))) -> c(x)
2: u(b(d(d(x)))) -> b(x)
3: v(a(a(x))) -> u(v(x))
4: v(a(c(x))) -> u(b(d(x)))
5: v(c(x)) -> b(x)
6: w(a(a(x))) -> u(w(x))
7: w(a(c(x))) -> u(b(d(x)))
8: w(c(x)) -> b(x)
There are 6 dependency pairs:
9: V(a(a(x))) -> U(v(x))
10: V(a(a(x))) -> V(x)
11: V(a(c(x))) -> U(b(d(x)))
12: W(a(a(x))) -> U(w(x))
13: W(a(a(x))) -> W(x)
14: W(a(c(x))) -> U(b(d(x)))
The approximated dependency graph contains 2 SCCs:
{10}
and {13}.
- Consider the SCC {10}.
There are no usable rules.
By taking the polynomial interpretation
[a](x) = [V](x) = x + 1,
rule 10
is strictly decreasing.
- Consider the SCC {13}.
There are no usable rules.
By taking the polynomial interpretation
[a](x) = [W](x) = x + 1,
rule 13
is strictly decreasing.
Hence the TRS is terminating.