Consider the TRS R consisting of the rewrite rules

1: intlist(nil) -> nil
2: int(s(x),0) -> nil
3: int(x,x) -> cons(x,nil)
4: intlist(cons(x,y)) -> cons(s(x),intlist(y))
5: int(s(x),s(y)) -> intlist(int(x,y))
6: int(0,s(y)) -> cons(0,int(s(0),s(y)))
7: intlist(cons(x,nil)) -> cons(s(x),nil)

There are 4 dependency pairs:

8: INTLIST(cons(x,y)) -> INTLIST(y)
9: INT(s(x),s(y)) -> INTLIST(int(x,y))
10: INT(s(x),s(y)) -> INT(x,y)
11: INT(0,s(y)) -> INT(s(0),s(y))

The approximated dependency graph contains 2 SCCs:
{8}
and {10,11}.

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

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

Hence the TRS is terminating.