Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_Luc04b_GM)

The rewrite relation of the following TRS is considered.

a__nats → cons(0,incr(nats)) (1)
a__pairs → cons(0,incr(odds)) (2)
a__odds → a__incr(a__pairs) (3)
a__incr(cons(X,XS)) → cons(s(mark(X)),incr(XS)) (4)
a__head(cons(X,XS)) → mark(X) (5)
a__tail(cons(X,XS)) → mark(XS) (6)
mark(nats) → a__nats (7)
mark(incr(X)) → a__incr(mark(X)) (8)
mark(pairs) → a__pairs (9)
mark(odds) → a__odds (10)
mark(head(X)) → a__head(mark(X)) (11)
mark(tail(X)) → a__tail(mark(X)) (12)
mark(cons(X1,X2)) → cons(mark(X1),X2) (13)
mark(0) → 0 (14)
mark(s(X)) → s(mark(X)) (15)
a__nats → nats (16)
a__incr(X) → incr(X) (17)
a__pairs → pairs (18)
a__odds → odds (19)
a__head(X) → head(X) (20)
a__tail(X) → tail(X) (21)

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
[cons(x1, x2)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 0 0
0 1 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[tail(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[a__incr(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__pairs] =
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[a__nats] =
0 0 0
1 0 0
0 0 0
[a__odds] =
0 0 0
1 0 0
0 0 0
[head(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[a__tail(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 0 0
1 0 0
0 0 0
[mark(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[pairs] =
0 0 0
0 0 0
0 0 0
[odds] =
0 0 0
0 0 0
0 0 0
[nats] =
0 0 0
1 0 0
0 0 0
all of the following rules can be deleted.
a__head(cons(X,XS)) → mark(X) (5)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[cons(x1, x2)] =
1 0 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 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__pairs] =
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
0 0 0
0 0 0
0 0 0
[a__odds] =
0 0 0
0 0 0
0 0 0
[head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__tail(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[pairs] =
0 0 0
0 0 0
0 0 0
[odds] =
0 0 0
0 0 0
0 0 0
[nats] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__tail(cons(X,XS)) → mark(XS) (6)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[cons(x1, x2)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 1 0
1 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[tail(x1)] =
1 1 0
1 0 0
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[a__incr(x1)] =
1 1 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 1 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__pairs] =
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
0 0 0
0 0 0
0 0 0
[a__odds] =
0 0 0
0 0 0
0 0 0
[head(x1)] =
1 0 0
0 1 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__tail(x1)] =
1 1 0
1 0 0
0 0 1
· x1 +
1 0 0
1 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 1 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[pairs] =
0 0 0
0 0 0
0 0 0
[odds] =
0 0 0
0 0 0
0 0 0
[nats] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(tail(X)) → a__tail(mark(X)) (12)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[cons(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 1
0 0 0
0 0 0
· 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
[a__incr(x1)] =
1 0 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__pairs] =
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[a__nats] =
0 0 0
1 0 0
0 0 0
[a__odds] =
0 0 0
1 0 0
0 0 0
[head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__tail(x1)] =
1 0 0
1 1 1
0 1 1
· x1 +
1 0 0
1 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[pairs] =
0 0 0
0 0 0
0 0 0
[odds] =
0 0 0
1 0 0
0 0 0
[nats] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__tail(X) → tail(X) (21)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[cons(x1, x2)] =
1 0 0
0 0 1
0 1 1
· x1 +
1 0 0
0 0 0
1 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 1 0
0 0 1
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
1 0 0
0 0 0
[incr(x1)] =
1 0 0
0 0 1
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__pairs] =
0 0 0
0 0 0
1 0 0
[s(x1)] =
1 0 0
0 0 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
0 0 0
1 0 0
1 0 0
[a__odds] =
1 0 0
1 0 0
1 0 0
[head(x1)] =
1 0 0
0 0 0
0 1 1
· x1 +
1 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 1 0
0 0 0
0 1 1
· x1 +
1 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 1
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[pairs] =
0 0 0
0 0 0
1 0 0
[odds] =
0 0 0
1 0 0
1 0 0
[nats] =
0 0 0
1 0 0
1 0 0
all of the following rules can be deleted.
a__odds → a__incr(a__pairs) (3)
mark(nats) → a__nats (7)
mark(pairs) → a__pairs (9)
a__odds → odds (19)

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
[cons(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 1 1
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__pairs] =
1 0 0
1 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
0 0 0
1 0 0
0 0 0
[a__odds] =
0 0 0
0 0 0
0 0 0
[head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 1 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[pairs] =
1 0 0
0 0 0
0 0 0
[odds] =
0 0 0
0 0 0
0 0 0
[nats] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__pairs → cons(0,incr(odds)) (2)

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
[cons(x1, x2)] =
1 0 0
0 0 1
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
0 0 1
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 0
0 0 1
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__pairs] =
1 0 0
1 0 0
1 0 0
[s(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
1 0 0
0 0 0
1 0 0
[a__odds] =
0 0 0
0 0 0
0 0 0
[head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
1 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[pairs] =
0 0 0
0 0 0
0 0 0
[odds] =
0 0 0
0 0 0
0 0 0
[nats] =
1 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__pairs → pairs (18)

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
[cons(x1, x2)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 0 1
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
1 1 0
1 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
1 0 0
1 0 0
1 0 0
[a__odds] =
0 0 0
1 0 0
0 0 0
[head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 1 0
0 1 0
· x1 +
0 0 0
1 0 0
0 0 0
[odds] =
0 0 0
0 0 0
0 0 0
[nats] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__nats → nats (16)

1.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
[cons(x1, x2)] =
1 0 0
0 0 0
0 0 1
· x1 +
1 1 1
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 1
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
0 0 0
1 0 0
1 0 0
[a__odds] =
0 0 0
0 0 0
0 0 0
[head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
1 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[odds] =
1 0 0
0 0 0
1 0 0
[nats] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(odds) → a__odds (10)

1.1.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
[cons(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 1
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
1 0 0
0 0 0
1 0 0
[head(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 0 1
0 0 1
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[nats] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__nats → cons(0,incr(nats)) (1)

1.1.1.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
[cons(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 1 0
0 0 1
0 0 1
· x2 +
0 0 0
1 0 0
1 0 0
[a__incr(x1)] =
1 0 1
0 1 0
0 0 1
· x1 +
0 0 0
1 0 0
1 0 0
[0] =
1 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 1
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
1 0 0
[s(x1)] =
1 0 0
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[a__head(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
1 0 0
[mark(x1)] =
1 0 0
0 1 1
0 0 1
· x1 +
1 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(0) → 0 (14)

1.1.1.1.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
[cons(x1, x2)] =
1 0 0
0 1 0
0 1 0
· x1 +
1 0 0
0 1 1
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 1 1
0 1 0
0 0 1
· x1 +
1 0 0
1 0 0
0 0 0
[incr(x1)] =
1 1 1
0 1 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[s(x1)] =
1 1 0
0 1 0
0 0 0
· x1 +
1 0 0
0 0 0
1 0 0
[head(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 1 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__incr(X) → incr(X) (17)

1.1.1.1.1.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
[cons(x1, x2)] =
1 0 0
0 1 1
0 0 0
· x1 +
1 0 0
0 1 0
1 1 0
· x2 +
0 0 0
1 0 0
1 0 0
[a__incr(x1)] =
1 1 0
0 1 0
1 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 1 0
0 1 0
1 1 1
· x1 +
1 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 0
0 0 0
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[head(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 0 0
1 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(incr(X)) → a__incr(mark(X)) (8)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(head) = 1 weight(head) = 2
prec(a__head) = 2 weight(a__head) = 2
prec(s) = 4 weight(s) = 2
prec(mark) = 7 weight(mark) = 2
prec(a__incr) = 3 weight(a__incr) = 5
prec(cons) = 0 weight(cons) = 0
prec(incr) = 6 weight(incr) = 1
all of the following rules can be deleted.
a__incr(cons(X,XS)) → cons(s(mark(X)),incr(XS)) (4)
mark(head(X)) → a__head(mark(X)) (11)
mark(cons(X1,X2)) → cons(mark(X1),X2) (13)
mark(s(X)) → s(mark(X)) (15)
a__head(X) → head(X) (20)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

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