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