YES 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))) max/plus interpretations on N: eq_A(x1,x2) = max{1, 1 + x1, 2 + x2} eq#_A(x1,x2) = max{7, 1, -2 + x2} 0_A = 1 0#_A = 9 true_A = 3 true#_A = 8 s_A(x1) = max{12, 10 + x1} s#_A(x1) = max{1, -1} false_A = 13 false#_A = 0 rm_A(x1,x2) = max{6, 12, x2} rm#_A(x1,x2) = max{2, 4, -5 + x2} nil_A = 13 nil#_A = 0 add_A(x1,x2) = max{20, 11 + x1, 8 + x2} add#_A(x1,x2) = max{9, 8, 7} ifrm_A(x1,x2,x3) = max{13, 7, -1, x3} ifrm#_A(x1,x2,x3) = max{5, -6, 15, -5 + x3} purge_A(x1) = max{8, 1 + x1} purge#_A(x1) = max{17, 10 + x1} precedence: purge > rm > eq = 0 = s = nil = ifrm > true = false = add