Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_complete-noand_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)
U11(tt,V) → U12(isPalListKind(activate(V)),activate(V)) (4)
U12(tt,V) → U13(isNeList(activate(V))) (5)
U13(tt) → tt (6)
U21(tt,V1,V2) → U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) (7)
U22(tt,V1,V2) → U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) (8)
U23(tt,V1,V2) → U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) (9)
U24(tt,V1,V2) → U25(isList(activate(V1)),activate(V2)) (10)
U25(tt,V2) → U26(isList(activate(V2))) (11)
U26(tt) → tt (12)
U31(tt,V) → U32(isPalListKind(activate(V)),activate(V)) (13)
U32(tt,V) → U33(isQid(activate(V))) (14)
U33(tt) → tt (15)
U41(tt,V1,V2) → U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) (16)
U42(tt,V1,V2) → U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) (17)
U43(tt,V1,V2) → U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) (18)
U44(tt,V1,V2) → U45(isList(activate(V1)),activate(V2)) (19)
U45(tt,V2) → U46(isNeList(activate(V2))) (20)
U46(tt) → tt (21)
U51(tt,V1,V2) → U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) (22)
U52(tt,V1,V2) → U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) (23)
U53(tt,V1,V2) → U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) (24)
U54(tt,V1,V2) → U55(isNeList(activate(V1)),activate(V2)) (25)
U55(tt,V2) → U56(isList(activate(V2))) (26)
U56(tt) → tt (27)
U61(tt,V) → U62(isPalListKind(activate(V)),activate(V)) (28)
U62(tt,V) → U63(isQid(activate(V))) (29)
U63(tt) → tt (30)
U71(tt,I,P) → U72(isPalListKind(activate(I)),activate(P)) (31)
U72(tt,P) → U73(isPal(activate(P)),activate(P)) (32)
U73(tt,P) → U74(isPalListKind(activate(P))) (33)
U74(tt) → tt (34)
U81(tt,V) → U82(isPalListKind(activate(V)),activate(V)) (35)
U82(tt,V) → U83(isNePal(activate(V))) (36)
U83(tt) → tt (37)
U91(tt,V2) → U92(isPalListKind(activate(V2))) (38)
U92(tt) → tt (39)
isList(V) → U11(isPalListKind(activate(V)),activate(V)) (40)
isList(n__nil) → tt (41)
isList(n____(V1,V2)) → U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) (42)
isNeList(V) → U31(isPalListKind(activate(V)),activate(V)) (43)
isNeList(n____(V1,V2)) → U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) (44)
isNeList(n____(V1,V2)) → U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) (45)
isNePal(V) → U61(isPalListKind(activate(V)),activate(V)) (46)
isNePal(n____(I,n____(P,I))) → U71(isQid(activate(I)),activate(I),activate(P)) (47)
isPal(V) → U81(isPalListKind(activate(V)),activate(V)) (48)
isPal(n__nil) → tt (49)
isPalListKind(n__a) → tt (50)
isPalListKind(n__e) → tt (51)
isPalListKind(n__i) → tt (52)
isPalListKind(n__nil) → tt (53)
isPalListKind(n__o) → tt (54)
isPalListKind(n__u) → tt (55)
isPalListKind(n____(V1,V2)) → U91(isPalListKind(activate(V1)),activate(V2)) (56)
isQid(n__a) → tt (57)
isQid(n__e) → tt (58)
isQid(n__i) → tt (59)
isQid(n__o) → tt (60)
isQid(n__u) → tt (61)
nil → n__nil (62)
__(X1,X2) → n____(X1,X2) (63)
a → n__a (64)
e → n__e (65)
i → n__i (66)
o → n__o (67)
u → n__u (68)
activate(n__nil) → nil (69)
activate(n____(X1,X2)) → __(activate(X1),activate(X2)) (70)
activate(n__a) → a (71)
activate(n__e) → e (72)
activate(n__i) → i (73)
activate(n__o) → o (74)
activate(n__u) → u (75)
activate(X) → X (76)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(__) = 31 stat(__) = lex
prec(nil) = 32 stat(nil) = mul
prec(U11) = 6 stat(U11) = mul
prec(tt) = 13 stat(tt) = mul
prec(U12) = 5 stat(U12) = mul
prec(isNeList) = 4 stat(isNeList) = lex
prec(U21) = 18 stat(U21) = mul
prec(U22) = 17 stat(U22) = mul
prec(U23) = 16 stat(U23) = lex
prec(U24) = 15 stat(U24) = mul
prec(U25) = 14 stat(U25) = mul
prec(isList) = 14 stat(isList) = mul
prec(U31) = 3 stat(U31) = mul
prec(U32) = 2 stat(U32) = mul
prec(U33) = 1 stat(U33) = lex
prec(U41) = 22 stat(U41) = mul
prec(U42) = 21 stat(U42) = mul
prec(U43) = 20 stat(U43) = mul
prec(U44) = 19 stat(U44) = mul
prec(U45) = 7 stat(U45) = mul
prec(U51) = 26 stat(U51) = mul
prec(U52) = 25 stat(U52) = mul
prec(U53) = 24 stat(U53) = mul
prec(U54) = 23 stat(U54) = mul
prec(U55) = 14 stat(U55) = mul
prec(U56) = 0 stat(U56) = mul
prec(U61) = 9 stat(U61) = mul
prec(U62) = 8 stat(U62) = mul
prec(U63) = 0 stat(U63) = mul
prec(U71) = 29 stat(U71) = mul
prec(U72) = 29 stat(U72) = mul
prec(U73) = 13 stat(U73) = mul
prec(isPal) = 29 stat(isPal) = mul
prec(U74) = 10 stat(U74) = lex
prec(U81) = 28 stat(U81) = mul
prec(U82) = 27 stat(U82) = mul
prec(U83) = 11 stat(U83) = lex
prec(isNePal) = 12 stat(isNePal) = lex
prec(U91) = 30 stat(U91) = mul
prec(n__nil) = 32 stat(n__nil) = mul
prec(n____) = 31 stat(n____) = lex
prec(n__a) = 13 stat(n__a) = mul
prec(n__e) = 33 stat(n__e) = mul
prec(n__i) = 34 stat(n__i) = mul
prec(n__o) = 13 stat(n__o) = mul
prec(n__u) = 35 stat(n__u) = mul
prec(a) = 13 stat(a) = mul
prec(e) = 33 stat(e) = mul
prec(i) = 34 stat(i) = mul
prec(o) = 13 stat(o) = mul
prec(u) = 35 stat(u) = mul

