Consider the TRS R consisting of the rewrite rules

1: f(c(s(x),y)) -> f(c(x,s(y)))
2: f(c(s(x),s(y))) -> g(c(x,y))
3: g(c(x,s(y))) -> g(c(s(x),y))
4: g(c(s(x),s(y))) -> f(c(x,y))

There are 4 dependency pairs:

5: F(c(s(x),y)) -> F(c(x,s(y)))
6: F(c(s(x),s(y))) -> G(c(x,y))
7: G(c(x,s(y))) -> G(c(s(x),y))
8: G(c(s(x),s(y))) -> F(c(x,y))

The approximated dependency graph contains one SCC:
{5-8}.

- Consider the SCC {5-8}.
There are no usable rules.
By taking the polynomial interpretation
[F](x) = [G](x) = [s](x) = x + 1
and [c](x,y) = x + y + 1,
the rules in {5,7}
are weakly decreasing and
the rules in {6,8}
are strictly decreasing.
There are 2 new SCCs.

- Consider the SCC {5}.
By taking the polynomial interpretation
[c](x,y) = [F](x) = [s](x) = x + 1,
rule 5
is strictly decreasing.

- Consider the SCC {7}.
By taking the polynomial interpretation
[G](x) = [s](x) = x + 1
and [c](x,y) = y + 1,
rule 7
is strictly decreasing.


Hence the TRS is terminating.