YES

Problem:
 rev(xs) -> revtl(xs,nil())
 revtl(nil(),ys) -> ys
 revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))

Proof:
 DP Processor:
  DPs:
   rev#(xs) -> revtl#(xs,nil())
   revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys))
  TRS:
   rev(xs) -> revtl(xs,nil())
   revtl(nil(),ys) -> ys
   revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
  TDG Processor:
   DPs:
    rev#(xs) -> revtl#(xs,nil())
    revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys))
   TRS:
    rev(xs) -> revtl(xs,nil())
    revtl(nil(),ys) -> ys
    revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
   graph:
    revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys)) ->
    revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys))
    rev#(xs) -> revtl#(xs,nil()) -> revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys))
   CDG Processor:
    DPs:
     rev#(xs) -> revtl#(xs,nil())
     revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys))
    TRS:
     rev(xs) -> revtl(xs,nil())
     revtl(nil(),ys) -> ys
     revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
    graph:
     
    Qed