(VAR M N X Y )
(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)))
        
)