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)
   TDG 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#(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)
     copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z)) -> copy#(0(),y,z) -> f#(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)
     f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),y,z) ->
     copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z))
     f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),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)
    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: 4
      #arcs: 8/16
      DPs:
       copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z))
       copy#(0(),y,z) -> f#(z)
       f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),y,z)
       copy#(s(x),y,z) -> f#(y)
      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,
        
        [f#](x0) = 0,
        
        [s](x0) = x0,
        
        [0] = 1,
        
        [copy](x0, x1, x2) = x2 + 1,
        
        [n] = 0,
        
        [f](x0) = x0 + 1,
        
        [cons](x0, x1) = x1,
        
        [nil] = 0
       orientation:
        copy#(s(x),y,z) = x >= x = copy#(x,y,cons(f(y),z))
        
        copy#(0(),y,z) = 1 >= 0 = f#(z)
        
        f#(cons(f(cons(nil(),y)),z)) = 0 >= 0 = copy#(n(),y,z)
        
        copy#(s(x),y,z) = x >= 0 = f#(y)
        
        f(cons(nil(),y)) = y + 1 >= y = y
        
        f(cons(f(cons(nil(),y)),z)) = z + 1 >= z + 1 = copy(n(),y,z)
        
        copy(0(),y,z) = z + 1 >= z + 1 = f(z)
        
        copy(s(x),y,z) = z + 1 >= z + 1 = copy(x,y,cons(f(y),z))
       problem:
        DPs:
         copy#(s(x),y,z) -> copy#(x,y,cons(f(y),z))
         f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),y,z)
         copy#(s(x),y,z) -> f#(y)
        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,
         
         [f#](x0) = 0,
         
         [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(f(cons(nil(),y)),z)) = 0 >= 0 = copy#(n(),y,z)
         
         copy#(s(x),y,z) = x + 1 >= 0 = f#(y)
         
         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:
          f#(cons(f(cons(nil(),y)),z)) -> copy#(n(),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) = 0,
          
          [f#](x0) = 1,
          
          [s](x0) = 0,
          
          [0] = 0,
          
          [copy](x0, x1, x2) = x2,
          
          [n] = 0,
          
          [f](x0) = x0,
          
          [cons](x0, x1) = x1,
          
          [nil] = 0
         orientation:
          f#(cons(f(cons(nil(),y)),z)) = 1 >= 0 = copy#(n(),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