Consider the TRS R consisting of the rewrite rules 1: f(x) -> s(x) 2: f(s(s(x))) -> s(f(f(x))) There are 2 dependency pairs: 3: F(s(s(x))) -> F(f(x)) 4: F(s(s(x))) -> F(x) Consider the SCC {3,4}. By taking the polynomial interpretation [f](x) = [F](x) = [s](x) = x + 1, the rules in {1,2} are weakly decreasing and the rules in {3,4} are strictly decreasing. Hence the TRS is terminating.