Consider the TRS R consisting of the rewrite rules

1: f(c(X,s(Y))) -> f(c(s(X),Y))
2: g(c(s(X),Y)) -> f(c(X,s(Y)))

There are 2 dependency pairs:

3: F(c(X,s(Y))) -> F(c(s(X),Y))
4: G(c(s(X),Y)) -> F(c(X,s(Y)))

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

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

Hence the TRS is terminating.