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

Strict Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , tail(cons(X, XS)) -> activate(XS)
  , activate(X) -> X
  , activate(n__zeros()) -> zeros() }
Obligation:
  runtime complexity
Answer:
  YES(?,O(1))

The input is overlay and right-linear. Switching to innermost
rewriting.

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

Strict Trs:
  { zeros() -> cons(0(), n__zeros())
  , zeros() -> n__zeros()
  , tail(cons(X, XS)) -> activate(XS)
  , activate(X) -> X
  , activate(n__zeros()) -> zeros() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(1))

The input was oriented with the instance of 'Small Polynomial Path
Order (PS,0-bounded)' as induced by the safe mapping

 safe(zeros) = {}, safe(cons) = {1, 2}, safe(0) = {},
 safe(n__zeros) = {}, safe(tail) = {1}, safe(activate) = {1}

and precedence

 tail > activate, activate > zeros .

Following symbols are considered recursive:

 {}

The recursion depth is 0.

For your convenience, here are the satisfied ordering constraints:

                 zeros() > cons(; 0(),  n__zeros())
                                                   
                 zeros() > n__zeros()              
                                                   
  tail(; cons(; X,  XS)) > activate(; XS)          
                                                   
           activate(; X) > X                       
                                                   
  activate(; n__zeros()) > zeros()                 
                                                   

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