π(__) = [1,2]
π(nil) = []
π(U11) = [1,2]
π(tt) = []
π(U12) = [1,2]
π(isPalListKind) = 1
π(activate) = 1
π(U13) = 1
π(isNeList) = [1]
π(U21) = [1,2,3]
π(U22) = [1,2,3]
π(U23) = [1,3,2]
π(U24) = [1,2,3]
π(U25) = [1,2]
π(isList) = [1]
π(U26) = 1
π(U31) = [1,2]
π(U32) = [1,2]
π(U33) = [1]
π(isQid) = 1
π(U41) = [1,2,3]
π(U42) = [1,2,3]
π(U43) = [1,2,3]
π(U44) = [1,2,3]
π(U45) = [1,2]
π(U46) = 1
π(U51) = [1,2,3]
π(U52) = [1,2,3]
π(U53) = [1,2,3]
π(U54) = [1,2,3]
π(U55) = [1,2]
π(U56) = [1]
π(U61) = [1,2]
π(U62) = [1,2]
π(U63) = [1]
π(U71) = [1,2,3]
π(U72) = [1,2]
π(U73) = [1,2]
π(isPal) = [1]
π(U74) = [1]
π(U81) = [1,2]
π(U82) = [1,2]
π(U83) = [1]
π(isNePal) = [1]
π(U91) = [1,2]
π(U92) = 1
π(n__nil) = []
π(n____) = [1,2]
π(n__a) = []
π(n__e) = []
π(n__i) = []
π(n__o) = []
π(n__u) = []
π(a) = []
π(e) = []
π(i) = []
π(o) = []
π(u) = []

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,V) → U12(isPalListKind(activate(V)),activate(V)) (4)
U12(tt,V) → U13(isNeList(activate(V))) (5)
U21(tt,V1,V2) → U22(isPalListKind(activate(V1)),activate(V1),activate(V2)) (7)
U22(tt,V1,V2) → U23(isPalListKind(activate(V2)),activate(V1),activate(V2)) (8)
U23(tt,V1,V2) → U24(isPalListKind(activate(V2)),activate(V1),activate(V2)) (9)
U24(tt,V1,V2) → U25(isList(activate(V1)),activate(V2)) (10)
U25(tt,V2) → U26(isList(activate(V2))) (11)
U31(tt,V) → U32(isPalListKind(activate(V)),activate(V)) (13)
U32(tt,V) → U33(isQid(activate(V))) (14)
U33(tt) → tt (15)
U41(tt,V1,V2) → U42(isPalListKind(activate(V1)),activate(V1),activate(V2)) (16)
U42(tt,V1,V2) → U43(isPalListKind(activate(V2)),activate(V1),activate(V2)) (17)
U43(tt,V1,V2) → U44(isPalListKind(activate(V2)),activate(V1),activate(V2)) (18)
U44(tt,V1,V2) → U45(isList(activate(V1)),activate(V2)) (19)
U45(tt,V2) → U46(isNeList(activate(V2))) (20)
U51(tt,V1,V2) → U52(isPalListKind(activate(V1)),activate(V1),activate(V2)) (22)
U52(tt,V1,V2) → U53(isPalListKind(activate(V2)),activate(V1),activate(V2)) (23)
U53(tt,V1,V2) → U54(isPalListKind(activate(V2)),activate(V1),activate(V2)) (24)
U54(tt,V1,V2) → U55(isNeList(activate(V1)),activate(V2)) (25)
U55(tt,V2) → U56(isList(activate(V2))) (26)
U56(tt) → tt (27)
U61(tt,V) → U62(isPalListKind(activate(V)),activate(V)) (28)
U62(tt,V) → U63(isQid(activate(V))) (29)
U63(tt) → tt (30)
U71(tt,I,P) → U72(isPalListKind(activate(I)),activate(P)) (31)
U72(tt,P) → U73(isPal(activate(P)),activate(P)) (32)
U73(tt,P) → U74(isPalListKind(activate(P))) (33)
U74(tt) → tt (34)
U81(tt,V) → U82(isPalListKind(activate(V)),activate(V)) (35)
U82(tt,V) → U83(isNePal(activate(V))) (36)
U83(tt) → tt (37)
U91(tt,V2) → U92(isPalListKind(activate(V2))) (38)
isList(V) → U11(isPalListKind(activate(V)),activate(V)) (40)
isList(n__nil) → tt (41)
isList(n____(V1,V2)) → U21(isPalListKind(activate(V1)),activate(V1),activate(V2)) (42)
isNeList(V) → U31(isPalListKind(activate(V)),activate(V)) (43)
isNeList(n____(V1,V2)) → U41(isPalListKind(activate(V1)),activate(V1),activate(V2)) (44)
isNeList(n____(V1,V2)) → U51(isPalListKind(activate(V1)),activate(V1),activate(V2)) (45)
isNePal(V) → U61(isPalListKind(activate(V)),activate(V)) (46)
isNePal(n____(I,n____(P,I))) → U71(isQid(activate(I)),activate(I),activate(P)) (47)
isPal(V) → U81(isPalListKind(activate(V)),activate(V)) (48)
isPal(n__nil) → tt (49)
isPalListKind(n__e) → tt (51)
isPalListKind(n__i) → tt (52)
isPalListKind(n__nil) → tt (53)
isPalListKind(n__u) → tt (55)
isPalListKind(n____(V1,V2)) → U91(isPalListKind(activate(V1)),activate(V2)) (56)
isQid(n__e) → tt (58)
isQid(n__i) → tt (59)
isQid(n__u) → tt (61)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(tt) = 0 weight(tt) = 2
prec(n__a) = 18 weight(n__a) = 1
prec(n__o) = 4 weight(n__o) = 1
prec(nil) = 7 weight(nil) = 1
prec(n__nil) = 6 weight(n__nil) = 1
prec(a) = 19 weight(a) = 1
prec(e) = 11 weight(e) = 1
prec(n__e) = 10 weight(n__e) = 1
prec(i) = 14 weight(i) = 1
prec(n__i) = 12 weight(n__i) = 1
prec(o) = 15 weight(o) = 1
prec(u) = 20 weight(u) = 1
prec(n__u) = 16 weight(n__u) = 1
prec(U13) = 17 weight(U13) = 1
prec(U26) = 13 weight(U26) = 1
prec(U46) = 1 weight(U46) = 1
prec(U92) = 2 weight(U92) = 1
prec(isPalListKind) = 3 weight(isPalListKind) = 1
prec(isQid) = 5 weight(isQid) = 1
prec(activate) = 21 weight(activate) = 0
prec(__) = 9 weight(__) = 0
prec(n____) = 8 weight(n____) = 0
all of the following rules can be deleted.
U13(tt) → tt (6)
U26(tt) → tt (12)
U46(tt) → tt (21)
U92(tt) → tt (39)
isPalListKind(n__a) → tt (50)
isPalListKind(n__o) → tt (54)
isQid(n__a) → tt (57)
isQid(n__o) → tt (60)
nil → n__nil (62)
__(X1,X2) → n____(X1,X2) (63)
a → n__a (64)
e → n__e (65)
i → n__i (66)
o → n__o (67)
u → n__u (68)
activate(n__nil) → nil (69)
activate(n____(X1,X2)) → __(activate(X1),activate(X2)) (70)
activate(n__a) → a (71)
activate(n__e) → e (72)
activate(n__i) → i (73)
activate(n__o) → o (74)
activate(n__u) → u (75)
activate(X) → X (76)

1.1.1 R is empty

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