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)
  EDG 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)
   graph:
    f#(cons(a,k),y) -> f#(y,k) ->
    f#(empty(),cons(a,k)) -> f#(cons(a,k),k)
    f#(cons(a,k),y) -> f#(y,k) ->
    f#(cons(a,k),y) -> f#(y,k)
    f#(empty(),cons(a,k)) -> f#(cons(a,k),k) -> f#(cons(a,k),y) -> f#(y,k)
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [f#](x0, x1) = x0 + 1x1,
     
     [cons](x0, x1) = 2x0 + 4x1 + 0,
     
     [f](x0, x1) = 1x0 + 3x1 + -16,
     
     [empty] = 0
    orientation:
     f#(empty(),cons(a,k)) = 3a + 5k + 1 >= 2a + 4k + 0 = f#(cons(a,k),k)
     
     f#(cons(a,k),y) = 2a + 4k + 1y + 0 >= 1k + y = f#(y,k)
     
     f(x,empty()) = 1x + 3 >= x = x
     
     f(empty(),cons(a,k)) = 5a + 7k + 3 >= 3a + 5k + 1 = f(cons(a,k),k)
     
     f(cons(a,k),y) = 3a + 5k + 3y + 1 >= 3k + 1y + -16 = f(y,k)
    problem:
     DPs:
      
     TRS:
      f(x,empty()) -> x
      f(empty(),cons(a,k)) -> f(cons(a,k),k)
      f(cons(a,k),y) -> f(y,k)
    Qed