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