YES
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:
  Strict:
   {             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))}
  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)))}
  EDG:
   {(ifrm#(false(), N, add(M, X)) -> rm#(N, X), 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)) -> eq#(N, M))
    (purge#(add(N, X)) -> purge#(rm(N, X)), purge#(add(N, X)) -> purge#(rm(N, X)))
    (purge#(add(N, X)) -> purge#(rm(N, X)), purge#(add(N, X)) -> rm#(N, X))
    (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))
    (purge#(add(N, 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)))
    (ifrm#(true(), N, add(M, X)) -> rm#(N, X), rm#(N, add(M, X)) -> eq#(N, M))
    (ifrm#(true(), N, add(M, X)) -> rm#(N, X), rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)))}
   SCCS:
    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:
     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:
      Argument Filtering:
       pi(purge#) = 0, pi(purge) = [], pi(add) = [1], pi(ifrm) = 2, pi(rm) = 1, pi(nil) = [], pi(s) = [], pi(false) = [], pi(0) = [], pi(eq) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [add](x0) = x0 + 1
      Strict:
       {}
      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)))}
      Qed
    SCC:
     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)))}
     SPSC:
      Simple Projection:
       pi(ifrm#) = 2, pi(rm#) = 1
      Strict:
       {          rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)),
        ifrm#(true(), N, add(M, X)) -> rm#(N, X)}
      EDG:
       {(rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)), ifrm#(true(), N, add(M, X)) -> rm#(N, X))
        (ifrm#(true(), N, add(M, X)) -> rm#(N, X), rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)))}
       SCCS:
        Scc:
         {          rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)),
          ifrm#(true(), N, add(M, X)) -> rm#(N, X)}
        SCC:
         Strict:
          {          rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)),
           ifrm#(true(), 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)))}
         SPSC:
          Simple Projection:
           pi(ifrm#) = 2, pi(rm#) = 1
          Strict:
           {rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X))}
          EDG:
           {}
           SCCS:
            
            Qed
    SCC:
     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)))}
     SPSC:
      Simple Projection:
       pi(eq#) = 0
      Strict:
       {}
      Qed