Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/secret5)

The rewrite relation of the following TRS is considered.

t(N) → cs(r(q(N)),nt(ns(N))) (1)
q(0) → 0 (2)
q(s(X)) → s(p(q(X),d(X))) (3)
d(0) → 0 (4)
d(s(X)) → s(s(d(X))) (5)
p(0,X) → X (6)
p(X,0) → X (7)
p(s(X),s(Y)) → s(s(p(X,Y))) (8)
f(0,X) → nil (9)
f(s(X),cs(Y,Z)) → cs(Y,nf(X,a(Z))) (10)
t(X) → nt(X) (11)
s(X) → ns(X) (12)
f(X1,X2) → nf(X1,X2) (13)
a(nt(X)) → t(a(X)) (14)
a(ns(X)) → s(a(X)) (15)
a(nf(X1,X2)) → f(a(X1),a(X2)) (16)
a(X) → X (17)

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(nf) = 0 status(nf) = [2, 1] list-extension(nf) = Lex
prec(a) = 12 status(a) = [1] list-extension(a) = Lex
prec(nil) = 0 status(nil) = [] list-extension(nil) = Lex
prec(f) = 1 status(f) = [2, 1] list-extension(f) = Lex
prec(p) = 4 status(p) = [1, 2] list-extension(p) = Lex
prec(d) = 4 status(d) = [1] list-extension(d) = Lex
prec(s) = 1 status(s) = [1] list-extension(s) = Lex
prec(0) = 0 status(0) = [] list-extension(0) = Lex
prec(cs) = 0 status(cs) = [2, 1] list-extension(cs) = Lex
prec(nt) = 0 status(nt) = [1] list-extension(nt) = Lex
prec(ns) = 0 status(ns) = [1] list-extension(ns) = Lex
prec(r) = 0 status(r) = [1] list-extension(r) = Lex
prec(q) = 8 status(q) = [1] list-extension(q) = Lex
prec(t) = 11 status(t) = [1] list-extension(t) = Lex
and the following Max-polynomial interpretation
[nf(x1, x2)] = max(0, 0 + 1 · x1, 1 + 1 · x2)
[a(x1)] = max(0, 0 + 1 · x1)
[nil] = max(1)
[f(x1, x2)] = max(0, 0 + 1 · x1, 1 + 1 · x2)
[p(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[d(x1)] = max(0, 0 + 1 · x1)
[s(x1)] = max(0, 0 + 1 · x1)
[0] = max(0)
[cs(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[nt(x1)] = 0 + 1 · x1
[ns(x1)] = max(0, 0 + 1 · x1)
[r(x1)] = 0 + 1 · x1
[q(x1)] = max(0, 0 + 1 · x1)
[t(x1)] = max(0, 0 + 1 · x1)
all of the following rules can be deleted.
t(N) → cs(r(q(N)),nt(ns(N))) (1)
q(0) → 0 (2)
q(s(X)) → s(p(q(X),d(X))) (3)
d(0) → 0 (4)
d(s(X)) → s(s(d(X))) (5)
p(0,X) → X (6)
p(X,0) → X (7)
p(s(X),s(Y)) → s(s(p(X,Y))) (8)
f(0,X) → nil (9)
f(s(X),cs(Y,Z)) → cs(Y,nf(X,a(Z))) (10)
t(X) → nt(X) (11)
s(X) → ns(X) (12)
f(X1,X2) → nf(X1,X2) (13)
a(nt(X)) → t(a(X)) (14)
a(ns(X)) → s(a(X)) (15)
a(nf(X1,X2)) → f(a(X1),a(X2)) (16)
a(X) → X (17)

1.1 R is empty

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