Consider the TRS R consisting of the rewrite rules

1: a__zeros -> cons(0,zeros)
2: a__tail(cons(X,XS)) -> mark(XS)
3: mark(zeros) -> a__zeros
4: mark(tail(X)) -> a__tail(mark(X))
5: mark(cons(X1,X2)) -> cons(mark(X1),X2)
6: mark(0) -> 0
7: a__zeros -> zeros
8: a__tail(X) -> tail(X)

There are 5 dependency pairs:

9: A__TAIL(cons(X,XS)) -> MARK(XS)
10: MARK(zeros) -> A__ZEROS
11: MARK(tail(X)) -> A__TAIL(mark(X))
12: MARK(tail(X)) -> MARK(X)
13: MARK(cons(X1,X2)) -> MARK(X1)

The approximated dependency graph contains one SCC:
{9,11-13}.

- Consider the SCC {9,11-13}.
By taking the polynomial interpretation
[0] = [zeros] = 0,
[a__zeros] = 1,
[a__tail](x) = [A__TAIL](x) = [mark](x) = [MARK](x) = [tail](x) = x + 1
and [cons](x,y) = x + y + 1,
the rules in {1,3-5,8,11}
are weakly decreasing and
the rules in {2,6,7,9,12,13}
are strictly decreasing.

Hence the TRS is terminating.