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