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