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
  Arctic Interpretation Processor:
   dimension: 1
   interpretation:
    [activate#](x0) = 2x0 + 0,
    
    [tail#](x0) = 4x0 + 2,
    
    [zeros#] = 1,
    
    [activate](x0) = 2x0,
    
    [tail](x0) = 3x0 + 0,
    
    [cons](x0, x1) = x1 + -3,
    
    [n__zeros] = 0,
    
    [0] = 4,
    
    [zeros] = 1
   orientation:
    tail#(cons(X,XS)) = 4XS + 2 >= 2XS + 0 = activate#(XS)
    
    activate#(n__zeros()) = 2 >= 1 = zeros#()
    
    zeros() = 1 >= 0 = cons(0(),n__zeros())
    
    tail(cons(X,XS)) = 3XS + 0 >= 2XS = activate(XS)
    
    zeros() = 1 >= 0 = n__zeros()
    
    activate(n__zeros()) = 2 >= 1 = zeros()
    
    activate(X) = 2X >= X = X
   problem:
    DPs:
     
    TRS:
     zeros() -> cons(0(),n__zeros())
     tail(cons(X,XS)) -> activate(XS)
     zeros() -> n__zeros()
     activate(n__zeros()) -> zeros()
     activate(X) -> X
   Qed