YES

Problem:
 rev(ls) -> r1(ls,empty())
 r1(empty(),a) -> a
 r1(cons(x,k),a) -> r1(k,cons(x,a))

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