Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_GM)

The rewrite relation of the following TRS is considered.

a____(__(X,Y),Z) → a____(mark(X),a____(mark(Y),mark(Z))) (1)
a____(X,nil) → mark(X) (2)
a____(nil,X) → mark(X) (3)
a__and(tt,X) → mark(X) (4)
a__isList(V) → a__isNeList(V) (5)
a__isList(nil) → tt (6)
a__isList(__(V1,V2)) → a__and(a__isList(V1),isList(V2)) (7)
a__isNeList(V) → a__isQid(V) (8)
a__isNeList(__(V1,V2)) → a__and(a__isList(V1),isNeList(V2)) (9)
a__isNeList(__(V1,V2)) → a__and(a__isNeList(V1),isList(V2)) (10)
a__isNePal(V) → a__isQid(V) (11)
a__isNePal(__(I,__(P,I))) → a__and(a__isQid(I),isPal(P)) (12)
a__isPal(V) → a__isNePal(V) (13)
a__isPal(nil) → tt (14)
a__isQid(a) → tt (15)
a__isQid(e) → tt (16)
a__isQid(i) → tt (17)
a__isQid(o) → tt (18)
a__isQid(u) → tt (19)
mark(__(X1,X2)) → a____(mark(X1),mark(X2)) (20)
mark(and(X1,X2)) → a__and(mark(X1),X2) (21)
mark(isList(X)) → a__isList(X) (22)
mark(isNeList(X)) → a__isNeList(X) (23)
mark(isQid(X)) → a__isQid(X) (24)
mark(isNePal(X)) → a__isNePal(X) (25)
mark(isPal(X)) → a__isPal(X) (26)
mark(nil) → nil (27)
mark(tt) → tt (28)
mark(a) → a (29)
mark(e) → e (30)
mark(i) → i (31)
mark(o) → o (32)
mark(u) → u (33)
a____(X1,X2) → __(X1,X2) (34)
a__and(X1,X2) → and(X1,X2) (35)
a__isList(X) → isList(X) (36)
a__isNeList(X) → isNeList(X) (37)
a__isQid(X) → isQid(X) (38)
a__isNePal(X) → isNePal(X) (39)
a__isPal(X) → isPal(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) = 19 weight(nil) = 1
prec(tt) = 0 weight(tt) = 3
prec(a) = 20 weight(a) = 2
prec(e) = 7 weight(e) = 2
prec(i) = 14 weight(i) = 2
prec(o) = 15 weight(o) = 2
prec(u) = 16 weight(u) = 2
prec(mark) = 21 weight(mark) = 0
prec(a__isList) = 4 weight(a__isList) = 3
prec(a__isNeList) = 13 weight(a__isNeList) = 2
prec(isList) = 3 weight(isList) = 3
prec(a__isQid) = 9 weight(a__isQid) = 1
prec(isNeList) = 12 weight(isNeList) = 2
prec(a__isNePal) = 11 weight(a__isNePal) = 2
prec(isPal) = 1 weight(isPal) = 9
prec(a__isPal) = 5 weight(a__isPal) = 9
prec(isQid) = 8 weight(isQid) = 1
prec(isNePal) = 10 weight(isNePal) = 2
prec(__) = 2 weight(__) = 4
prec(a____) = 6 weight(a____) = 4
prec(a__and) = 18 weight(a__and) = 0
prec(and) = 17 weight(and) = 0
all of the following rules can be deleted.
a____(__(X,Y),Z) → a____(mark(X),a____(mark(Y),mark(Z))) (1)
a____(X,nil) → mark(X) (2)
a____(nil,X) → mark(X) (3)
a__and(tt,X) → mark(X) (4)
a__isList(V) → a__isNeList(V) (5)
a__isList(nil) → tt (6)
a__isList(__(V1,V2)) → a__and(a__isList(V1),isList(V2)) (7)
a__isNeList(V) → a__isQid(V) (8)
a__isNeList(__(V1,V2)) → a__and(a__isList(V1),isNeList(V2)) (9)
a__isNeList(__(V1,V2)) → a__and(a__isNeList(V1),isList(V2)) (10)
a__isNePal(V) → a__isQid(V) (11)
a__isNePal(__(I,__(P,I))) → a__and(a__isQid(I),isPal(P)) (12)
a__isPal(V) → a__isNePal(V) (13)
a__isPal(nil) → tt (14)
a__isQid(a) → tt (15)
a__isQid(e) → tt (16)
a__isQid(i) → tt (17)
a__isQid(o) → tt (18)
a__isQid(u) → tt (19)
mark(__(X1,X2)) → a____(mark(X1),mark(X2)) (20)
mark(and(X1,X2)) → a__and(mark(X1),X2) (21)
mark(isList(X)) → a__isList(X) (22)
mark(isNeList(X)) → a__isNeList(X) (23)
mark(isQid(X)) → a__isQid(X) (24)
mark(isNePal(X)) → a__isNePal(X) (25)
mark(isPal(X)) → a__isPal(X) (26)
mark(nil) → nil (27)
mark(tt) → tt (28)
mark(a) → a (29)
mark(e) → e (30)
mark(i) → i (31)
mark(o) → o (32)
mark(u) → u (33)
a____(X1,X2) → __(X1,X2) (34)
a__and(X1,X2) → and(X1,X2) (35)
a__isList(X) → isList(X) (36)
a__isNeList(X) → isNeList(X) (37)
a__isQid(X) → isQid(X) (38)
a__isNePal(X) → isNePal(X) (39)
a__isPal(X) → isPal(X) (40)

1.1 R is empty

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