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