YES

Problem:
 f(cons(nil(),y)) -> y
 f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
 copy(0(),y,z) -> f(z)
 copy(s(x),y,z) -> copy(x,y,cons(f(y),z))

Proof:
 DP Processor:
  DPs:
   f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),y,z)
   copy#(0(),y,z) -> f#(z)
   copy#(s(x),y,z) -> f#(y)
   copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z))
  TRS:
   f(cons(nil(),y)) -> y
   f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
   copy(0(),y,z) -> f(z)
   copy(s(x),y,z) -> copy(x,y,cons(f(y),z))
  Usable Rule Processor:
   DPs:
    f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),y,z)
    copy#(0(),y,z) -> f#(z)
    copy#(s(x),y,z) -> f#(y)
    copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z))
   TRS:
    f(cons(nil(),y)) -> y
    f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [copy#](x0, x1, x2) = x0 + 0,
     
     [f#](x0) = 1,
     
     [s](x0) = 2x0 + 4,
     
     [0] = 4,
     
     [copy](x0, x1, x2) = 6x0 + x1 + x2 + 0,
     
     [n] = 0,
     
     [f](x0) = x0 + 0,
     
     [cons](x0, x1) = x1 + 0,
     
     [nil] = 2
    orientation:
     f#(cons(f(cons(nil(),y)),z)) = 1 >= 0 = copy#(n(),y,z)
     
     copy#(0(),y,z) = 4 >= 1 = f#(z)
     
     copy#(s(x),y,z) = 2x + 4 >= 1 = f#(y)
     
     copy#(s(x),y,z) = 2x + 4 >= x + 0 = copy#(x,y,cons(f(y),z))
     
     f(cons(nil(),y)) = y + 0 >= y = y
     
     f(cons(f(cons(nil(),y)),z)) = z + 0 >= y + z + 6 = copy(n(),y,z)
    problem:
     DPs:
      
     TRS:
      f(cons(nil(),y)) -> y
      f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
    Qed