Consider the TRS R consisting of the rewrite rules

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

There are 3 dependency pairs:

4: F(c(s(x),y)) -> F(c(x,s(y)))
5: G(c(x,s(y))) -> G(c(s(x),y))
6: G(s(f(x))) -> G(f(x))

The approximated dependency graph contains 3 SCCs:
{4},
{5}
and {6}.

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

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

- Consider the SCC {6}.
The usable rules are {1}.
By taking the polynomial interpretation
[f](x) = [G](x) = [s](x) = x + 1
and [c](x,y) = x + y + 1,
rule 1
is weakly decreasing and
rule 6
is strictly decreasing.

Hence the TRS is terminating.