Consider the TRS R consisting of the rewrite rules 1: w(r(x)) -> r(w(x)) 2: b(r(x)) -> r(b(x)) 3: b(w(x)) -> w(b(x)) There are 4 dependency pairs: 4: W(r(x)) -> W(x) 5: B(r(x)) -> B(x) 6: B(w(x)) -> W(b(x)) 7: B(w(x)) -> B(x) The approximated dependency graph contains 2 SCCs: {4} and {5,7}. - Consider the SCC {4}. There are no usable rules. By taking the polynomial interpretation [r](x) = [W](x) = x + 1, rule 4 is strictly decreasing. - Consider the SCC {5,7}. There are no usable rules. By taking the polynomial interpretation [B](x) = [r](x) = [w](x) = x + 1, the rules in {5,7} are strictly decreasing. Hence the TRS is terminating.