Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds-noand_Z)

The rewrite relation of the following TRS is considered.

__(__(X,Y),Z) → __(X,__(Y,Z)) (1)
__(X,nil) → X (2)
__(nil,X) → X (3)
U11(tt) → tt (4)
U21(tt,V2) → U22(isList(activate(V2))) (5)
U22(tt) → tt (6)
U31(tt) → tt (7)
U41(tt,V2) → U42(isNeList(activate(V2))) (8)
U42(tt) → tt (9)
U51(tt,V2) → U52(isList(activate(V2))) (10)
U52(tt) → tt (11)
U61(tt) → tt (12)
U71(tt,P) → U72(isPal(activate(P))) (13)
U72(tt) → tt (14)
U81(tt) → tt (15)
isList(V) → U11(isNeList(activate(V))) (16)
isList(n__nil) → tt (17)
isList(n____(V1,V2)) → U21(isList(activate(V1)),activate(V2)) (18)
isNeList(V) → U31(isQid(activate(V))) (19)
isNeList(n____(V1,V2)) → U41(isList(activate(V1)),activate(V2)) (20)
isNeList(n____(V1,V2)) → U51(isNeList(activate(V1)),activate(V2)) (21)
isNePal(V) → U61(isQid(activate(V))) (22)
isNePal(n____(I,__(P,I))) → U71(isQid(activate(I)),activate(P)) (23)
isPal(V) → U81(isNePal(activate(V))) (24)
isPal(n__nil) → tt (25)
isQid(n__a) → tt (26)
isQid(n__e) → tt (27)
isQid(n__i) → tt (28)
isQid(n__o) → tt (29)
isQid(n__u) → tt (30)
nil → n__nil (31)
__(X1,X2) → n____(X1,X2) (32)
a → n__a (33)
e → n__e (34)
i → n__i (35)
o → n__o (36)
u → n__u (37)
activate(n__nil) → nil (38)
activate(n____(X1,X2)) → __(X1,X2) (39)
activate(n__a) → a (40)
activate(n__e) → e (41)
activate(n__i) → i (42)
activate(n__o) → o (43)
activate(n__u) → u (44)
activate(X) → X (45)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(nil) = 6 weight(nil) = 5
prec(tt) = 32 weight(tt) = 11
prec(n__nil) = 8 weight(n__nil) = 4
prec(n__a) = 25 weight(n__a) = 11
prec(n__e) = 30 weight(n__e) = 11
prec(n__i) = 1 weight(n__i) = 11
prec(n__o) = 7 weight(n__o) = 11
prec(n__u) = 9 weight(n__u) = 11
prec(a) = 15 weight(a) = 13
prec(e) = 16 weight(e) = 12
prec(i) = 17 weight(i) = 12
prec(o) = 27 weight(o) = 12
prec(u) = 28 weight(u) = 12
prec(U11) = 5 weight(U11) = 1
prec(U22) = 10 weight(U22) = 1
prec(isList) = 26 weight(isList) = 9
prec(activate) = 31 weight(activate) = 2
prec(U31) = 20 weight(U31) = 1
prec(U42) = 12 weight(U42) = 1
prec(isNeList) = 29 weight(isNeList) = 5
prec(U52) = 13 weight(U52) = 3
prec(U61) = 0 weight(U61) = 1
prec(U72) = 4 weight(U72) = 18
prec(isPal) = 21 weight(isPal) = 8
prec(U81) = 18 weight(U81) = 1
prec(isQid) = 23 weight(isQid) = 1
prec(isNePal) = 24 weight(isNePal) = 5
prec(__) = 3 weight(__) = 9
prec(U21) = 2 weight(U21) = 3
prec(U41) = 11 weight(U41) = 0
prec(U51) = 19 weight(U51) = 3
prec(U71) = 14 weight(U71) = 18
prec(n____) = 22 weight(n____) = 8
all of the following rules can be deleted.
__(__(X,Y),Z) → __(X,__(Y,Z)) (1)
__(X,nil) → X (2)
__(nil,X) → X (3)
U11(tt) → tt (4)
U21(tt,V2) → U22(isList(activate(V2))) (5)
U22(tt) → tt (6)
U31(tt) → tt (7)
U41(tt,V2) → U42(isNeList(activate(V2))) (8)
U42(tt) → tt (9)
U51(tt,V2) → U52(isList(activate(V2))) (10)
U52(tt) → tt (11)
U61(tt) → tt (12)
U71(tt,P) → U72(isPal(activate(P))) (13)
U72(tt) → tt (14)
U81(tt) → tt (15)
isList(V) → U11(isNeList(activate(V))) (16)
isList(n__nil) → tt (17)
isList(n____(V1,V2)) → U21(isList(activate(V1)),activate(V2)) (18)
isNeList(V) → U31(isQid(activate(V))) (19)
isNeList(n____(V1,V2)) → U41(isList(activate(V1)),activate(V2)) (20)
isNeList(n____(V1,V2)) → U51(isNeList(activate(V1)),activate(V2)) (21)
isNePal(V) → U61(isQid(activate(V))) (22)
isNePal(n____(I,__(P,I))) → U71(isQid(activate(I)),activate(P)) (23)
isPal(V) → U81(isNePal(activate(V))) (24)
isPal(n__nil) → tt (25)
isQid(n__a) → tt (26)
isQid(n__e) → tt (27)
isQid(n__i) → tt (28)
isQid(n__o) → tt (29)
isQid(n__u) → tt (30)
nil → n__nil (31)
__(X1,X2) → n____(X1,X2) (32)
a → n__a (33)
e → n__e (34)
i → n__i (35)
o → n__o (36)
u → n__u (37)
activate(n__nil) → nil (38)
activate(n____(X1,X2)) → __(X1,X2) (39)
activate(n__a) → a (40)
activate(n__e) → e (41)
activate(n__i) → i (42)
activate(n__o) → o (43)
activate(n__u) → u (44)
activate(X) → X (45)

1.1 R is empty

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