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