Consider the TRS R consisting of the rewrite rules

1: f(s(X),X) -> f(X,a(X))
2: f(X,c(X)) -> f(s(X),X)
3: f(X,X) -> c(X)

There are 2 dependency pairs:

4: F(s(X),X) -> F(X,a(X))
5: F(X,c(X)) -> F(s(X),X)

The approximated dependency graph contains 2 SCCs:
{4}
and {5}.

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

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

Hence the TRS is terminating.