Consider the TRS R consisting of the rewrite rules

1: f(0,y) -> 0
2: f(s(x),y) -> f(f(x,y),y)

There are 2 dependency pairs:

3: F(s(x),y) -> F(f(x,y),y)
4: F(s(x),y) -> F(x,y)

The approximated dependency graph contains one SCC:
{3,4}.

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

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


Hence the TRS is terminating.