YES
Time: 0.016605
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:
  DP:
   {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)}
  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))}
  UR:
   {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)),
                a(x, y) -> x,
                a(x, y) -> y}
   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))}
    STATUS:
     arrows: 0.666667
     SCCS (2):
      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 (4):
       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:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [rev1](x0, x1) = x0 + 1,
         
         [cons](x0, x1) = x0 + 1,
         
         [rev2](x0, x1) = x0,
         
         [s](x0) = 0,
         
         [rev](x0) = x0,
         
         [0] = 0,
         
         [nil] = 1,
         
         [rev2#](x0, x1) = x0,
         
         [rev#](x0) = x0
        Strict:
         rev2#(X, cons(Y, L)) -> rev2#(Y, L)
         1 + 0X + 0Y + 1L >= 0 + 0Y + 1L
         rev2#(X, cons(Y, L)) -> rev# rev2(Y, L)
         1 + 0X + 0Y + 1L >= 0 + 0Y + 1L
         rev2#(X, cons(Y, L)) -> rev# cons(X, rev rev2(Y, L))
         1 + 0X + 0Y + 1L >= 1 + 0X + 0Y + 1L
         rev# cons(X, L) -> rev2#(X, L)
         1 + 0X + 1L >= 0 + 0X + 1L
        Weak:
         rev2(X, cons(Y, L)) -> rev cons(X, rev rev2(Y, L))
         1 + 0X + 0Y + 1L >= 1 + 0X + 0Y + 1L
         rev2(X, nil()) -> nil()
         1 + 0X >= 1
         rev cons(X, L) -> cons(rev1(X, L), rev2(X, L))
         1 + 0X + 1L >= 1 + 0X + 1L
         rev nil() -> nil()
         1 >= 1
         rev1(s X, nil()) -> s X
         2 + 0X >= 0 + 0X
         rev1(0(), nil()) -> 0()
         2 >= 0
         rev1(X, cons(Y, L)) -> rev1(Y, L)
         2 + 0X + 0Y + 1L >= 1 + 0Y + 1L
       SCCS (0):
        
        
     
     SCC (1):
      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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [rev1](x0, x1) = x0 + x1 + 1,
        
        [cons](x0, x1) = x0 + x1 + 1,
        
        [rev2](x0, x1) = x0 + x1 + 1,
        
        [s](x0) = 0,
        
        [rev](x0) = x0 + 1,
        
        [0] = 0,
        
        [nil] = 1,
        
        [rev1#](x0, x1) = x0 + x1
       Strict:
        rev1#(X, cons(Y, L)) -> rev1#(Y, L)
        1 + 1X + 1Y + 1L >= 0 + 1Y + 1L
       Weak:
        rev2(X, cons(Y, L)) -> rev cons(X, rev rev2(Y, L))
        2 + 1X + 1Y + 1L >= 4 + 1X + 1Y + 1L
        rev2(X, nil()) -> nil()
        2 + 1X >= 1
        rev cons(X, L) -> cons(rev1(X, L), rev2(X, L))
        2 + 1X + 1L >= 3 + 2X + 2L
        rev nil() -> nil()
        2 >= 1
        rev1(s X, nil()) -> s X
        2 + 0X >= 0 + 0X
        rev1(0(), nil()) -> 0()
        2 >= 0
        rev1(X, cons(Y, L)) -> rev1(Y, L)
        2 + 1X + 1Y + 1L >= 1 + 1Y + 1L
      Qed