YES

Problem:
 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)))

Proof:
 DP Processor:
  DPs:
   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)))
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [purge#](x0) = 6x0 + 6,
    
    [ifrm#](x0, x1, x2) = x1 + 4x2 + 4,
    
    [rm#](x0, x1) = x0 + 6x1 + 1,
    
    [eq#](x0, x1) = 5x1,
    
    [purge](x0) = 4x0 + 2,
    
    [ifrm](x0, x1, x2) = x2,
    
    [add](x0, x1) = 3x0 + 3x1 + 2,
    
    [rm](x0, x1) = x1,
    
    [nil] = 5,
    
    [false] = 0,
    
    [s](x0) = x0 + 3,
    
    [true] = 4,
    
    [eq](x0, x1) = 4x0,
    
    [0] = 1
   orientation:
    eq#(s(X),s(Y)) = 5Y + 15 >= 5Y = eq#(X,Y)
    
    rm#(N,add(M,X)) = 18M + N + 18X + 13 >= 5M = eq#(N,M)
    
    rm#(N,add(M,X)) = 18M + N + 18X + 13 >= 12M + N + 12X + 12 = ifrm#(eq(N,M),N,add(M,X))
    
    ifrm#(true(),N,add(M,X)) = 12M + N + 12X + 12 >= N + 6X + 1 = rm#(N,X)
    
    ifrm#(false(),N,add(M,X)) = 12M + N + 12X + 12 >= N + 6X + 1 = rm#(N,X)
    
    purge#(add(N,X)) = 18N + 18X + 18 >= N + 6X + 1 = rm#(N,X)
    
    purge#(add(N,X)) = 18N + 18X + 18 >= 6X + 6 = purge#(rm(N,X))
    
    eq(0(),0()) = 4 >= 4 = true()
    
    eq(0(),s(X)) = 4 >= 0 = false()
    
    eq(s(X),0()) = 4X + 12 >= 0 = false()
    
    eq(s(X),s(Y)) = 4X + 12 >= 4X = eq(X,Y)
    
    rm(N,nil()) = 5 >= 5 = nil()
    
    rm(N,add(M,X)) = 3M + 3X + 2 >= 3M + 3X + 2 = ifrm(eq(N,M),N,add(M,X))
    
    ifrm(true(),N,add(M,X)) = 3M + 3X + 2 >= X = rm(N,X)
    
    ifrm(false(),N,add(M,X)) = 3M + 3X + 2 >= 3M + 3X + 2 = add(M,rm(N,X))
    
    purge(nil()) = 22 >= 5 = nil()
    
    purge(add(N,X)) = 12N + 12X + 10 >= 3N + 12X + 8 = add(N,purge(rm(N,X)))
   problem:
    DPs:
     
    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)))
   Qed