YES
Time: 0.015655
TRS:
 {   int(0(), 0()) -> .(0(), nil()),
     int(0(), s y) -> .(0(), int(s 0(), s y)),
     int(s x, 0()) -> nil(),
     int(s x, s y) -> int_list int(x, y),
  int_list .(x, y) -> .(s x, int_list y),
    int_list nil() -> nil()}
 DP:
  DP:
   {   int#(0(), s y) -> int#(s 0(), s y),
       int#(s x, s y) -> int#(x, y),
       int#(s x, s y) -> int_list# int(x, y),
    int_list# .(x, y) -> int_list# y}
  TRS:
  {   int(0(), 0()) -> .(0(), nil()),
      int(0(), s y) -> .(0(), int(s 0(), s y)),
      int(s x, 0()) -> nil(),
      int(s x, s y) -> int_list int(x, y),
   int_list .(x, y) -> .(s x, int_list y),
     int_list nil() -> nil()}
  EDG:
   {(int#(0(), s y) -> int#(s 0(), s y), int#(s x, s y) -> int_list# int(x, y))
    (int#(0(), s y) -> int#(s 0(), s y), int#(s x, s y) -> int#(x, y))
    (int#(s x, s y) -> int_list# int(x, y), int_list# .(x, y) -> int_list# y)
    (int#(s x, s y) -> int#(x, y), int#(0(), s y) -> int#(s 0(), s 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#(s x, s y) -> int_list# int(x, y))
    (int_list# .(x, y) -> int_list# y, int_list# .(x, y) -> int_list# y)}
   STATUS:
    arrows: 0.562500
    SCCS (2):
     Scc:
      {int#(0(), s y) -> int#(s 0(), s y),
       int#(s x, s y) -> int#(x, y)}
     Scc:
      {int_list# .(x, y) -> int_list# y}
     
     SCC (2):
      Strict:
       {int#(0(), s y) -> int#(s 0(), s y),
        int#(s x, s y) -> int#(x, y)}
      Weak:
      {   int(0(), 0()) -> .(0(), nil()),
          int(0(), s y) -> .(0(), int(s 0(), s y)),
          int(s x, 0()) -> nil(),
          int(s x, s y) -> int_list int(x, y),
       int_list .(x, y) -> .(s x, int_list y),
         int_list nil() -> nil()}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [.](x0, x1) = x0,
        
        [int](x0, x1) = 0,
        
        [s](x0) = x0 + 1,
        
        [int_list](x0) = 0,
        
        [0] = 0,
        
        [nil] = 0,
        
        [int#](x0, x1) = x0
       Strict:
        int#(s x, s y) -> int#(x, y)
        1 + 1y + 0x >= 0 + 1y + 0x
        int#(0(), s y) -> int#(s 0(), s y)
        1 + 1y >= 1 + 1y
       Weak:
        int_list nil() -> nil()
        0 >= 0
        int_list .(x, y) -> .(s x, int_list y)
        0 + 0y + 0x >= 1 + 0y + 1x
        int(s x, s y) -> int_list int(x, y)
        0 + 0y + 0x >= 0 + 0y + 0x
        int(s x, 0()) -> nil()
        0 + 0x >= 0
        int(0(), s y) -> .(0(), int(s 0(), s y))
        0 + 0y >= 0 + 0y
        int(0(), 0()) -> .(0(), nil())
        0 >= 0
      SCCS (0):
       
       
    
    SCC (1):
     Strict:
      {int_list# .(x, y) -> int_list# y}
     Weak:
     {   int(0(), 0()) -> .(0(), nil()),
         int(0(), s y) -> .(0(), int(s 0(), s y)),
         int(s x, 0()) -> nil(),
         int(s x, s y) -> int_list int(x, y),
      int_list .(x, y) -> .(s x, int_list y),
        int_list nil() -> nil()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [.](x0, x1) = x0 + 1,
       
       [int](x0, x1) = x0 + 1,
       
       [s](x0) = 0,
       
       [int_list](x0) = x0 + 1,
       
       [0] = 1,
       
       [nil] = 0,
       
       [int_list#](x0) = x0
      Strict:
       int_list# .(x, y) -> int_list# y
       1 + 1y + 0x >= 0 + 1y
      Weak:
       int_list nil() -> nil()
       1 >= 0
       int_list .(x, y) -> .(s x, int_list y)
       2 + 1y + 0x >= 2 + 1y + 0x
       int(s x, s y) -> int_list int(x, y)
       1 + 0y + 0x >= 2 + 0y + 1x
       int(s x, 0()) -> nil()
       1 + 0x >= 0
       int(0(), s y) -> .(0(), int(s 0(), s y))
       2 + 0y >= 2 + 0y
       int(0(), 0()) -> .(0(), nil())
       2 >= 1
     Qed