Consider the TRS R consisting of the rewrite rules

1: int(0,0) -> 0 . nil
2: int(0,s(y)) -> 0 . int(s(0),s(y))
3: int(s(x),0) -> nil
4: int(s(x),s(y)) -> int_list(int(x,y))
5: int_list(nil) -> nil
6: int_list(x . y) -> s(x) . int_list(y)

There are 4 dependency pairs:

7: INT(0,s(y)) -> INT(s(0),s(y))
8: INT(s(x),s(y)) -> INT_LIST(int(x,y))
9: INT(s(x),s(y)) -> INT(x,y)
10: INT_LIST(x . y) -> INT_LIST(y)

The approximated dependency graph contains 2 SCCs:
{10}
and {7,9}.

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

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

Hence the TRS is terminating.