Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExSec4_2_DLMMU04_Z)

The rewrite relation of the following TRS is considered.

natsFrom(N) → cons(N,n__natsFrom(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)
activate(n__natsFrom(X)) → natsFrom(X) (13)
activate(X) → X (14)

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) = 0 status(take) = [2, 1] list-extension(take) = Lex
prec(afterNth) = 29 status(afterNth) = [1, 2] list-extension(afterNth) = Lex
prec(sel) = 0 status(sel) = [2, 1] list-extension(sel) = Lex
prec(tail) = 17 status(tail) = [1] list-extension(tail) = Lex
prec(head) = 0 status(head) = [1] list-extension(head) = Lex
prec(u) = 24 status(u) = [3, 4, 2, 1] list-extension(u) = Lex
prec(activate) = 16 status(activate) = [1] list-extension(activate) = Lex
prec(nil) = 0 status(nil) = [] list-extension(nil) = Lex
prec(splitAt) = 25 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(s) = 0 status(s) = [1] list-extension(s) = Lex
prec(natsFrom) = 10 status(natsFrom) = [1] list-extension(natsFrom) = Lex
and the following Max-polynomial interpretation
[take(x1, x2)] = max(4, 5 + 1 · x1, 4 + 1 · x2)
[afterNth(x1, x2)] = max(2, 0 + 1 · x1, 2 + 1 · x2)
[sel(x1, x2)] = max(1, 7 + 1 · x1, 4 + 1 · x2)
[tail(x1)] = max(5, 1 + 1 · x1)
[head(x1)] = max(6, 0 + 1 · x1)
[u(x1,...,x4)] = max(0, 0 + 1 · x1, 0 + 1 · x2, 0 + 1 · x3, 0 + 1 · x4)
[activate(x1)] = 0 + 1 · x1
[nil] = max(0)
[splitAt(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[0] = max(1)
[snd(x1)] = max(0, 0 + 1 · x1)
[fst(x1)] = max(0, 3 + 1 · x1)
[pair(x1, x2)] = max(0, 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)
[s(x1)] = max(0, 0 + 1 · x1)
[natsFrom(x1)] = max(0, 0 + 1 · x1)
all of the following rules can be deleted.
natsFrom(N) → cons(N,n__natsFrom(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)
activate(n__natsFrom(X)) → natsFrom(X) (13)
activate(X) → X (14)

1.1 R is empty

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