YES
Time: 0.030731
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))}
  UR:
   {        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)),
              a(w, v) -> w,
              a(w, v) -> v}
   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))}
    STATUS:
     arrows: 0.666667
     SCCS (2):
      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:
       {rev1#(x, ++(y, z)) -> rev1#(y, z)}
      
      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:
         rev2(x, ++(y, z)) -> rev ++(x, rev rev2(y, z))
         1 + 0x + 0y + 1z >= 1 + 0x + 0y + 1z
         rev2(x, nil()) -> nil()
         0 + 0x >= 0
         rev1(x, ++(y, z)) -> rev1(y, z)
         0 + 0x + 0y + 0z >= 0 + 0y + 0z
         rev1(x, nil()) -> x
         0 + 0x >= 1x
         rev ++(x, y) -> ++(rev1(x, y), rev2(x, y))
         1 + 0x + 1y >= 1 + 0x + 1y
         rev nil() -> nil()
         0 >= 0
       SCCS (0):
        
        
     
     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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [++](x0, x1) = x0 + x1 + 1,
        
        [rev1](x0, x1) = x0,
        
        [rev2](x0, x1) = x0,
        
        [rev](x0) = 0,
        
        [nil] = 0,
        
        [rev1#](x0, x1) = x0 + x1
       Strict:
        rev1#(x, ++(y, z)) -> rev1#(y, z)
        1 + 1x + 1y + 1z >= 0 + 1y + 1z
       Weak:
        rev2(x, ++(y, z)) -> rev ++(x, rev rev2(y, z))
        1 + 0x + 1y + 1z >= 0 + 0x + 0y + 0z
        rev2(x, nil()) -> nil()
        0 + 0x >= 0
        rev1(x, ++(y, z)) -> rev1(y, z)
        1 + 0x + 1y + 1z >= 0 + 0y + 1z
        rev1(x, nil()) -> x
        0 + 0x >= 1x
        rev ++(x, y) -> ++(rev1(x, y), rev2(x, y))
        0 + 0x + 0y >= 1 + 0x + 2y
        rev nil() -> nil()
        0 >= 0
      Qed