Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex6_9_Luc02c_Z)

The rewrite relation of the following TRS is considered.

2nd(cons1(X,cons(Y,Z))) → Y (1)
2nd(cons(X,X1)) → 2nd(cons1(X,activate(X1))) (2)
from(X) → cons(X,n__from(s(X))) (3)
from(X) → n__from(X) (4)
activate(n__from(X)) → from(X) (5)
activate(X) → X (6)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

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

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[from(x1)] = 7 · x1 + 17
[activate(x1)] = 13 · x1 + 4
[s(x1)] = 1 · x1 + 3
[cons(x1, x2)] = 4 · x1 + 1 · x2 + 0
[n__from(x1)] = 2 · x1 + 10
all of the following rules can be deleted.
from(X) → cons(X,n__from(s(X))) (3)
activate(n__from(X)) → from(X) (5)

1.1.1 R is empty

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