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 AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(natsFrom) = 4 stat(natsFrom) = mul
prec(cons) = 0 stat(cons) = mul
prec(n__natsFrom) = 1 stat(n__natsFrom) = mul
prec(s) = 2 stat(s) = mul
prec(fst) = 5 stat(fst) = mul
prec(pair) = 3 stat(pair) = mul
prec(snd) = 6 stat(snd) = mul
prec(splitAt) = 7 stat(splitAt) = lex
prec(0) = 7 stat(0) = mul
prec(nil) = 7 stat(nil) = mul
prec(u) = 4 stat(u) = mul
prec(activate) = 4 stat(activate) = mul
prec(tail) = 4 stat(tail) = mul
prec(sel) = 8 stat(sel) = mul
prec(afterNth) = 8 stat(afterNth) = mul
prec(take) = 9 stat(take) = mul

π(natsFrom) = [1]
π(cons) = [1,2]
π(n__natsFrom) = [1]
π(s) = [1]
π(fst) = [1]
π(pair) = [1,2]
π(snd) = [1]
π(splitAt) = [1,2]
π(0) = []
π(nil) = []
π(u) = [1,2,3,4]
π(activate) = [1]
π(head) = 1
π(tail) = [1]
π(sel) = [1,2]
π(afterNth) = [1,2]
π(take) = [1,2]

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)
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 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(head) = 0 weight(head) = 1
prec(sel) = 1 weight(sel) = 1
prec(afterNth) = 2 weight(afterNth) = 0
all of the following rules can be deleted.
sel(N,XS) → head(afterNth(N,XS)) (9)

1.1.1 R is empty

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