Consider the TRS R consisting of the rewrite rules

1: a__first(0,X) -> nil
2: a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
3: a__from(X) -> cons(mark(X),from(s(X)))
4: mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
5: mark(from(X)) -> a__from(mark(X))
6: mark(0) -> 0
7: mark(nil) -> nil
8: mark(s(X)) -> s(mark(X))
9: mark(cons(X1,X2)) -> cons(mark(X1),X2)
10: a__first(X1,X2) -> first(X1,X2)
11: a__from(X) -> from(X)

There are 9 dependency pairs:

12: A__FIRST(s(X),cons(Y,Z)) -> MARK(Y)
13: A__FROM(X) -> MARK(X)
14: MARK(first(X1,X2)) -> A__FIRST(mark(X1),mark(X2))
15: MARK(first(X1,X2)) -> MARK(X1)
16: MARK(first(X1,X2)) -> MARK(X2)
17: MARK(from(X)) -> A__FROM(mark(X))
18: MARK(from(X)) -> MARK(X)
19: MARK(s(X)) -> MARK(X)
20: MARK(cons(X1,X2)) -> MARK(X1)

Consider the SCC {12-20}.
By taking the polynomial interpretation
[0] = [nil] = 1,
[mark](x) = x,
[a__from](x) = [A__FROM](x) = [cons](x,y) = [from](x) = [MARK](x) = [s](x) = x + 1
and [a__first](x,y) = [A__FIRST](x,y) = [first](x,y) = x + y + 1,
the rules in {3-11,13}
are weakly decreasing and
the rules in {1,2,12,14-20}
are strictly decreasing.
Hence the TRS is terminating.