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))))
  EDG 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))))
   graph:
    rev2#(X,cons(Y,L)) -> rev2#(Y,L) ->
    rev2#(X,cons(Y,L)) -> rev2#(Y,L)
    rev2#(X,cons(Y,L)) -> rev2#(Y,L) ->
    rev2#(X,cons(Y,L)) -> rev#(rev2(Y,L))
    rev2#(X,cons(Y,L)) -> rev2#(Y,L) ->
    rev2#(X,cons(Y,L)) -> rev#(cons(X,rev(rev2(Y,L))))
    rev2#(X,cons(Y,L)) -> rev#(rev2(Y,L)) ->
    rev#(cons(X,L)) -> rev2#(X,L)
    rev2#(X,cons(Y,L)) -> rev#(rev2(Y,L)) ->
    rev#(cons(X,L)) -> rev1#(X,L)
    rev2#(X,cons(Y,L)) -> rev#(cons(X,rev(rev2(Y,L)))) ->
    rev#(cons(X,L)) -> rev2#(X,L)
    rev2#(X,cons(Y,L)) -> rev#(cons(X,rev(rev2(Y,L)))) ->
    rev#(cons(X,L)) -> rev1#(X,L)
    rev#(cons(X,L)) -> rev2#(X,L) -> rev2#(X,cons(Y,L)) -> rev2#(Y,L)
    rev#(cons(X,L)) -> rev2#(X,L) ->
    rev2#(X,cons(Y,L)) -> rev#(rev2(Y,L))
    rev#(cons(X,L)) -> rev2#(X,L) ->
    rev2#(X,cons(Y,L)) -> rev#(cons(X,rev(rev2(Y,L))))
    rev#(cons(X,L)) -> rev1#(X,L) ->
    rev1#(X,cons(Y,L)) -> rev1#(Y,L)
    rev1#(X,cons(Y,L)) -> rev1#(Y,L) -> rev1#(X,cons(Y,L)) -> rev1#(Y,L)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 12/36
    DPs:
     rev2#(X,cons(Y,L)) -> rev2#(Y,L)
     rev2#(X,cons(Y,L)) -> rev#(cons(X,rev(rev2(Y,L))))
     rev#(cons(X,L)) -> rev2#(X,L)
     rev2#(X,cons(Y,L)) -> 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:
     dimension: 1
     interpretation:
      [rev2#](x0, x1) = x1 + 1,
      
      [rev#](x0) = x0 + 1,
      
      [rev2](x0, x1) = x1,
      
      [rev](x0) = x0,
      
      [cons](x0, x1) = x1 + 1,
      
      [s](x0) = 0,
      
      [rev1](x0, x1) = 0,
      
      [nil] = 0,
      
      [0] = 0
     orientation:
      rev2#(X,cons(Y,L)) = L + 2 >= L + 1 = rev2#(Y,L)
      
      rev2#(X,cons(Y,L)) = L + 2 >= L + 2 = rev#(cons(X,rev(rev2(Y,L))))
      
      rev#(cons(X,L)) = L + 2 >= L + 1 = rev2#(X,L)
      
      rev2#(X,cons(Y,L)) = L + 2 >= L + 1 = rev#(rev2(Y,L))
      
      rev1(0(),nil()) = 0 >= 0 = 0()
      
      rev1(s(X),nil()) = 0 >= 0 = s(X)
      
      rev1(X,cons(Y,L)) = 0 >= 0 = rev1(Y,L)
      
      rev(nil()) = 0 >= 0 = nil()
      
      rev(cons(X,L)) = L + 1 >= L + 1 = cons(rev1(X,L),rev2(X,L))
      
      rev2(X,nil()) = 0 >= 0 = nil()
      
      rev2(X,cons(Y,L)) = L + 1 >= L + 1 = rev(cons(X,rev(rev2(Y,L))))
     problem:
      DPs:
       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:
      dimension: 1
      interpretation:
       [rev2#](x0, x1) = 1,
       
       [rev#](x0) = 0,
       
       [rev2](x0, x1) = 0,
       
       [rev](x0) = 0,
       
       [cons](x0, x1) = 0,
       
       [s](x0) = 0,
       
       [rev1](x0, x1) = 0,
       
       [nil] = 0,
       
       [0] = 0
      orientation:
       rev2#(X,cons(Y,L)) = 1 >= 0 = rev#(cons(X,rev(rev2(Y,L))))
       
       rev1(0(),nil()) = 0 >= 0 = 0()
       
       rev1(s(X),nil()) = 0 >= 0 = s(X)
       
       rev1(X,cons(Y,L)) = 0 >= 0 = rev1(Y,L)
       
       rev(nil()) = 0 >= 0 = nil()
       
       rev(cons(X,L)) = 0 >= 0 = cons(rev1(X,L),rev2(X,L))
       
       rev2(X,nil()) = 0 >= 0 = nil()
       
       rev2(X,cons(Y,L)) = 0 >= 0 = 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
    
    DPs:
     rev1#(X,cons(Y,L)) -> rev1#(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))))
    Subterm Criterion Processor:
     simple projection:
      pi(rev1#) = 1
     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