YES
Time: 0.036789
TRS:
 {     intlist nil() -> nil(),
  intlist cons(x, y) -> cons(s x, intlist y),
       int(s x, s y) -> intlist int(x, y),
       int(s x, 0()) -> nil(),
       int(0(), s y) -> cons(0(), int(s 0(), s y)),
       int(0(), 0()) -> cons(0(), nil())}
 DP:
  DP:
   {intlist# cons(x, y) -> intlist# y,
         int#(s x, s y) -> intlist# int(x, y),
         int#(s x, s y) -> int#(x, y),
         int#(0(), s y) -> int#(s 0(), s y)}
  TRS:
  {     intlist nil() -> nil(),
   intlist cons(x, y) -> cons(s x, intlist y),
        int(s x, s y) -> intlist int(x, y),
        int(s x, 0()) -> nil(),
        int(0(), s y) -> cons(0(), int(s 0(), s y)),
        int(0(), 0()) -> cons(0(), nil())}
  EDG:
   {(int#(0(), s y) -> int#(s 0(), s y), int#(s x, s y) -> int#(x, y))
    (int#(0(), s y) -> int#(s 0(), s y), int#(s x, s y) -> intlist# int(x, y))
    (int#(s x, s y) -> intlist# int(x, y), intlist# cons(x, y) -> intlist# y)
    (int#(s x, s y) -> int#(x, y), int#(s x, s y) -> intlist# int(x, y))
    (int#(s x, s y) -> int#(x, y), int#(s x, s y) -> int#(x, y))
    (int#(s x, s y) -> int#(x, y), int#(0(), s y) -> int#(s 0(), s y))
    (intlist# cons(x, y) -> intlist# y, intlist# cons(x, y) -> intlist# y)}
   STATUS:
    arrows: 0.562500
    SCCS (2):
     Scc:
      {int#(s x, s y) -> int#(x, y),
       int#(0(), s y) -> int#(s 0(), s y)}
     Scc:
      {intlist# cons(x, y) -> intlist# y}
     
     SCC (2):
      Strict:
       {int#(s x, s y) -> int#(x, y),
        int#(0(), s y) -> int#(s 0(), s y)}
      Weak:
      {     intlist nil() -> nil(),
       intlist cons(x, y) -> cons(s x, intlist y),
            int(s x, s y) -> intlist int(x, y),
            int(s x, 0()) -> nil(),
            int(0(), s y) -> cons(0(), int(s 0(), s y)),
            int(0(), 0()) -> cons(0(), nil())}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [cons](x0, x1) = 1,
        
        [int](x0, x1) = 0,
        
        [intlist](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [nil] = 1,
        
        [0] = 0,
        
        [int#](x0, x1) = x0
       Strict:
        int#(0(), s y) -> int#(s 0(), s y)
        1 + 1y >= 1 + 1y
        int#(s x, s y) -> int#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        int(0(), 0()) -> cons(0(), nil())
        0 >= 1
        int(0(), s y) -> cons(0(), int(s 0(), s y))
        0 + 0y >= 1 + 0y
        int(s x, 0()) -> nil()
        0 + 0x >= 1
        int(s x, s y) -> intlist int(x, y)
        0 + 0x + 0y >= 1 + 0x + 0y
        intlist cons(x, y) -> cons(s x, intlist y)
        2 + 0x + 0y >= 1 + 0x + 0y
        intlist nil() -> nil()
        2 >= 1
      SCCS (0):
       
       
    
    SCC (1):
     Strict:
      {intlist# cons(x, y) -> intlist# y}
     Weak:
     {     intlist nil() -> nil(),
      intlist cons(x, y) -> cons(s x, intlist y),
           int(s x, s y) -> intlist int(x, y),
           int(s x, 0()) -> nil(),
           int(0(), s y) -> cons(0(), int(s 0(), s y)),
           int(0(), 0()) -> cons(0(), nil())}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [cons](x0, x1) = x0 + x1 + 1,
       
       [int](x0, x1) = 0,
       
       [intlist](x0) = 0,
       
       [s](x0) = x0 + 1,
       
       [nil] = 0,
       
       [0] = 1,
       
       [intlist#](x0) = x0
      Strict:
       intlist# cons(x, y) -> intlist# y
       1 + 1x + 1y >= 0 + 1y
      Weak:
       int(0(), 0()) -> cons(0(), nil())
       0 >= 2
       int(0(), s y) -> cons(0(), int(s 0(), s y))
       0 + 0y >= 2 + 0y
       int(s x, 0()) -> nil()
       0 + 0x >= 0
       int(s x, s y) -> intlist int(x, y)
       0 + 0x + 0y >= 0 + 0x + 0y
       intlist cons(x, y) -> cons(s x, intlist y)
       0 + 0x + 0y >= 2 + 1x + 0y
       intlist nil() -> nil()
       0 >= 0
     Qed