Consider the TRS R consisting of the rewrite rules 1: f(h(x)) -> f(i(x)) 2: g(i(x)) -> g(h(x)) 3: h(a) -> b 4: i(a) -> b There are 4 dependency pairs: 5: F(h(x)) -> F(i(x)) 6: F(h(x)) -> I(x) 7: G(i(x)) -> G(h(x)) 8: G(i(x)) -> H(x) The approximated dependency graph contains 2 SCCs: {5} and {7}. - Consider the SCC {5}. The usable rules are {4}. By taking the polynomial interpretation [a] = [b] = 1, [i](x) = x and [F](x) = [h](x) = x + 1, rule 4 is weakly decreasing and rule 5 is strictly decreasing. - Consider the SCC {7}. The usable rules are {3}. By taking the polynomial interpretation [a] = [b] = 1, [h](x) = x and [G](x) = [i](x) = x + 1, rule 3 is weakly decreasing and rule 7 is strictly decreasing. Hence the TRS is terminating.