Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_complete_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(isNeList(activate(V))) (4)
U12(tt) → tt (5)
U21(tt,V1,V2) → U22(isList(activate(V1)),activate(V2)) (6)
U22(tt,V2) → U23(isList(activate(V2))) (7)
U23(tt) → tt (8)
U31(tt,V) → U32(isQid(activate(V))) (9)
U32(tt) → tt (10)
U41(tt,V1,V2) → U42(isList(activate(V1)),activate(V2)) (11)
U42(tt,V2) → U43(isNeList(activate(V2))) (12)
U43(tt) → tt (13)
U51(tt,V1,V2) → U52(isNeList(activate(V1)),activate(V2)) (14)
U52(tt,V2) → U53(isList(activate(V2))) (15)
U53(tt) → tt (16)
U61(tt,V) → U62(isQid(activate(V))) (17)
U62(tt) → tt (18)
U71(tt,V) → U72(isNePal(activate(V))) (19)
U72(tt) → tt (20)
and(tt,X) → activate(X) (21)
isList(V) → U11(isPalListKind(activate(V)),activate(V)) (22)
isList(n__nil) → tt (23)
isList(n____(V1,V2)) → U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) (24)
isNeList(V) → U31(isPalListKind(activate(V)),activate(V)) (25)
isNeList(n____(V1,V2)) → U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) (26)
isNeList(n____(V1,V2)) → U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) (27)
isNePal(V) → U61(isPalListKind(activate(V)),activate(V)) (28)
isNePal(n____(I,n____(P,I))) → and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P)))) (29)
isPal(V) → U71(isPalListKind(activate(V)),activate(V)) (30)
isPal(n__nil) → tt (31)
isPalListKind(n__a) → tt (32)
isPalListKind(n__e) → tt (33)
isPalListKind(n__i) → tt (34)
isPalListKind(n__nil) → tt (35)
isPalListKind(n__o) → tt (36)
isPalListKind(n__u) → tt (37)
isPalListKind(n____(V1,V2)) → and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) (38)
isQid(n__a) → tt (39)
isQid(n__e) → tt (40)
isQid(n__i) → tt (41)
isQid(n__o) → tt (42)
isQid(n__u) → tt (43)
nil → n__nil (44)
__(X1,X2) → n____(X1,X2) (45)
isPalListKind(X) → n__isPalListKind(X) (46)
and(X1,X2) → n__and(X1,X2) (47)
isPal(X) → n__isPal(X) (48)
a → n__a (49)
e → n__e (50)
i → n__i (51)
o → n__o (52)
u → n__u (53)
activate(n__nil) → nil (54)
activate(n____(X1,X2)) → __(activate(X1),activate(X2)) (55)
activate(n__isPalListKind(X)) → isPalListKind(X) (56)
activate(n__and(X1,X2)) → and(activate(X1),X2) (57)
activate(n__isPal(X)) → isPal(X) (58)
activate(n__a) → a (59)
activate(n__e) → e (60)
activate(n__i) → i (61)
activate(n__o) → o (62)
activate(n__u) → u (63)
activate(X) → X (64)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(__) = 18 stat(__) = lex
prec(nil) = 19 stat(nil) = mul
prec(U11) = 3 stat(U11) = mul
prec(tt) = 0 stat(tt) = mul
prec(isNeList) = 3 stat(isNeList) = mul
prec(U21) = 8 stat(U21) = lex
prec(U22) = 7 stat(U22) = mul
prec(isList) = 5 stat(isList) = mul
prec(U23) = 6 stat(U23) = mul
prec(U31) = 2 stat(U31) = lex
prec(isQid) = 1 stat(isQid) = mul
prec(U41) = 11 stat(U41) = mul
prec(U42) = 10 stat(U42) = mul
prec(U43) = 9 stat(U43) = mul
prec(U51) = 12 stat(U51) = mul
prec(U52) = 5 stat(U52) = mul
prec(U53) = 4 stat(U53) = mul
prec(U61) = 14 stat(U61) = mul
prec(U62) = 13 stat(U62) = lex
prec(U71) = 15 stat(U71) = mul
prec(isNePal) = 15 stat(isNePal) = mul
prec(and) = 16 stat(and) = mul
prec(n__nil) = 19 stat(n__nil) = mul
prec(n____) = 18 stat(n____) = lex
prec(n__and) = 16 stat(n__and) = mul
prec(n__isPal) = 17 stat(n__isPal) = mul
prec(isPal) = 17 stat(isPal) = mul
prec(n__a) = 20 stat(n__a) = mul
prec(n__e) = 21 stat(n__e) = mul
prec(n__i) = 22 stat(n__i) = mul
prec(n__o) = 23 stat(n__o) = mul
prec(n__u) = 24 stat(n__u) = mul
prec(a) = 20 stat(a) = mul
prec(e) = 21 stat(e) = mul
prec(i) = 22 stat(i) = mul
prec(o) = 23 stat(o) = mul
prec(u) = 24 stat(u) = mul

