(VAR X Y M N)
(RULES

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