Consider the TRS R consisting of the rewrite rules
1: f(g(X)) -> g(f(f(X)))
2: f(h(X)) -> h(g(X))
There are 2 dependency pairs:
3: F(g(X)) -> F(f(X))
4: F(g(X)) -> F(X)
Consider the SCC {3,4}.
By taking the polynomial interpretation
[h](x) = 1,
[f](x) = x
and [F](x) = [g](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.