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.