YES

Problem:
 zeros() -> cons(0(),n__zeros())
 tail(cons(X,XS)) -> activate(XS)
 zeros() -> n__zeros()
 activate(n__zeros()) -> zeros()
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   tail#(cons(X,XS)) -> activate#(XS)
   activate#(n__zeros()) -> zeros#()
  TRS:
   zeros() -> cons(0(),n__zeros())
   tail(cons(X,XS)) -> activate(XS)
   zeros() -> n__zeros()
   activate(n__zeros()) -> zeros()
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    tail#(cons(X,XS)) -> activate#(XS)
    activate#(n__zeros()) -> zeros#()
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [activate#](x0) = 5x0,
     
     [tail#](x0) = x0 + 0,
     
     [zeros#] = 0,
     
     [cons](x0, x1) = x0 + 6x1 + 0,
     
     [n__zeros] = 0
    orientation:
     tail#(cons(X,XS)) = X + 6XS + 0 >= 5XS = activate#(XS)
     
     activate#(n__zeros()) = 5 >= 0 = zeros#()
    problem:
     DPs:
      
     TRS:
      
    Qed