Consider the TRS R consisting of the rewrite rules

1: f(f(x)) -> f(g(f(x),x))
2: f(f(x)) -> f(h(f(x),f(x)))
3: g(x,y) -> y
4: h(x,x) -> g(x,0)

There are 5 dependency pairs:

5: F(f(x)) -> F(g(f(x),x))
6: F(f(x)) -> G(f(x),x)
7: F(f(x)) -> F(h(f(x),f(x)))
8: F(f(x)) -> H(f(x),f(x))
9: H(x,x) -> G(x,0)

The approximated dependency graph contains one SCC:
{5,7}.

- Consider the SCC {5,7}.
By taking the polynomial interpretation
[0] = 0,
[h](x,y) = x,
[f](x) = [F](x) = x + 1
and [g](x,y) = y,
the rules in {2-4,7}
are weakly decreasing and
the rules in {1,5}
are strictly decreasing.
There is one new SCC.

- Consider the SCC {7}.
By taking the polynomial interpretation
[0] = [h](x,y) = 0,
[f](x) = [F](x) = x + 1
and [g](x,y) = y,
the rules in {3,4}
are weakly decreasing and
the rules in {1,2,7}
are strictly decreasing.


Hence the TRS is terminating.