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 AProVE @ termCOMP 2023)

1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions
prec(nil) = 5 weight(nil) = 2
prec(tt) = 0 weight(tt) = 2
prec(n__nil) = 1 weight(n__nil) = 2
prec(n__a) = 9 weight(n__a) = 1
prec(n__e) = 12 weight(n__e) = 1
prec(n__i) = 13 weight(n__i) = 1
prec(n__o) = 14 weight(n__o) = 1
prec(n__u) = 10 weight(n__u) = 2
prec(a) = 15 weight(a) = 1
prec(e) = 16 weight(e) = 1
prec(i) = 21 weight(i) = 1
prec(o) = 22 weight(o) = 1
prec(u) = 23 weight(u) = 2
prec(activate) = 24 weight(activate) = 0
prec(isList) = 20 weight(isList) = 1
prec(isNeList) = 4 weight(isNeList) = 1
prec(n__isList) = 17 weight(n__isList) = 1
prec(isQid) = 2 weight(isQid) = 1
prec(n__isNeList) = 3 weight(n__isNeList) = 1
prec(isNePal) = 6 weight(isNePal) = 1
prec(n__isPal) = 7 weight(n__isPal) = 1
prec(isPal) = 8 weight(isPal) = 1
prec(__) = 18 weight(__) = 2
prec(and) = 19 weight(and) = 0
prec(n____) = 11 weight(n____) = 2
all of the following rules can be deleted.
__(__(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)

1.1 R is empty

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