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:
    f9(x,y) -> x
    f9(x,y) -> y
    f(cons(nil(),y)) -> y
    f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
   EDG 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:
     f9(x,y) -> x
     f9(x,y) -> y
     f(cons(nil(),y)) -> y
     f(cons(f(cons(nil(),y)),z)) -> copy(n(),y,z)
    graph:
     copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z)) ->
     copy#(0(),y,z) -> f#(z)
     copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z)) ->
     copy#(s(x),y,z) -> f#(y)
     copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z)) ->
     copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z))
     copy#(s(x),y,z) -> f#(y) ->
     f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),y,z)
     copy#(0(),y,z) -> f#(z) -> f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),y,z)
    Restore Modifier:
     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))
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 5/16
      DPs:
       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))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [copy#](x0, x1, x2) = x0,
        
        [s](x0) = x0 + 1,
        
        [0] = 0,
        
        [copy](x0, x1, x2) = x2,
        
        [n] = 0,
        
        [f](x0) = x0,
        
        [cons](x0, x1) = x1,
        
        [nil] = 0
       orientation:
        copy#(s(x),y,z) = x + 1 >= x = copy#(x,y,cons(f(y),z))
        
        f(cons(nil(),y)) = y >= y = y
        
        f(cons(f(cons(nil(),y)),z)) = z >= z = copy(n(),y,z)
        
        copy(0(),y,z) = z >= z = f(z)
        
        copy(s(x),y,z) = z >= z = copy(x,y,cons(f(y),z))
       problem:
        DPs:
         
        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))
       Qed