π(__) = [1,2]
π(nil) = []
π(U11) = [1,2]
π(tt) = []
π(U12) = 1
π(isNeList) = [1]
π(activate) = 1
π(U21) = [3,2,1]
π(U22) = [1,2]
π(isList) = [1]
π(U23) = [1]
π(U31) = [2,1]
π(U32) = 1
π(isQid) = [1]
π(U41) = [1,2,3]
π(U42) = [1,2]
π(U43) = [1]
π(U51) = [1,2,3]
π(U52) = [1,2]
π(U53) = [1]
π(U61) = [1,2]
π(U62) = [1]
π(U71) = [1,2]
π(U72) = 1
π(isNePal) = [1]
π(and) = [1,2]
π(isPalListKind) = 1
π(n__nil) = []
π(n____) = [1,2]
π(n__isPalListKind) = 1
π(n__and) = [1,2]
π(n__isPal) = [1]
π(isPal) = [1]
π(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(isNeList(activate(V))) (4)
U21(tt,V1,V2) → U22(isList(activate(V1)),activate(V2)) (6)
U22(tt,V2) → U23(isList(activate(V2))) (7)
U23(tt) → tt (8)
U31(tt,V) → U32(isQid(activate(V))) (9)
U41(tt,V1,V2) → U42(isList(activate(V1)),activate(V2)) (11)
U42(tt,V2) → U43(isNeList(activate(V2))) (12)
U43(tt) → tt (13)
U51(tt,V1,V2) → U52(isNeList(activate(V1)),activate(V2)) (14)
U52(tt,V2) → U53(isList(activate(V2))) (15)
U53(tt) → tt (16)
U61(tt,V) → U62(isQid(activate(V))) (17)
U62(tt) → tt (18)
U71(tt,V) → U72(isNePal(activate(V))) (19)
and(tt,X) → activate(X) (21)
isList(V) → U11(isPalListKind(activate(V)),activate(V)) (22)
isList(n__nil) → tt (23)
isList(n____(V1,V2)) → U21(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) (24)
isNeList(V) → U31(isPalListKind(activate(V)),activate(V)) (25)
isNeList(n____(V1,V2)) → U41(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) (26)
isNeList(n____(V1,V2)) → U51(and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))),activate(V1),activate(V2)) (27)
isNePal(V) → U61(isPalListKind(activate(V)),activate(V)) (28)
isNePal(n____(I,n____(P,I))) → and(and(isQid(activate(I)),n__isPalListKind(activate(I))),n__and(n__isPal(activate(P)),n__isPalListKind(activate(P)))) (29)
isPal(V) → U71(isPalListKind(activate(V)),activate(V)) (30)
isPal(n__nil) → tt (31)
isPalListKind(n__a) → tt (32)
isPalListKind(n__e) → tt (33)
isPalListKind(n__i) → tt (34)
isPalListKind(n__nil) → tt (35)
isPalListKind(n__o) → tt (36)
isPalListKind(n__u) → tt (37)
isPalListKind(n____(V1,V2)) → and(isPalListKind(activate(V1)),n__isPalListKind(activate(V2))) (38)
isQid(n__a) → tt (39)
isQid(n__e) → tt (40)
isQid(n__i) → tt (41)
isQid(n__o) → tt (42)
isQid(n__u) → tt (43)

1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(tt) = 14 weight(tt) = 1
prec(nil) = 17 weight(nil) = 1
prec(n__nil) = 16 weight(n__nil) = 1
prec(a) = 12 weight(a) = 1
prec(n__a) = 11 weight(n__a) = 1
prec(e) = 6 weight(e) = 1
prec(n__e) = 5 weight(n__e) = 1
prec(i) = 8 weight(i) = 1
prec(n__i) = 7 weight(n__i) = 1
prec(o) = 23 weight(o) = 1
prec(n__o) = 19 weight(n__o) = 1
prec(u) = 21 weight(u) = 2
prec(n__u) = 20 weight(n__u) = 2
prec(U12) = 4 weight(U12) = 1
prec(U32) = 22 weight(U32) = 1
prec(U72) = 3 weight(U72) = 1
prec(isPalListKind) = 15 weight(isPalListKind) = 1
prec(n__isPalListKind) = 13 weight(n__isPalListKind) = 1
prec(isPal) = 10 weight(isPal) = 2
prec(n__isPal) = 0 weight(n__isPal) = 2
prec(activate) = 24 weight(activate) = 0
prec(__) = 18 weight(__) = 0
prec(n____) = 9 weight(n____) = 0
prec(and) = 2 weight(and) = 0
prec(n__and) = 1 weight(n__and) = 0
all of the following rules can be deleted.
U12(tt) → tt (5)
U32(tt) → tt (10)
U72(tt) → tt (20)
nil → n__nil (44)
__(X1,X2) → n____(X1,X2) (45)
isPalListKind(X) → n__isPalListKind(X) (46)
and(X1,X2) → n__and(X1,X2) (47)
isPal(X) → n__isPal(X) (48)
a → n__a (49)
e → n__e (50)
i → n__i (51)
o → n__o (52)
u → n__u (53)
activate(n__nil) → nil (54)
activate(n____(X1,X2)) → __(activate(X1),activate(X2)) (55)
activate(n__isPalListKind(X)) → isPalListKind(X) (56)
activate(n__and(X1,X2)) → and(activate(X1),X2) (57)
activate(n__isPal(X)) → isPal(X) (58)
activate(n__a) → a (59)
activate(n__e) → e (60)
activate(n__i) → i (61)
activate(n__o) → o (62)
activate(n__u) → u (63)
activate(X) → X (64)

1.1.1 R is empty

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