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.