Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex6_Luc98_Z)

The rewrite relation of the following TRS is considered.

first(0,X) → nil (1)
first(s(X),cons(Y,Z)) → cons(Y,n__first(X,activate(Z))) (2)
from(X) → cons(X,n__from(s(X))) (3)
first(X1,X2) → n__first(X1,X2) (4)
from(X) → n__from(X) (5)
activate(n__first(X1,X2)) → first(X1,X2) (6)
activate(n__from(X)) → from(X) (7)
activate(X) → X (8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[cons(x1, x2)] = 1 · x1 + 1 · x2 + 0
[n__from(x1)] = 2 · x1 + 8
[first(x1, x2)] = 16 · x1 + 18 · x2 + 0
[s(x1)] = 8 · x1 + 4
[activate(x1)] = 9 · x1 + 0
[0] = 0
[from(x1)] = 18 · x1 + 16
[n__first(x1, x2)] = 2 · x1 + 2 · x2 + 0
[nil] = 0
all of the following rules can be deleted.
first(s(X),cons(Y,Z)) → cons(Y,n__first(X,activate(Z))) (2)
from(X) → n__from(X) (5)
activate(n__from(X)) → from(X) (7)

1.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals
[cons(x1, x2)] =
1 0
4 0
· x1 +
1 0
0 0
· x2 +
0 0
0 0
[n__from(x1)] =
1 1
2 2
· x1 +
0 0
0 0
[first(x1, x2)] =
2 0
1 0
· x1 +
1 2
5 1
· x2 +
2 0
4 0
[s(x1)] =
4 6
2 0
· x1 +
2 0
2 0
[activate(x1)] =
2 2
2 1
· x1 +
1 0
0 0
[0] =
3 0
0 0
[from(x1)] =
7 6
4 0
· x1 +
4 0
4 0
[n__first(x1, x2)] =
2 0
0 0
· x1 +
1 2
5 0
· x2 +
0 0
4 0
[nil] =
0 0
7 0
all of the following rules can be deleted.
first(0,X) → nil (1)
first(X1,X2) → n__first(X1,X2) (4)
activate(n__first(X1,X2)) → first(X1,X2) (6)
activate(X) → X (8)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (2 x 2)-matrices with strict dimension 1 over the naturals
[cons(x1, x2)] =
2 1
0 2
· x1 +
4 4
4 0
· x2 +
1 0
4 0
[n__from(x1)] =
1 0
0 0
· x1 +
0 0
1 0
[s(x1)] =
1 0
0 0
· x1 +
0 0
0 0
[from(x1)] =
6 1
4 4
· x1 +
6 0
4 0
all of the following rules can be deleted.
from(X) → cons(X,n__from(s(X))) (3)

1.1.1.1 R is empty

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