YES
O(n)
TRS:
 {
               zeros() -> cons(0(), n__zeros()),
               zeros() -> n__zeros(),
           activate(X) -> X,
  activate(n__zeros()) -> zeros(),
     tail(cons(X, XS)) -> activate(XS)
 }
 Natural interpretation:
  Strict:
   {
                 zeros() -> cons(0(), n__zeros()),
                 zeros() -> n__zeros(),
             activate(X) -> X,
    activate(n__zeros()) -> zeros(),
       tail(cons(X, XS)) -> activate(XS)
   }
  Weak:
   {}
  Interpretation class: stronglylinear
  [tail](X0) = + 1*X0 + 3
  [activate](X0) = + 1*X0 + 2
  [zeros] = + 1
  [n__zeros] = + 0
  [0] = + 0
  [cons](X1, X0) = + 1*X0 + 1*X1 + 0
  
  Qed