(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(zeros) → mark(cons(0, zeros))
active(tail(cons(X, XS))) → mark(XS)
mark(zeros) → active(zeros)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(0) → active(0)
mark(tail(X)) → active(tail(mark(X)))
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)

Q is empty.