YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { a__zeros() -> cons(0(), zeros())
  , a__zeros() -> zeros()
  , a__tail(X) -> tail(X)
  , a__tail(cons(X, XS)) -> mark(XS)
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(0()) -> 0()
  , mark(zeros()) -> a__zeros()
  , mark(tail(X)) -> a__tail(mark(X)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 4. The enriched problem is
compatible with the following automaton.
{ a__zeros_0() -> 1
, a__zeros_1() -> 1
, a__zeros_2() -> 1
, a__zeros_3() -> 1
, cons_0(2, 2) -> 2
, cons_1(1, 2) -> 1
, cons_1(3, 4) -> 1
, cons_2(5, 6) -> 1
, cons_3(7, 8) -> 1
, cons_4(9, 10) -> 1
, 0_0() -> 2
, 0_1() -> 1
, 0_1() -> 3
, 0_2() -> 5
, 0_3() -> 7
, 0_4() -> 9
, zeros_0() -> 2
, zeros_1() -> 1
, zeros_1() -> 4
, zeros_2() -> 1
, zeros_2() -> 6
, zeros_3() -> 1
, zeros_3() -> 8
, zeros_4() -> 1
, zeros_4() -> 10
, a__tail_0(2) -> 1
, a__tail_1(1) -> 1
, mark_0(2) -> 1
, mark_1(2) -> 1
, mark_2(2) -> 1
, mark_2(4) -> 1
, mark_2(6) -> 1
, mark_2(8) -> 1
, mark_2(10) -> 1
, tail_0(2) -> 2
, tail_1(2) -> 1
, tail_2(1) -> 1 }

Hurray, we answered YES(?,O(n^1))