Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM04_GM)

The rewrite relation of the following TRS is considered.

a__nats → a__adx(a__zeros) (1)
a__zeros → cons(0,zeros) (2)
a__incr(cons(X,Y)) → cons(s(X),incr(Y)) (3)
a__adx(cons(X,Y)) → a__incr(cons(X,adx(Y))) (4)
a__hd(cons(X,Y)) → mark(X) (5)
a__tl(cons(X,Y)) → mark(Y) (6)
mark(nats) → a__nats (7)
mark(adx(X)) → a__adx(mark(X)) (8)
mark(zeros) → a__zeros (9)
mark(incr(X)) → a__incr(mark(X)) (10)
mark(hd(X)) → a__hd(mark(X)) (11)
mark(tl(X)) → a__tl(mark(X)) (12)
mark(cons(X1,X2)) → cons(X1,X2) (13)
mark(0) → 0 (14)
mark(s(X)) → s(X) (15)
a__nats → nats (16)
a__adx(X) → adx(X) (17)
a__zeros → zeros (18)
a__incr(X) → incr(X) (19)
a__hd(X) → hd(X) (20)
a__tl(X) → tl(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
[zeros] =
0 0 0
0 0 0
0 0 0
[tl(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
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__zeros] =
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 1
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__hd(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__nats] =
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
[hd(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__tl(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 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[adx(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[nats] =
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
[a__adx(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__nats → a__adx(a__zeros) (1)
a__hd(cons(X,Y)) → mark(X) (5)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[zeros] =
0 0 0
0 0 0
0 0 0
[tl(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 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__zeros] =
0 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[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
[a__hd(x1)] =
1 0 0
0 0 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
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
[hd(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__tl(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[adx(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[nats] =
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[a__adx(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
all of the following rules can be deleted.
a__tl(cons(X,Y)) → mark(Y) (6)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[zeros] =
1 0 0
1 0 0
0 0 0
[tl(x1)] =
1 1 1
0 1 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[incr(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
1 0 0
1 0 0
1 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
1 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
· x2 +
0 0 0
1 0 0
1 0 0
[a__hd(x1)] =
1 1 0
0 1 1
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[a__nats] =
1 0 0
0 0 0
1 0 0
[s(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[hd(x1)] =
1 1 0
0 1 1
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[a__tl(x1)] =
1 1 1
0 1 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[mark(x1)] =
1 1 0
0 1 1
0 0 0
· x1 +
1 0 0
0 0 0
1 0 0
[adx(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[nats] =
1 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__adx(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(nats) → a__nats (7)
mark(zeros) → a__zeros (9)
mark(cons(X1,X2)) → cons(X1,X2) (13)
mark(0) → 0 (14)
mark(s(X)) → s(X) (15)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[zeros] =
1 0 0
0 0 0
0 0 0
[tl(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
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__zeros] =
1 0 0
1 0 0
1 0 0
[0] =
0 0 0
1 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
0 1 0
0 1 0
· x1 +
1 0 0
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[a__hd(x1)] =
1 0 1
0 1 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__nats] =
1 0 0
1 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
[hd(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__tl(x1)] =
1 0 0
0 0 1
0 1 0
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[adx(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
[a__incr(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__adx(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
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 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[zeros] =
0 0 0
0 0 0
0 0 0
[tl(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
1 0 0
1 0 0
0 0 0
[0] =
0 0 0
0 0 0
1 0 0
[cons(x1, x2)] =
1 0 1
1 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
[a__hd(x1)] =
1 0 0
0 1 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
[hd(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__tl(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
1 0 0
1 0 0
[mark(x1)] =
1 0 0
1 1 0
1 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[adx(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__adx(x1)] =
1 0 0
1 1 0
0 0 0
· x1 +
1 0 0
0 0 0
1 0 0
all of the following rules can be deleted.
a__zeros → zeros (18)

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
[zeros] =
0 0 0
0 0 0
0 0 0
[tl(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[incr(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
0 0 0
0 0 0
1 0 0
[0] =
0 0 0
0 0 0
0 0 0
[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
[a__hd(x1)] =
1 0 1
0 1 1
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
[hd(x1)] =
1 0 1
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__tl(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
1 0 0
1 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
[adx(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
0 1 1
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__adx(x1)] =
1 0 0
0 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
mark(tl(X)) → a__tl(mark(X)) (12)

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
[zeros] =
1 0 0
0 0 0
0 0 0
[tl(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
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__zeros] =
1 0 0
0 0 0
0 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 1
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
[a__hd(x1)] =
1 0 0
0 1 0
0 1 0
· x1 +
0 0 0
0 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
[hd(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__tl(x1)] =
1 0 1
0 1 0
1 1 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
[adx(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 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[a__adx(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__tl(X) → tl(X) (21)

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
[zeros] =
0 0 0
0 0 0
0 0 0
[incr(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__zeros] =
1 0 0
0 0 0
1 0 0
[0] =
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 1
0 1 0
0 0 0
· x2 +
0 0 0
0 0 0
1 0 0
[a__hd(x1)] =
1 0 0
0 0 0
0 0 1
· 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
[hd(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[mark(x1)] =
1 0 1
1 0 0
0 0 0
· x1 +
0 0 0
0 0 0
1 0 0
[adx(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
1 0 0
1 0 0
1 0 0
[a__incr(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__adx(x1)] =
1 0 1
0 1 0
0 0 0
· x1 +
1 0 0
1 0 0
1 0 0
all of the following rules can be deleted.
a__zeros → cons(0,zeros) (2)

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
[incr(x1)] =
1 0 0
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[cons(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 1
1 1 0
1 1 0
· x2 +
0 0 0
1 0 0
1 0 0
[a__hd(x1)] =
1 1 0
0 0 1
0 1 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
[hd(x1)] =
1 1 0
0 0 0
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
[adx(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 0
0 1 0
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__adx(x1)] =
1 1 0
0 0 1
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
a__adx(cons(X,Y)) → a__incr(cons(X,adx(Y))) (4)

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(hd) = 0 weight(hd) = 1
prec(mark) = 9 weight(mark) = 2
prec(a__hd) = 1 weight(a__hd) = 1
prec(adx) = 2 weight(adx) = 2
prec(incr) = 3 weight(incr) = 1
prec(s) = 15 weight(s) = 0
prec(a__incr) = 8 weight(a__incr) = 1
prec(cons) = 5 weight(cons) = 0
prec(a__adx) = 7 weight(a__adx) = 2
all of the following rules can be deleted.
a__incr(cons(X,Y)) → cons(s(X),incr(Y)) (3)
mark(adx(X)) → a__adx(mark(X)) (8)
mark(incr(X)) → a__incr(mark(X)) (10)
mark(hd(X)) → a__hd(mark(X)) (11)
a__adx(X) → adx(X) (17)
a__incr(X) → incr(X) (19)
a__hd(X) → hd(X) (20)

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.