Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex6_Luc98_GM)

The rewrite relation of the following TRS is considered.

a__first(0,X) → nil (1)
a__first(s(X),cons(Y,Z)) → cons(mark(Y),first(X,Z)) (2)
a__from(X) → cons(mark(X),from(s(X))) (3)
mark(first(X1,X2)) → a__first(mark(X1),mark(X2)) (4)
mark(from(X)) → a__from(mark(X)) (5)
mark(0) → 0 (6)
mark(nil) → nil (7)
mark(s(X)) → s(mark(X)) (8)
mark(cons(X1,X2)) → cons(mark(X1),X2) (9)
a__first(X1,X2) → first(X1,X2) (10)
a__from(X) → from(X) (11)

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(from) = 0 status(from) = [1] list-extension(from) = Lex
prec(a__from) = 1 status(a__from) = [1] list-extension(a__from) = Lex
prec(first) = 0 status(first) = [2, 1] list-extension(first) = Lex
prec(mark) = 8 status(mark) = [1] list-extension(mark) = Lex
prec(cons) = 0 status(cons) = [1, 2] list-extension(cons) = Lex
prec(s) = 0 status(s) = [1] list-extension(s) = Lex
prec(nil) = 0 status(nil) = [] list-extension(nil) = Lex
prec(a__first) = 1 status(a__first) = [1, 2] list-extension(a__first) = Lex
prec(0) = 0 status(0) = [] list-extension(0) = Lex
and the following Max-polynomial interpretation
[from(x1)] = max(0, 1 + 1 · x1)
[a__from(x1)] = max(1, 1 + 1 · x1)
[first(x1, x2)] = max(0, 0 + 1 · x1, 7 + 1 · x2)
[mark(x1)] = 0 + 1 · x1
[cons(x1, x2)] = max(1, 0 + 1 · x1, 0 + 1 · x2)
[s(x1)] = max(0, 0 + 1 · x1)
[nil] = max(4)
[a__first(x1, x2)] = max(0, 0 + 1 · x1, 7 + 1 · x2)
[0] = max(0)
all of the following rules can be deleted.
a__first(0,X) → nil (1)
a__first(s(X),cons(Y,Z)) → cons(mark(Y),first(X,Z)) (2)
a__from(X) → cons(mark(X),from(s(X))) (3)
mark(first(X1,X2)) → a__first(mark(X1),mark(X2)) (4)
mark(from(X)) → a__from(mark(X)) (5)
mark(0) → 0 (6)
mark(nil) → nil (7)
mark(s(X)) → s(mark(X)) (8)
mark(cons(X1,X2)) → cons(mark(X1),X2) (9)
a__first(X1,X2) → first(X1,X2) (10)
a__from(X) → from(X) (11)

1.1 R is empty

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