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

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for elimdupl:

-> Dependency pairs:
nF_eq(s(X),s(Y)) -> nF_eq(X,Y)
nF_rm(N,add(M,X)) -> nF_ifrm(eq(N,M),N,add(M,X))
nF_rm(N,add(M,X)) -> nF_eq(N,M)
nF_ifrm(true,N,add(M,X)) -> nF_rm(N,X)
nF_ifrm(false,N,add(M,X)) -> nF_rm(N,X)
nF_purge(add(N,X)) -> nF_purge(rm(N,X))
nF_purge(add(N,X)) -> nF_rm(N,X)

-> Proof of termination for elimdupl_1_1:
-> -> Dependency pairs in cycle:
nF_purge(add(N,X)) -> nF_purge(rm(N,X))

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

Polynomial Interpretation:

[eq](X1,X2) = X1
[0] = 1
[true] = 0
[s](X) = X + 1
[false] = 0
[rm](X1,X2) = X2
[nil] = 0
[add](X1,X2) = X2 + 1
[ifrm](X1,X2,X3) = X3
[purge](X) = 0
[nF_purge](X) = X

TIME: 5.0338e-2


-> Proof of termination for elimdupl_1_2:
-> -> Dependency pairs in cycle:
nF_rm(N,add(M,X)) -> nF_ifrm(eq(N,M),N,add(M,X))
nF_ifrm(false,N,add(M,X)) -> nF_rm(N,X)
nF_ifrm(true,N,add(M,X)) -> nF_rm(N,X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for elimdupl_1_3:
-> -> Dependency pairs in cycle:
nF_eq(s(X),s(Y)) -> nF_eq(X,Y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.