Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex4_7_77_Bor03_iGM)

The rewrite relation of the following TRS is considered.

active(zeros) → mark(cons(0,zeros)) (1)
active(tail(cons(X,XS))) → mark(XS) (2)
mark(zeros) → active(zeros) (3)
mark(cons(X1,X2)) → active(cons(mark(X1),X2)) (4)
mark(0) → active(0) (5)
mark(tail(X)) → active(tail(mark(X))) (6)
cons(mark(X1),X2) → cons(X1,X2) (7)
cons(X1,mark(X2)) → cons(X1,X2) (8)
cons(active(X1),X2) → cons(X1,X2) (9)
cons(X1,active(X2)) → cons(X1,X2) (10)
tail(mark(X)) → tail(X) (11)
tail(active(X)) → tail(X) (12)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[mark(x1)] =
1 1 0
1 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[active(x1)] =
1 0 1
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 1 0
1 1 0
1 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[tail(x1)] =
1 1 0
1 1 0
0 0 0
· x1 +
1 0 0
1 0 0
1 0 0
[zeros] =
0 0 0
0 0 0
1 0 0
[0] =
0 0 0
0 0 0
1 0 0
all of the following rules can be deleted.
active(tail(cons(X,XS))) → mark(XS) (2)
cons(mark(X1),X2) → cons(X1,X2) (7)
cons(X1,mark(X2)) → cons(X1,X2) (8)
tail(mark(X)) → tail(X) (11)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[mark(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[active(x1)] =
1 0 0
0 1 1
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 1 0
0 0 0
0 1 1
· x2 +
0 0 0
0 0 0
0 0 0
[tail(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[zeros] =
0 0 0
0 0 0
1 0 0
[0] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
cons(X1,active(X2)) → cons(X1,X2) (10)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[mark(x1)] =
1 1 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[active(x1)] =
1 1 1
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[cons(x1, x2)] =
1 1 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[tail(x1)] =
1 1 0
1 1 0
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[zeros] =
0 0 0
1 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
active(zeros) → mark(cons(0,zeros)) (1)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[mark(x1)] =
1 0 1
1 1 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[active(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 1 0
1 1 1
1 0 1
· x1 +
1 0 1
1 0 0
1 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[tail(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[zeros] =
1 0 0
1 0 0
1 0 0
[0] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(zeros) → active(zeros) (3)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[mark(x1)] =
1 1 1
0 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[active(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 1 1
0 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
· x2 +
1 0 0
1 0 0
0 0 0
[tail(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 0 0
1 0 0
0 0 0
[0] =
1 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
cons(active(X1),X2) → cons(X1,X2) (9)
tail(active(X)) → tail(X) (12)

1.1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (4 x 4)-matrices with strict dimension 1 over the naturals
[mark(x1)] =
1 0 0 0
0 0 0 0
0 0 0 1
1 1 0 0
· x1 +
1 0 0 0
0 0 0 0
0 0 0 0
1 0 0 0
[active(x1)] =
1 0 0 0
0 0 0 0
0 0 0 0
0 0 0 0
· x1 +
0 0 0 0
0 0 0 0
0 0 0 0
1 0 0 0
[cons(x1, x2)] =
1 1 0 0
1 1 1 0
0 0 0 0
0 1 1 0
· x1 +
1 1 0 0
1 0 0 1
0 0 0 0
0 0 0 0
· x2 +
0 0 0 0
0 0 0 0
0 0 0 0
0 0 0 0
[0] =
0 0 0 0
1 0 0 0
0 0 0 0
1 0 0 0
all of the following rules can be deleted.
mark(0) → active(0) (5)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[mark(x1)] =
1 0 1
0 1 0
1 1 0
· x1 +
0 0 0
0 0 0
1 0 0
[active(x1)] =
1 0 0
0 0 0
1 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 1 0
1 1 1
0 0 1
· x1 +
1 0 0
0 0 1
0 0 1
· x2 +
1 0 0
1 0 0
1 0 0
all of the following rules can be deleted.
mark(cons(X1,X2)) → active(cons(mark(X1),X2)) (4)

1.1.1.1.1.1.1.1.1 R is empty

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