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))
  Usable Rule Processor:
   DPs:
    rev#(xs) -> revtl#(xs,nil())
    revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys))
   TRS:
    
   CDG Processor:
    DPs:
     rev#(xs) -> revtl#(xs,nil())
     revtl#(cons(x,xs),ys) -> revtl#(xs,cons(x,ys))
    TRS:
     
    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))
    Restore Modifier:
     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))
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 2/4
      DPs:
       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))
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [revtl#](x0, x1) = x0,
        
        [cons](x0, x1) = x1 + 1,
        
        [revtl](x0, x1) = x0 + x1 + 1,
        
        [nil] = 0,
        
        [rev](x0) = x0 + 1
       orientation:
        revtl#(cons(x,xs),ys) = xs + 1 >= xs = revtl#(xs,cons(x,ys))
        
        rev(xs) = xs + 1 >= xs + 1 = revtl(xs,nil())
        
        revtl(nil(),ys) = ys + 1 >= ys = ys
        
        revtl(cons(x,xs),ys) = xs + ys + 2 >= xs + ys + 2 = revtl(xs,cons(x,ys))
       problem:
        DPs:
         
        TRS:
         rev(xs) -> revtl(xs,nil())
         revtl(nil(),ys) -> ys
         revtl(cons(x,xs),ys) -> revtl(xs,cons(x,ys))
       Qed