YES
TRS:
 {rev1(X, cons(Y, L)) -> rev1(Y, L),
     rev1(0(), nil()) -> 0(),
    rev1(s(X), nil()) -> s(X),
           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))))}
 DP:
  Strict:
   {rev1#(X, cons(Y, L)) -> rev1#(Y, L),
        rev#(cons(X, L)) -> rev1#(X, L),
        rev#(cons(X, L)) -> rev2#(X, L),
    rev2#(X, cons(Y, L)) -> rev#(cons(X, rev(rev2(Y, L)))),
    rev2#(X, cons(Y, L)) -> rev#(rev2(Y, L)),
    rev2#(X, cons(Y, L)) -> rev2#(Y, L)}
  Weak:
  {rev1(X, cons(Y, L)) -> rev1(Y, L),
      rev1(0(), nil()) -> 0(),
     rev1(s(X), nil()) -> s(X),
            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:
   {(rev#(cons(X, L)) -> rev1#(X, L), rev1#(X, cons(Y, L)) -> rev1#(Y, L))
    (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)) -> rev1#(X, L))
    (rev2#(X, cons(Y, L)) -> rev#(cons(X, rev(rev2(Y, L)))), rev#(cons(X, L)) -> rev2#(X, L))
    (rev#(cons(X, L)) -> rev2#(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#(rev2(Y, L)))
    (rev#(cons(X, L)) -> rev2#(X, L), rev2#(X, cons(Y, L)) -> rev2#(Y, L))
    (rev1#(X, cons(Y, L)) -> rev1#(Y, L), rev1#(X, cons(Y, L)) -> rev1#(Y, L))}
   SCCS:
    Scc:
     {    rev#(cons(X, L)) -> rev2#(X, L),
      rev2#(X, cons(Y, L)) -> rev#(cons(X, rev(rev2(Y, L)))),
      rev2#(X, cons(Y, L)) -> rev#(rev2(Y, L)),
      rev2#(X, cons(Y, L)) -> rev2#(Y, L)}
    Scc:
     {rev1#(X, cons(Y, L)) -> rev1#(Y, L)}
    SCC:
     Strict:
      {    rev#(cons(X, L)) -> rev2#(X, L),
       rev2#(X, cons(Y, L)) -> rev#(cons(X, rev(rev2(Y, L)))),
       rev2#(X, cons(Y, L)) -> rev#(rev2(Y, L)),
       rev2#(X, cons(Y, L)) -> rev2#(Y, L)}
     Weak:
     {rev1(X, cons(Y, L)) -> rev1(Y, L),
         rev1(0(), nil()) -> 0(),
        rev1(s(X), nil()) -> s(X),
               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))))}
     POLY:
      Argument Filtering:
       pi(rev2#) = 1, pi(rev2) = 1, pi(rev#) = 0, pi(rev) = 0, pi(cons) = [1], pi(s) = [], pi(nil) = [], pi(rev1) = [], pi(0) = []
      Usable Rules:
       {}
      Interpretation:
       [cons](x0) = x0 + 1
      Strict:
       {rev2#(X, cons(Y, L)) -> rev#(cons(X, rev(rev2(Y, L))))}
      Weak:
       {rev1(X, cons(Y, L)) -> rev1(Y, L),
           rev1(0(), nil()) -> 0(),
          rev1(s(X), nil()) -> s(X),
                 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:
       {}
       SCCS:
        
        Qed
    SCC:
     Strict:
      {rev1#(X, cons(Y, L)) -> rev1#(Y, L)}
     Weak:
     {rev1(X, cons(Y, L)) -> rev1(Y, L),
         rev1(0(), nil()) -> 0(),
        rev1(s(X), nil()) -> s(X),
               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))))}
     SPSC:
      Simple Projection:
       pi(rev1#) = 1
      Strict:
       {}
      Qed