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))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
    [r1#](x0, x1) = [0 1 0]x0 + [0 0 1]x1,
    
    [rev#](x0) = [1 1 0]x0 + [1],
    
                     [0 0 0]     [0]
    [cons](x0, x1) = [0 1 0]x1 + [1]
                     [0 0 0]     [0],
    
                   [0 0 0]     [1 0 1]     [0]
    [r1](x0, x1) = [0 1 0]x0 + [1 1 0]x1 + [0]
                   [0 0 0]     [0 0 1]     [1],
    
              [0]
    [empty] = [1]
              [0],
    
                [0 1 0]     [1]
    [rev](x0) = [0 1 0]x0 + [1]
                [0 0 0]     [1]
   orientation:
    rev#(ls) = [1 1 0]ls + [1] >= [0 1 0]ls = r1#(ls,empty())
    
    r1#(cons(x,k),a) = [0 0 1]a + [0 1 0]k + [1] >= [0 1 0]k = r1#(k,cons(x,a))
    
              [0 1 0]     [1]    [0 0 0]     [0]                 
    rev(ls) = [0 1 0]ls + [1] >= [0 1 0]ls + [1] = r1(ls,empty())
              [0 0 0]     [1]    [0 0 0]     [1]                 
    
                    [1 0 1]    [0]         
    r1(empty(),a) = [1 1 0]a + [1] >= a = a
                    [0 0 1]    [1]         
    
                      [1 0 1]    [0 0 0]    [0]    [0 0 0]    [0 0 0]    [0]                  
    r1(cons(x,k),a) = [1 1 0]a + [0 1 0]k + [1] >= [0 1 0]a + [0 1 0]k + [1] = r1(k,cons(x,a))
                      [0 0 1]    [0 0 0]    [1]    [0 0 0]    [0 0 0]    [1]                  
   problem:
    DPs:
     
    TRS:
     rev(ls) -> r1(ls,empty())
     r1(empty(),a) -> a
     r1(cons(x,k),a) -> r1(k,cons(x,a))
   Qed