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:
    
   TDG Processor:
    DPs:
     rev#(ls) -> r1#(ls,empty())
     r1#(cons(x,k),a) -> r1#(k,cons(x,a))
    TRS:
     
    graph:
     r1#(cons(x,k),a) -> r1#(k,cons(x,a)) ->
     r1#(cons(x,k),a) -> r1#(k,cons(x,a))
     rev#(ls) -> r1#(ls,empty()) -> r1#(cons(x,k),a) -> r1#(k,cons(x,a))
    Restore Modifier:
     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))
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 2/4
      DPs:
       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))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [r1#](x0, x1) = x0,
        
        [cons](x0, x1) = x1 + 1,
        
        [r1](x0, x1) = x0 + x1 + 1,
        
        [empty] = 0,
        
        [rev](x0) = x0 + 1
       orientation:
        r1#(cons(x,k),a) = k + 1 >= k = r1#(k,cons(x,a))
        
        rev(ls) = ls + 1 >= ls + 1 = r1(ls,empty())
        
        r1(empty(),a) = a + 1 >= a = a
        
        r1(cons(x,k),a) = a + k + 2 >= a + k + 2 = r1(k,cons(x,a))
       problem:
        DPs:
         
        TRS:
         rev(ls) -> r1(ls,empty())
         r1(empty(),a) -> a
         r1(cons(x,k),a) -> r1(k,cons(x,a))
       Qed