YES
Time: 0.011522
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))}
   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:
       
     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))}
    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 (1):
       Scc:
        {          rm#(N, add(M, X)) -> ifrm#(eq(N, M), N, add(M, X)),
         ifrm#(true(), N, add(M, X)) -> rm#(N, X)}
       SCC (2):
        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 (0):
           
           Qed
   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))}
    SPSC:
     Simple Projection:
      pi(eq#) = 1
     Strict:
      {}
     Qed