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