Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_FR)

The rewrite relation of the following TRS is considered.

__(__(X,Y),Z) → __(X,__(Y,Z)) (1)
__(X,nil) → X (2)
__(nil,X) → X (3)
and(tt,X) → activate(X) (4)
isList(V) → isNeList(activate(V)) (5)
isList(n__nil) → tt (6)
isList(n____(V1,V2)) → and(isList(activate(V1)),n__isList(activate(V2))) (7)
isNeList(V) → isQid(activate(V)) (8)
isNeList(n____(V1,V2)) → and(isList(activate(V1)),n__isNeList(activate(V2))) (9)
isNeList(n____(V1,V2)) → and(isNeList(activate(V1)),n__isList(activate(V2))) (10)
isNePal(V) → isQid(activate(V)) (11)
isNePal(n____(I,n____(P,I))) → and(isQid(activate(I)),n__isPal(activate(P))) (12)
isPal(V) → isNePal(activate(V)) (13)
isPal(n__nil) → tt (14)
isQid(n__a) → tt (15)
isQid(n__e) → tt (16)
isQid(n__i) → tt (17)
isQid(n__o) → tt (18)
isQid(n__u) → tt (19)
nil → n__nil (20)
__(X1,X2) → n____(X1,X2) (21)
isList(X) → n__isList(X) (22)
isNeList(X) → n__isNeList(X) (23)
isPal(X) → n__isPal(X) (24)
a → n__a (25)
e → n__e (26)
i → n__i (27)
o → n__o (28)
u → n__u (29)
activate(n__nil) → nil (30)
activate(n____(X1,X2)) → __(activate(X1),activate(X2)) (31)
activate(n__isList(X)) → isList(X) (32)
activate(n__isNeList(X)) → isNeList(X) (33)
activate(n__isPal(X)) → isPal(X) (34)
activate(n__a) → a (35)
activate(n__e) → e (36)
activate(n__i) → i (37)
activate(n__o) → o (38)
activate(n__u) → u (39)
activate(X) → X (40)

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
[n__o] =
0 0 0
0 0 0
0 0 0
[activate(x1)] =
1 0 0
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[n__a] =
1 0 0
0 0 0
0 0 0
[n____(x1, x2)] =
1 1 1
0 1 0
1 0 1
· x1 +
1 0 0
0 1 0
0 0 1
· x2 +
1 0 0
1 0 0
0 0 0
[nil] =
0 0 0
0 0 0
0 0 0
[and(x1, x2)] =
1 1 0
0 0 0
0 0 0
· x1 +
1 0 0
0 1 1
0 0 1
· x2 +
0 0 0
0 0 0
0 0 0
[n__e] =
0 0 0
0 0 0
0 0 0
[e] =
0 0 0
0 0 0
0 0 0
[n__u] =
0 0 0
0 0 0
0 0 0
[n__i] =
0 0 0
0 0 0
0 0 0
[i] =
0 0 0
0 0 0
0 0 0
[isList(x1)] =
1 1 0
0 0 1
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[isQid(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[__(x1, x2)] =
1 1 1
0 1 0
1 0 1
· x1 +
1 0 0
0 1 0
0 0 1
· x2 +
1 0 0
1 0 0
0 0 0
[n__nil] =
0 0 0
0 0 0
0 0 0
[a] =
1 0 0
0 0 0
0 0 0
[isPal(x1)] =
1 1 0
1 0 0
0 1 0
· x1 +
1 0 0
0 0 0
1 0 0
[isNePal(x1)] =
1 0 0
1 0 0
0 1 0
· x1 +
1 0 0
0 0 0
0 0 0
[o] =
0 0 0
0 0 0
0 0 0
[u] =
0 0 0
0 0 0
0 0 0
[n__isNeList(x1)] =
1 1 0
0 0 1
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[n__isList(x1)] =
1 1 0
0 0 1
0 0 0
· x1 +
1 0 0
1 0 0
0 0 0
[n__isPal(x1)] =
1 1 0
1 0 0
0 1 0
· x1 +
1 0 0
0 0 0
1 0 0
[isNeList(x1)] =
1 1 0
0 0 1
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[tt] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
__(__(X,Y),Z) → __(X,__(Y,Z)) (1)
__(X,nil) → X (2)
__(nil,X) → X (3)
isList(V) → isNeList(activate(V)) (5)
isList(n__nil) → tt (6)
isNePal(V) → isQid(activate(V)) (11)
isNePal(n____(I,n____(P,I))) → and(isQid(activate(I)),n__isPal(activate(P))) (12)
isPal(n__nil) → tt (14)
isQid(n__a) → tt (15)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[n__o] =
1 0 0
0 0 0
0 0 0
[activate(x1)] =
1 0 0
1 1 0
0 0 1
· x1 +
0 0 0
1 0 0
0 0 0
[n__a] =
0 0 0
0 0 0
0 0 0
[n____(x1, x2)] =
1 0 0
1 1 0
0 0 0
· x1 +
1 0 1
1 1 0
0 0 0
· x2 +
1 0 0
1 0 0
0 0 0
[nil] =
0 0 0
1 0 0
0 0 0
[and(x1, x2)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
1 1 1
0 1 1
· x2 +
0 0 0
1 0 0
0 0 0
[n__e] =
0 0 0
0 0 0
0 0 0
[e] =
0 0 0
1 0 0
0 0 0
[n__u] =
0 0 0
0 0 0
0 0 0
[n__i] =
0 0 0
0 0 0
0 0 0
[i] =
0 0 0
0 0 0
0 0 0
[isList(x1)] =
1 1 0
1 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[isQid(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[__(x1, x2)] =
1 0 0
1 1 0
0 0 0
· x1 +
1 0 1
1 1 0
0 0 0
· x2 +
1 0 0
1 0 0
0 0 0
[n__nil] =
0 0 0
0 0 0
0 0 0
[a] =
0 0 0
0 0 0
0 0 0
[isPal(x1)] =
1 1 1
0 1 1
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[isNePal(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[o] =
1 0 0
0 0 0
0 0 0
[u] =
0 0 0
0 0 0
0 0 0
[n__isNeList(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[n__isList(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[n__isPal(x1)] =
1 1 1
0 0 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[isNeList(x1)] =
1 1 0
1 1 0
0 0 0
· x1 +
0 0 0
0 0 0
0 0 0
[tt] =
0 0 0
0 0 0
0 0 0
all of the following rules can be deleted.
isQid(n__o) → tt (18)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals
[n__o] =
0 0 0
0 0 0
0 0 0
[activate(x1)] =
1 0 1
0 1 0
0 0 1
· x1 +
0 0 0
0 0 0
0 0 0
[n__a] =
1 0 0
1 0 0
1 0 0
[n____(x1, x2)] =
1 0 0
0 0 1
0 1 1
· x1 +
1 0 1
0 0 0
0 1 1
· x2 +
0 0 0
1 0 0
1 0 0
[nil] =
1 0 0
0 0 0
1 0 0
[and(x1, x2)] =
1 1 0
0 0 0
0 0 0
· x1 +
1 0 1
0 1 0
0 0 1
· x2 +
1 0 0
0 0 0
0 0 0
[n__e] =
1 0 0
1 0 0
0 0 0
[e] =
1 0 0
1 0 0
0 0 0
[n__u] =
1 0 0
0 0 0
0 0 0
[n__i] =
0 0 0
1 0 0
0 0 0
[i] =
0 0 0
1 0 0
0 0 0
[isList(x1)] =
1 1 1
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[isQid(x1)] =
1 1 0
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[__(x1, x2)] =
1 0 0
0 0 1
0 1 1
· x1 +
1 0 1
0 0 0
0 1 1
· x2 +
0 0 0
1 0 0
1 0 0
[n__nil] =
0 0 0
0 0 0
1 0 0
[a] =
1 0 0
1 0 0
1 0 0
[isPal(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
1 0 0
[isNePal(x1)] =
1 0 0
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
0 0 0
[o] =
0 0 0
0 0 0
0 0 0
[u] =
1 0 0
0 0 0
0 0 0
[n__isNeList(x1)] =
1 1 1
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[n__isList(x1)] =
1 1 1
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[n__isPal(x1)] =
1 0 1
0 0 0
0 0 0
· x1 +
1 0 0
0 0 0
1 0 0
[isNeList(x1)] =
1 1 1
0 0 0
0 0 0
· x1 +
0 0 0
1 0 0
0 0 0
[tt] =
1 0 0
1 0 0
0 0 0
all of the following rules can be deleted.
and(tt,X) → activate(X) (4)
isQid(n__e) → tt (16)
nil → n__nil (20)
activate(n____(X1,X2)) → __(activate(X1),activate(X2)) (31)
activate(n__isPal(X)) → isPal(X) (34)
activate(n__a) → a (35)

1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(u) = 1 weight(u) = 5
prec(o) = 10 weight(o) = 1
prec(i) = 8 weight(i) = 4
prec(e) = 0 weight(e) = 4
prec(a) = 20 weight(a) = 4
prec(n__u) = 4 weight(n__u) = 4
prec(n__o) = 5 weight(n__o) = 1
prec(n__i) = 23 weight(n__i) = 3
prec(n__e) = 16 weight(n__e) = 3
prec(n__a) = 6 weight(n__a) = 2
prec(isPal) = 11 weight(isPal) = 6
prec(n__isPal) = 28 weight(n__isPal) = 1
prec(isNePal) = 24 weight(isNePal) = 4
prec(n__isNeList) = 7 weight(n__isNeList) = 4
prec(isQid) = 19 weight(isQid) = 1
prec(n__isList) = 12 weight(n__isList) = 2
prec(n____) = 17 weight(n____) = 5
prec(n__nil) = 9 weight(n__nil) = 1
prec(isNeList) = 27 weight(isNeList) = 4
prec(isList) = 2 weight(isList) = 3
prec(activate) = 18 weight(activate) = 1
prec(and) = 25 weight(and) = 0
prec(tt) = 14 weight(tt) = 4
prec(nil) = 15 weight(nil) = 1
prec(__) = 3 weight(__) = 6
all of the following rules can be deleted.
isList(n____(V1,V2)) → and(isList(activate(V1)),n__isList(activate(V2))) (7)
isNeList(V) → isQid(activate(V)) (8)
isNeList(n____(V1,V2)) → and(isList(activate(V1)),n__isNeList(activate(V2))) (9)
isNeList(n____(V1,V2)) → and(isNeList(activate(V1)),n__isList(activate(V2))) (10)
isPal(V) → isNePal(activate(V)) (13)
isQid(n__i) → tt (17)
isQid(n__u) → tt (19)
__(X1,X2) → n____(X1,X2) (21)
isList(X) → n__isList(X) (22)
isNeList(X) → n__isNeList(X) (23)
isPal(X) → n__isPal(X) (24)
a → n__a (25)
e → n__e (26)
i → n__i (27)
o → n__o (28)
u → n__u (29)
activate(n__nil) → nil (30)
activate(n__isList(X)) → isList(X) (32)
activate(n__isNeList(X)) → isNeList(X) (33)
activate(n__e) → e (36)
activate(n__i) → i (37)
activate(n__o) → o (38)
activate(n__u) → u (39)
activate(X) → X (40)

1.1.1.1.1 R is empty

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