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