Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec4_2_DLMMU04_FR)

The rewrite relation of the following TRS is considered.

natsFrom(N) → cons(N,n__natsFrom(n__s(N))) (1)
fst(pair(XS,YS)) → XS (2)
snd(pair(XS,YS)) → YS (3)
splitAt(0,XS) → pair(nil,XS) (4)
splitAt(s(N),cons(X,XS)) → u(splitAt(N,activate(XS)),N,X,activate(XS)) (5)
u(pair(YS,ZS),N,X,XS) → pair(cons(activate(X),YS),ZS) (6)
head(cons(N,XS)) → N (7)
tail(cons(N,XS)) → activate(XS) (8)
sel(N,XS) → head(afterNth(N,XS)) (9)
take(N,XS) → fst(splitAt(N,XS)) (10)
afterNth(N,XS) → snd(splitAt(N,XS)) (11)
natsFrom(X) → n__natsFrom(X) (12)
s(X) → n__s(X) (13)
activate(n__natsFrom(X)) → natsFrom(activate(X)) (14)
activate(n__s(X)) → s(activate(X)) (15)
activate(X) → X (16)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the Weighted Path Order with the following precedence and status
prec(take) = 1 status(take) = [1, 2] list-extension(take) = Lex
prec(afterNth) = 0 status(afterNth) = [2, 1] list-extension(afterNth) = Lex
prec(sel) = 0 status(sel) = [1, 2] list-extension(sel) = Lex
prec(tail) = 10 status(tail) = [1] list-extension(tail) = Lex
prec(head) = 0 status(head) = [1] list-extension(head) = Lex
prec(u) = 20 status(u) = [1, 2, 3, 4] list-extension(u) = Lex
prec(activate) = 9 status(activate) = [1] list-extension(activate) = Lex
prec(s) = 8 status(s) = [1] list-extension(s) = Lex
prec(nil) = 0 status(nil) = [] list-extension(nil) = Lex
prec(splitAt) = 21 status(splitAt) = [1, 2] list-extension(splitAt) = Lex
prec(0) = 0 status(0) = [] list-extension(0) = Lex
prec(snd) = 0 status(snd) = [1] list-extension(snd) = Lex
prec(fst) = 0 status(fst) = [1] list-extension(fst) = Lex
prec(pair) = 0 status(pair) = [1, 2] list-extension(pair) = Lex
prec(cons) = 0 status(cons) = [2, 1] list-extension(cons) = Lex
prec(n__natsFrom) = 0 status(n__natsFrom) = [1] list-extension(n__natsFrom) = Lex
prec(n__s) = 0 status(n__s) = [1] list-extension(n__s) = Lex
prec(natsFrom) = 8 status(natsFrom) = [1] list-extension(natsFrom) = Lex
and the following Max-polynomial interpretation
[take(x1, x2)] = max(2, 4 + 1 · x1, 5 + 1 · x2)
[afterNth(x1, x2)] = max(4, 4 + 1 · x1, 4 + 1 · x2)
[sel(x1, x2)] = 5 + 1 · x1 + 1 · x2
[tail(x1)] = max(0, 0 + 1 · x1)
[head(x1)] = max(0, 0 + 1 · x1)
[u(x1,...,x4)] = max(0, 0 + 1 · x1, 0 + 1 · x2, 0 + 1 · x3, 0 + 1 · x4)
[activate(x1)] = max(0, 0 + 1 · x1)
[s(x1)] = max(0, 0 + 1 · x1)
[nil] = 0
[splitAt(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[0] = max(7)
[snd(x1)] = 3 + 1 · x1
[fst(x1)] = 4 + 1 · x1
[pair(x1, x2)] = max(2, 0 + 1 · x1, 0 + 1 · x2)
[cons(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[n__natsFrom(x1)] = max(0, 0 + 1 · x1)
[n__s(x1)] = 0 + 1 · x1
[natsFrom(x1)] = max(0, 0 + 1 · x1)
all of the following rules can be deleted.
natsFrom(N) → cons(N,n__natsFrom(n__s(N))) (1)
fst(pair(XS,YS)) → XS (2)
snd(pair(XS,YS)) → YS (3)
splitAt(0,XS) → pair(nil,XS) (4)
splitAt(s(N),cons(X,XS)) → u(splitAt(N,activate(XS)),N,X,activate(XS)) (5)
u(pair(YS,ZS),N,X,XS) → pair(cons(activate(X),YS),ZS) (6)
head(cons(N,XS)) → N (7)
tail(cons(N,XS)) → activate(XS) (8)
sel(N,XS) → head(afterNth(N,XS)) (9)
take(N,XS) → fst(splitAt(N,XS)) (10)
afterNth(N,XS) → snd(splitAt(N,XS)) (11)
natsFrom(X) → n__natsFrom(X) (12)
s(X) → n__s(X) (13)
activate(n__natsFrom(X)) → natsFrom(activate(X)) (14)
activate(n__s(X)) → s(activate(X)) (15)
activate(X) → X (16)

1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.