YES

Problem:
 f(x,empty()) -> x
 f(empty(),cons(a,k)) -> f(cons(a,k),k)
 f(cons(a,k),y) -> f(y,k)

Proof:
 DP Processor:
  DPs:
   f#(empty(),cons(a,k)) -> f#(cons(a,k),k)
   f#(cons(a,k),y) -> f#(y,k)
  TRS:
   f(x,empty()) -> x
   f(empty(),cons(a,k)) -> f(cons(a,k),k)
   f(cons(a,k),y) -> f(y,k)
  Usable Rule Processor:
   DPs:
    f#(empty(),cons(a,k)) -> f#(cons(a,k),k)
    f#(cons(a,k),y) -> f#(y,k)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [f#](x0, x1) = -2x0 + x1 + -16,
     
     [cons](x0, x1) = 4x1 + 1,
     
     [empty] = 0
    orientation:
     f#(empty(),cons(a,k)) = 4k + 1 >= 2k + -1 = f#(cons(a,k),k)
     
     f#(cons(a,k),y) = 2k + y + -1 >= k + -2y + -16 = f#(y,k)
    problem:
     DPs:
      
     TRS:
      
    Qed