YES
Time: 0.029347
TRS:
 {               eq(0(), 0()) -> true(),
                 eq(0(), s X) -> false(),
                 eq(s X, 0()) -> false(),
                 eq(s X, s Y) -> eq(X, Y),
                 rm(N, nil()) -> nil(),
             rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)),
   ifrm(true(), N, add(M, X)) -> rm(N, X),
  ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)),
                  purge nil() -> nil(),
              purge add(N, X) -> add(N, purge rm(N, X))}
 DP:
  DP:
   {               eq#(s X, s Y) -> eq#(X, Y),
               rm#(N, add(M, X)) -> eq#(N, M),
               rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)),
     ifrm#(true(), N, add(M, X)) -> rm#(N, X),
    ifrm#(false(), N, add(M, X)) -> rm#(N, X),
                purge# add(N, X) -> rm#(N, X),
                purge# add(N, X) -> purge# rm(N, X)}
  TRS:
  {               eq(0(), 0()) -> true(),
                  eq(0(), s X) -> false(),
                  eq(s X, 0()) -> false(),
                  eq(s X, s Y) -> eq(X, Y),
                  rm(N, nil()) -> nil(),
              rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)),
    ifrm(true(), N, add(M, X)) -> rm(N, X),
   ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)),
                   purge nil() -> nil(),
               purge add(N, X) -> add(N, purge rm(N, X))}
  EDG:
   {(ifrm#(true(), N, add(M, X)) -> rm#(N, X), rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)))
    (ifrm#(true(), N, add(M, X)) -> rm#(N, X), rm#(N, add(M, X)) -> eq#(N, M))
    (purge# add(N, X) -> rm#(N, X), rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)))
    (purge# add(N, X) -> rm#(N, X), rm#(N, add(M, X)) -> eq#(N, M))
    (rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)), ifrm#(false(), N, add(M, X)) -> rm#(N, X))
    (rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)), ifrm#(true(), N, add(M, X)) -> rm#(N, X))
    (rm#(N, add(M, X)) -> eq#(N, M), eq#(s X, s Y) -> eq#(X, Y))
    (eq#(s X, s Y) -> eq#(X, Y), eq#(s X, s Y) -> eq#(X, Y))
    (ifrm#(false(), N, add(M, X)) -> rm#(N, X), rm#(N, add(M, X)) -> eq#(N, M))
    (ifrm#(false(), N, add(M, X)) -> rm#(N, X), rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)))
    (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> rm#(N, X))
    (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> purge# rm(N, X))}
   STATUS:
    arrows: 0.755102
    SCCS (3):
     Scc:
      {purge# add(N, X) -> purge# rm(N, X)}
     Scc:
      {           rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)),
        ifrm#(true(), N, add(M, X)) -> rm#(N, X),
       ifrm#(false(), N, add(M, X)) -> rm#(N, X)}
     Scc:
      {eq#(s X, s Y) -> eq#(X, Y)}
     
     SCC (1):
      Strict:
       {purge# add(N, X) -> purge# rm(N, X)}
      Weak:
      {               eq(0(), 0()) -> true(),
                      eq(0(), s X) -> false(),
                      eq(s X, 0()) -> false(),
                      eq(s X, s Y) -> eq(X, Y),
                      rm(N, nil()) -> nil(),
                  rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)),
        ifrm(true(), N, add(M, X)) -> rm(N, X),
       ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)),
                       purge nil() -> nil(),
                   purge add(N, X) -> add(N, purge rm(N, X))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [ifrm](x0, x1, x2) = x0,
        
        [eq](x0, x1) = 0,
        
        [rm](x0, x1) = x0,
        
        [add](x0, x1) = x0 + 1,
        
        [s](x0) = 0,
        
        [purge](x0) = 0,
        
        [true] = 0,
        
        [0] = 0,
        
        [false] = 0,
        
        [nil] = 0,
        
        [purge#](x0) = x0
       Strict:
        purge# add(N, X) -> purge# rm(N, X)
        1 + 1X + 0N >= 0 + 1X + 0N
       Weak:
        purge add(N, X) -> add(N, purge rm(N, X))
        0 + 0X + 0N >= 1 + 0X + 0N
        purge nil() -> nil()
        0 >= 0
        ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
        1 + 1X + 0N + 0M >= 1 + 1X + 0N + 0M
        ifrm(true(), N, add(M, X)) -> rm(N, X)
        1 + 1X + 0N + 0M >= 0 + 1X + 0N
        rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
        1 + 1X + 0N + 0M >= 1 + 1X + 0N + 0M
        rm(N, nil()) -> nil()
        0 + 0N >= 0
        eq(s X, s Y) -> eq(X, Y)
        0 + 0X + 0Y >= 0 + 0X + 0Y
        eq(s X, 0()) -> false()
        0 + 0X >= 0
        eq(0(), s X) -> false()
        0 + 0X >= 0
        eq(0(), 0()) -> true()
        0 >= 0
      Qed
    
    SCC (3):
     Strict:
      {           rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)),
        ifrm#(true(), N, add(M, X)) -> rm#(N, X),
       ifrm#(false(), N, add(M, X)) -> rm#(N, X)}
     Weak:
     {               eq(0(), 0()) -> true(),
                     eq(0(), s X) -> false(),
                     eq(s X, 0()) -> false(),
                     eq(s X, s Y) -> eq(X, Y),
                     rm(N, nil()) -> nil(),
                 rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)),
       ifrm(true(), N, add(M, X)) -> rm(N, X),
      ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)),
                      purge nil() -> nil(),
                  purge add(N, X) -> add(N, purge rm(N, X))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [ifrm](x0, x1, x2) = 0,
       
       [eq](x0, x1) = 0,
       
       [rm](x0, x1) = x0 + 1,
       
       [add](x0, x1) = x0 + 1,
       
       [s](x0) = 0,
       
       [purge](x0) = 0,
       
       [true] = 0,
       
       [0] = 0,
       
       [false] = 0,
       
       [nil] = 1,
       
       [ifrm#](x0, x1, x2) = x0,
       
       [rm#](x0, x1) = x0
      Strict:
       ifrm#(false(), N, add(M, X)) -> rm#(N, X)
       1 + 1X + 0N + 0M >= 0 + 1X + 0N
       ifrm#(true(), N, add(M, X)) -> rm#(N, X)
       1 + 1X + 0N + 0M >= 0 + 1X + 0N
       rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X))
       1 + 1X + 0N + 0M >= 1 + 1X + 0N + 0M
      Weak:
       purge add(N, X) -> add(N, purge rm(N, X))
       0 + 0X + 0N >= 1 + 0X + 0N
       purge nil() -> nil()
       0 >= 1
       ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
       0 + 0X + 0N + 0M >= 2 + 1X + 0N + 0M
       ifrm(true(), N, add(M, X)) -> rm(N, X)
       0 + 0X + 0N + 0M >= 1 + 1X + 0N
       rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
       2 + 1X + 0N + 0M >= 0 + 0X + 0N + 0M
       rm(N, nil()) -> nil()
       2 + 0N >= 1
       eq(s X, s Y) -> eq(X, Y)
       0 + 0X + 0Y >= 0 + 0X + 0Y
       eq(s X, 0()) -> false()
       0 + 0X >= 0
       eq(0(), s X) -> false()
       0 + 0X >= 0
       eq(0(), 0()) -> true()
       0 >= 0
     SCCS (0):
      
      
    
    SCC (1):
     Strict:
      {eq#(s X, s Y) -> eq#(X, Y)}
     Weak:
     {               eq(0(), 0()) -> true(),
                     eq(0(), s X) -> false(),
                     eq(s X, 0()) -> false(),
                     eq(s X, s Y) -> eq(X, Y),
                     rm(N, nil()) -> nil(),
                 rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X)),
       ifrm(true(), N, add(M, X)) -> rm(N, X),
      ifrm(false(), N, add(M, X)) -> add(M, rm(N, X)),
                      purge nil() -> nil(),
                  purge add(N, X) -> add(N, purge rm(N, X))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [ifrm](x0, x1, x2) = 0,
       
       [eq](x0, x1) = x0 + 1,
       
       [rm](x0, x1) = x0 + 1,
       
       [add](x0, x1) = 1,
       
       [s](x0) = x0 + 1,
       
       [purge](x0) = x0 + 1,
       
       [true] = 0,
       
       [0] = 1,
       
       [false] = 0,
       
       [nil] = 1,
       
       [eq#](x0, x1) = x0
      Strict:
       eq#(s X, s Y) -> eq#(X, Y)
       1 + 0X + 1Y >= 0 + 0X + 1Y
      Weak:
       purge add(N, X) -> add(N, purge rm(N, X))
       2 + 0X + 0N >= 1 + 0X + 0N
       purge nil() -> nil()
       2 >= 1
       ifrm(false(), N, add(M, X)) -> add(M, rm(N, X))
       0 + 0X + 0N + 0M >= 1 + 0X + 0N + 0M
       ifrm(true(), N, add(M, X)) -> rm(N, X)
       0 + 0X + 0N + 0M >= 1 + 1X + 0N
       rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
       2 + 0X + 0N + 0M >= 0 + 0X + 0N + 0M
       rm(N, nil()) -> nil()
       2 + 0N >= 1
       eq(s X, s Y) -> eq(X, Y)
       2 + 1X + 0Y >= 1 + 1X + 0Y
       eq(s X, 0()) -> false()
       2 + 1X >= 0
       eq(0(), s X) -> false()
       2 + 0X >= 0
       eq(0(), 0()) -> true()
       2 >= 0
     Qed