YES
  TPA v.1.0

Result: TRS is terminating

Default interpretations for symbols are not printed. For polynomial interpretations
and semantic labelling over N\{0,1} defaults are 2 for constants, identity for unary
symbols and x+y-2 for binary symbols. For semantic labelling over {0,1} (booleans)
defaults are 0 for constants, identity for unary symbols and disjunction for binary symbols.

[1]  TRS loaded from input file:
(1) eq(0,0) -> true
(2) eq(0,s(X)) -> false
(3) eq(s(X),0) -> false
(4) eq(s(X),s(Y)) -> eq(X,Y)
(5) rm(N,nil) -> nil
(6) rm(N,add(M,X)) -> ifrm`1(eq(N,M),ifrm`2(N,add(M,X)))
(7) ifrm`1(true,ifrm`2(N,add(M,X))) -> rm(N,X)
(8) ifrm`1(false,ifrm`2(N,add(M,X))) -> add(M,rm(N,X))
(9) purge(nil) -> nil
(10) purge(add(N,X)) -> add(N,purge(rm(N,X)))

[2]  Apply the Dependency Pair transformation resulting in the following dependency pairs:
<Eq(s(X),s(Y)), Eq(X,Y)>
<Rm(N,add(M,X)), Ifrm`1(eq(N,M),ifrm`2(N,add(M,X)))>
<Rm(N,add(M,X)), Eq(N,M)>
<Ifrm`1(true,ifrm`2(N,add(M,X))), Rm(N,X)>
<Ifrm`1(false,ifrm`2(N,add(M,X))), Rm(N,X)>
<Purge(add(N,X)), Purge(rm(N,X))>
<Purge(add(N,X)), Rm(N,X)>
 and 3 SCCs in the dependency graph. Proofs for those SCCs follow.

[2a-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) eq(0,0) ->= true
(2) eq(0,s(X)) ->= false
(3) eq(s(X),0) ->= false
(4) eq(s(X),s(Y)) ->= eq(X,Y)
(5) rm(N,nil) ->= nil
(6) rm(N,add(M,X)) ->= ifrm`1(eq(N,M),ifrm`2(N,add(M,X)))
(7) ifrm`1(true,ifrm`2(N,add(M,X))) ->= rm(N,X)
(8) ifrm`1(false,ifrm`2(N,add(M,X))) ->= add(M,rm(N,X))
(9) purge(nil) ->= nil
(10) purge(add(N,X)) ->= add(N,purge(rm(N,X)))
(DP6) Purge(add(N,X)) -> Purge(rm(N,X))

[2a-2]  Use following polynomial interpretation:
[rm(x,y)] = y
[add(x,y)] = x + y + 1
[ifrm`1(x,y)] = y
[ifrm`2(x,y)] = y
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(7), (DP6)

[2a-3]  Since there are no remaining strict rules, relative termination is proved!

[2b-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) eq(0,0) ->= true
(2) eq(0,s(X)) ->= false
(3) eq(s(X),0) ->= false
(4) eq(s(X),s(Y)) ->= eq(X,Y)
(5) rm(N,nil) ->= nil
(6) rm(N,add(M,X)) ->= ifrm`1(eq(N,M),ifrm`2(N,add(M,X)))
(7) ifrm`1(true,ifrm`2(N,add(M,X))) ->= rm(N,X)
(8) ifrm`1(false,ifrm`2(N,add(M,X))) ->= add(M,rm(N,X))
(9) purge(nil) ->= nil
(10) purge(add(N,X)) ->= add(N,purge(rm(N,X)))
(DP5) Ifrm`1(false,ifrm`2(N,add(M,X))) -> Rm(N,X)
(DP4) Ifrm`1(true,ifrm`2(N,add(M,X))) -> Rm(N,X)
(DP2) Rm(N,add(M,X)) -> Ifrm`1(eq(N,M),ifrm`2(N,add(M,X)))

[2b-2]  Use following polynomial interpretation:
[eq(x,y)] = 2
[rm(x,y)] = y
[add(x,y)] = x + y + 1
[ifrm`2(x,y)] = y
[Rm(x,y)] = y + 1
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(7), (DP5), (DP4), (DP2)

[2b-3]  Since there are no remaining strict rules, relative termination is proved!

[2c-1]  Consider the following SCC obtained from analysis of dependency graph:
(1) eq(0,0) ->= true
(2) eq(0,s(X)) ->= false
(3) eq(s(X),0) ->= false
(4) eq(s(X),s(Y)) ->= eq(X,Y)
(5) rm(N,nil) ->= nil
(6) rm(N,add(M,X)) ->= ifrm`1(eq(N,M),ifrm`2(N,add(M,X)))
(7) ifrm`1(true,ifrm`2(N,add(M,X))) ->= rm(N,X)
(8) ifrm`1(false,ifrm`2(N,add(M,X))) ->= add(M,rm(N,X))
(9) purge(nil) ->= nil
(10) purge(add(N,X)) ->= add(N,purge(rm(N,X)))
(DP1) Eq(s(X),s(Y)) -> Eq(X,Y)

[2c-2]  Use following polynomial interpretation:
[s(x)] = x + 1
[add(x,y)] = y
[ifrm`1(x,y)] = y
[purge(x)] = 2
rest default

  Remove rules with left hand side strictly bigger than right hand side:
(2)-(4), (DP1)

[2c-3]  Since there are no remaining strict rules, relative termination is proved!



../tpdb/TRS/Rubio/elimdupl.trs, 0., Y
Couldn't open file <60>: 60: No such file or directory