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