Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/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(pairs) → a__pairs (8)
mark(odds) → a__odds (9)
mark(incr(X)) → a__incr(mark(X)) (10)
mark(head(X)) → a__head(mark(X)) (11)
mark(tail(X)) → a__tail(mark(X)) (12)
mark(0) → 0 (13)
mark(s(X)) → s(mark(X)) (14)
mark(nil) → nil (15)
mark(cons(X1,X2)) → cons(mark(X1),X2) (16)
a__nats → nats (17)
a__pairs → pairs (18)
a__odds → odds (19)
a__incr(X) → incr(X) (20)
a__head(X) → head(X) (21)
a__tail(X) → tail(X) (22)

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 1
0 0 1
· x1 +
1 0 0
0 0 0
0 0 0
· x2 +
0 0 0
0 0 0
0 0 0
[tail(x1)] =
1 0 1
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
[nil] =
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 1 1
0 1 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
[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 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[cons(x1, x2)] =
1 1 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
[tail(x1)] =
1 1 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__incr(x1)] =
1 0 0
0 1 1
0 1 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 1 1
0 1 1
· x1 +
0 0 0
0 0 0
0 0 0
[nil] =
0 0 0
0 0 0
0 0 0
[a__pairs] =
0 0 0
0 0 0
0 0 0
[s(x1)] =
1 0 1
0 0 0
0 1 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 1 1
· x1 +
1 0 0
0 0 0
0 0 0
[a__tail(x1)] =
1 1 0
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[a__head(x1)] =
1 0 0
0 1 0
0 1 1
· x1 +
1 0 0
0 0 0
0 0 0
[mark(x1)] =
1 1 1
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__head(cons(X,XS)) → mark(X) (5)

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

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

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

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(nil) = 10 weight(nil) = 4
prec(tail) = 2 weight(tail) = 2
prec(head) = 1 weight(head) = 1
prec(pairs) = 14 weight(pairs) = 4
prec(a__tail) = 3 weight(a__tail) = 2
prec(a__head) = 12 weight(a__head) = 1
prec(s) = 0 weight(s) = 4
prec(mark) = 13 weight(mark) = 2
prec(a__incr) = 9 weight(a__incr) = 1
prec(a__odds) = 4 weight(a__odds) = 1
prec(odds) = 7 weight(odds) = 1
prec(a__pairs) = 5 weight(a__pairs) = 6
prec(cons) = 6 weight(cons) = 1
prec(incr) = 8 weight(incr) = 1
prec(0) = 11 weight(0) = 1
all of the following rules can be deleted.
a__pairs → cons(0,incr(odds)) (2)
mark(pairs) → a__pairs (8)
mark(odds) → a__odds (9)
mark(incr(X)) → a__incr(mark(X)) (10)
mark(head(X)) → a__head(mark(X)) (11)
mark(tail(X)) → a__tail(mark(X)) (12)
mark(0) → 0 (13)
mark(s(X)) → s(mark(X)) (14)
mark(nil) → nil (15)
mark(cons(X1,X2)) → cons(mark(X1),X2) (16)
a__pairs → pairs (18)
a__incr(X) → incr(X) (20)
a__head(X) → head(X) (21)
a__tail(X) → tail(X) (22)

1.1.1.1.1.1.1.1 R is empty

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