YES

Problem:
 rev1(0(),nil()) -> 0()
 rev1(s(X),nil()) -> s(X)
 rev1(X,cons(Y,L)) -> rev1(Y,L)
 rev(nil()) -> nil()
 rev(cons(X,L)) -> cons(rev1(X,L),rev2(X,L))
 rev2(X,nil()) -> nil()
 rev2(X,cons(Y,L)) -> rev(cons(X,rev(rev2(Y,L))))

Proof:
 DP Processor:
  DPs:
   rev1#(X,cons(Y,L)) -> rev1#(Y,L)
   rev#(cons(X,L)) -> rev2#(X,L)
   rev#(cons(X,L)) -> rev1#(X,L)
   rev2#(X,cons(Y,L)) -> rev2#(Y,L)
   rev2#(X,cons(Y,L)) -> rev#(rev2(Y,L))
   rev2#(X,cons(Y,L)) -> rev#(cons(X,rev(rev2(Y,L))))
  TRS:
   rev1(0(),nil()) -> 0()
   rev1(s(X),nil()) -> s(X)
   rev1(X,cons(Y,L)) -> rev1(Y,L)
   rev(nil()) -> nil()
   rev(cons(X,L)) -> cons(rev1(X,L),rev2(X,L))
   rev2(X,nil()) -> nil()
   rev2(X,cons(Y,L)) -> rev(cons(X,rev(rev2(Y,L))))
  Matrix Interpretation Processor: dim=1
   
   usable rules:
    rev(nil()) -> nil()
    rev(cons(X,L)) -> cons(rev1(X,L),rev2(X,L))
    rev2(X,nil()) -> nil()
    rev2(X,cons(Y,L)) -> rev(cons(X,rev(rev2(Y,L))))
   interpretation:
    [rev2#](x0, x1) = 2x1 + 4,
    
    [rev#](x0) = 2x0 + 1,
    
    [rev1#](x0, x1) = 4x1,
    
    [rev2](x0, x1) = x1,
    
    [rev](x0) = x0,
    
    [cons](x0, x1) = 2x1 + 2,
    
    [s](x0) = 4x0,
    
    [rev1](x0, x1) = 5x0 + 3x1,
    
    [nil] = 1,
    
    [0] = 5
   orientation:
    rev1#(X,cons(Y,L)) = 8L + 8 >= 4L = rev1#(Y,L)
    
    rev#(cons(X,L)) = 4L + 5 >= 2L + 4 = rev2#(X,L)
    
    rev#(cons(X,L)) = 4L + 5 >= 4L = rev1#(X,L)
    
    rev2#(X,cons(Y,L)) = 4L + 8 >= 2L + 4 = rev2#(Y,L)
    
    rev2#(X,cons(Y,L)) = 4L + 8 >= 2L + 1 = rev#(rev2(Y,L))
    
    rev2#(X,cons(Y,L)) = 4L + 8 >= 4L + 5 = rev#(cons(X,rev(rev2(Y,L))))
    
    rev1(0(),nil()) = 28 >= 5 = 0()
    
    rev1(s(X),nil()) = 20X + 3 >= 4X = s(X)
    
    rev1(X,cons(Y,L)) = 6L + 5X + 6 >= 3L + 5Y = rev1(Y,L)
    
    rev(nil()) = 1 >= 1 = nil()
    
    rev(cons(X,L)) = 2L + 2 >= 2L + 2 = cons(rev1(X,L),rev2(X,L))
    
    rev2(X,nil()) = 1 >= 1 = nil()
    
    rev2(X,cons(Y,L)) = 2L + 2 >= 2L + 2 = rev(cons(X,rev(rev2(Y,L))))
   problem:
    DPs:
     
    TRS:
     rev1(0(),nil()) -> 0()
     rev1(s(X),nil()) -> s(X)
     rev1(X,cons(Y,L)) -> rev1(Y,L)
     rev(nil()) -> nil()
     rev(cons(X,L)) -> cons(rev1(X,L),rev2(X,L))
     rev2(X,nil()) -> nil()
     rev2(X,cons(Y,L)) -> rev(cons(X,rev(rev2(Y,L))))
   Qed