Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/secret3)

The rewrite relation of the following TRS is considered.

app(nil,k) → k (1)
app(l,nil) → l (2)
app(cons(x,l),k) → cons(x,app(l,k)) (3)
sum(cons(x,nil)) → cons(x,nil) (4)
sum(cons(x,cons(y,l))) → sum(cons(a(x,y,h),l)) (5)
a(h,h,x) → s(x) (6)
a(x,s(y),h) → a(x,y,s(h)) (7)
a(x,s(y),s(z)) → a(x,y,a(x,s(y),z)) (8)
a(s(x),h,z) → a(x,z,z) (9)

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(s) = 0 status(s) = [1] list-extension(s) = Lex
prec(a) = 1 status(a) = [1, 2, 3] list-extension(a) = Lex
prec(h) = 0 status(h) = [] list-extension(h) = Lex
prec(sum) = 3 status(sum) = [1] list-extension(sum) = Lex
prec(cons) = 2 status(cons) = [2, 1] list-extension(cons) = Lex
prec(app) = 3 status(app) = [2, 1] list-extension(app) = Lex
prec(nil) = 0 status(nil) = [] list-extension(nil) = Lex
and the following Max-polynomial interpretation
[s(x1)] = max(0, 0 + 1 · x1)
[a(x1, x2, x3)] = max(0, 0 + 1 · x1, 0 + 1 · x2, 0 + 1 · x3)
[h] = max(0)
[sum(x1)] = max(0, 0 + 1 · x1)
[cons(x1, x2)] = max(0, 0 + 1 · x1, 0 + 1 · x2)
[app(x1, x2)] = max(0, 0 + 1 · x1, 5 + 1 · x2)
[nil] = max(0)
all of the following rules can be deleted.
app(nil,k) → k (1)
app(l,nil) → l (2)
app(cons(x,l),k) → cons(x,app(l,k)) (3)
sum(cons(x,nil)) → cons(x,nil) (4)
sum(cons(x,cons(y,l))) → sum(cons(a(x,y,h),l)) (5)
a(h,h,x) → s(x) (6)
a(x,s(y),h) → a(x,y,s(h)) (7)
a(x,s(y),s(z)) → a(x,y,a(x,s(y),z)) (8)
a(s(x),h,z) → a(x,z,z) (9)

1.1 R is empty

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