YES
Time: 0.008287
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:
  DP:
   {     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)}
  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))}
  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 (2):
    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 (1):
     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 (4):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [++](x0, x1) = x0 + 1,
       
       [rev1](x0, x1) = 0,
       
       [rev2](x0, x1) = x0,
       
       [rev](x0) = x0,
       
       [nil] = 0,
       
       [rev2#](x0, x1) = x0 + 1,
       
       [rev#](x0) = x0 + 1
      Strict:
       rev2#(x, ++(y, z)) -> rev2#(y, z)
       2 + 0x + 0y + 1z >= 1 + 0y + 1z
       rev2#(x, ++(y, z)) -> rev# rev2(y, z)
       2 + 0x + 0y + 1z >= 1 + 0y + 1z
       rev2#(x, ++(y, z)) -> rev# ++(x, rev rev2(y, z))
       2 + 0x + 0y + 1z >= 2 + 0x + 0y + 1z
       rev# ++(x, y) -> rev2#(x, y)
       2 + 0x + 1y >= 1 + 0x + 1y
      Weak:
       
     EDG:
      {}
      SCCS (0):
       
       Qed