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)))}
 Fail