Consider the TRS R consisting of the rewrite rules

1: f(s(X)) -> f(X)
2: g(cons(0,Y)) -> g(Y)
3: g(cons(s(X),Y)) -> s(X)
4: h(cons(X,Y)) -> h(g(cons(X,Y)))

There are 4 dependency pairs:

5: F(s(X)) -> F(X)
6: G(cons(0,Y)) -> G(Y)
7: H(cons(X,Y)) -> H(g(cons(X,Y)))
8: H(cons(X,Y)) -> G(cons(X,Y))

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

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

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

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

Hence the TRS is terminating.