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))
  TDG 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))
   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))
   CDG 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))
    graph:
     
    Qed