Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_complete_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__U11(tt,V)	→	a__U12(a__isNeList(V))	(4)
a__U12(tt)	→	tt	(5)
a__U21(tt,V1,V2)	→	a__U22(a__isList(V1),V2)	(6)
a__U22(tt,V2)	→	a__U23(a__isList(V2))	(7)
a__U23(tt)	→	tt	(8)
a__U31(tt,V)	→	a__U32(a__isQid(V))	(9)
a__U32(tt)	→	tt	(10)
a__U41(tt,V1,V2)	→	a__U42(a__isList(V1),V2)	(11)
a__U42(tt,V2)	→	a__U43(a__isNeList(V2))	(12)
a__U43(tt)	→	tt	(13)
a__U51(tt,V1,V2)	→	a__U52(a__isNeList(V1),V2)	(14)
a__U52(tt,V2)	→	a__U53(a__isList(V2))	(15)
a__U53(tt)	→	tt	(16)
a__U61(tt,V)	→	a__U62(a__isQid(V))	(17)
a__U62(tt)	→	tt	(18)
a__U71(tt,V)	→	a__U72(a__isNePal(V))	(19)
a__U72(tt)	→	tt	(20)
a__and(tt,X)	→	mark(X)	(21)
a__isList(V)	→	a__U11(a__isPalListKind(V),V)	(22)
a__isList(nil)	→	tt	(23)
a__isList(__(V1,V2))	→	a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(24)
a__isNeList(V)	→	a__U31(a__isPalListKind(V),V)	(25)
a__isNeList(__(V1,V2))	→	a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(26)
a__isNeList(__(V1,V2))	→	a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(27)
a__isNePal(V)	→	a__U61(a__isPalListKind(V),V)	(28)
a__isNePal(__(I,__(P,I)))	→	a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(29)
a__isPal(V)	→	a__U71(a__isPalListKind(V),V)	(30)
a__isPal(nil)	→	tt	(31)
a__isPalListKind(a)	→	tt	(32)
a__isPalListKind(e)	→	tt	(33)
a__isPalListKind(i)	→	tt	(34)
a__isPalListKind(nil)	→	tt	(35)
a__isPalListKind(o)	→	tt	(36)
a__isPalListKind(u)	→	tt	(37)
a__isPalListKind(__(V1,V2))	→	a__and(a__isPalListKind(V1),isPalListKind(V2))	(38)
a__isQid(a)	→	tt	(39)
a__isQid(e)	→	tt	(40)
a__isQid(i)	→	tt	(41)
a__isQid(o)	→	tt	(42)
a__isQid(u)	→	tt	(43)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(44)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(45)
mark(U12(X))	→	a__U12(mark(X))	(46)
mark(isNeList(X))	→	a__isNeList(X)	(47)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(48)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(49)
mark(isList(X))	→	a__isList(X)	(50)
mark(U23(X))	→	a__U23(mark(X))	(51)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(52)
mark(U32(X))	→	a__U32(mark(X))	(53)
mark(isQid(X))	→	a__isQid(X)	(54)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(55)
mark(U42(X1,X2))	→	a__U42(mark(X1),X2)	(56)
mark(U43(X))	→	a__U43(mark(X))	(57)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(58)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(59)
mark(U53(X))	→	a__U53(mark(X))	(60)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(61)
mark(U62(X))	→	a__U62(mark(X))	(62)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(63)
mark(U72(X))	→	a__U72(mark(X))	(64)
mark(isNePal(X))	→	a__isNePal(X)	(65)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(66)
mark(isPalListKind(X))	→	a__isPalListKind(X)	(67)
mark(isPal(X))	→	a__isPal(X)	(68)
mark(nil)	→	nil	(69)
mark(tt)	→	tt	(70)
mark(a)	→	a	(71)
mark(e)	→	e	(72)
mark(i)	→	i	(73)
mark(o)	→	o	(74)
mark(u)	→	u	(75)
a____(X1,X2)	→	__(X1,X2)	(76)
a__U11(X1,X2)	→	U11(X1,X2)	(77)
a__U12(X)	→	U12(X)	(78)
a__isNeList(X)	→	isNeList(X)	(79)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(80)
a__U22(X1,X2)	→	U22(X1,X2)	(81)
a__isList(X)	→	isList(X)	(82)
a__U23(X)	→	U23(X)	(83)
a__U31(X1,X2)	→	U31(X1,X2)	(84)
a__U32(X)	→	U32(X)	(85)
a__isQid(X)	→	isQid(X)	(86)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(87)
a__U42(X1,X2)	→	U42(X1,X2)	(88)
a__U43(X)	→	U43(X)	(89)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(90)
a__U52(X1,X2)	→	U52(X1,X2)	(91)
a__U53(X)	→	U53(X)	(92)
a__U61(X1,X2)	→	U61(X1,X2)	(93)
a__U62(X)	→	U62(X)	(94)
a__U71(X1,X2)	→	U71(X1,X2)	(95)
a__U72(X)	→	U72(X)	(96)
a__isNePal(X)	→	isNePal(X)	(97)
a__and(X1,X2)	→	and(X1,X2)	(98)
a__isPalListKind(X)	→	isPalListKind(X)	(99)
a__isPal(X)	→	isPal(X)	(100)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the

prec(a____)	=	16	stat(a____)	=	lex
prec(__)	=	16	stat(__)	=	lex
prec(nil)	=	18	stat(nil)	=	mul
prec(a__U11)	=	3	stat(a__U11)	=	mul
prec(tt)	=	17	stat(tt)	=	mul
prec(a__isNeList)	=	2	stat(a__isNeList)	=	mul
prec(a__U21)	=	6	stat(a__U21)	=	mul
prec(a__U22)	=	5	stat(a__U22)	=	mul
prec(a__isList)	=	4	stat(a__isList)	=	mul
prec(a__U31)	=	0	stat(a__U31)	=	mul
prec(a__U41)	=	8	stat(a__U41)	=	mul
prec(a__U42)	=	7	stat(a__U42)	=	mul
prec(a__U51)	=	10	stat(a__U51)	=	mul
prec(a__U52)	=	9	stat(a__U52)	=	mul
prec(a__U61)	=	11	stat(a__U61)	=	mul
prec(a__U71)	=	14	stat(a__U71)	=	lex
prec(a__isNePal)	=	13	stat(a__isNePal)	=	mul
prec(a__and)	=	12	stat(a__and)	=	mul
prec(a__isPalListKind)	=	1	stat(a__isPalListKind)	=	mul
prec(isPalListKind)	=	1	stat(isPalListKind)	=	mul
prec(and)	=	12	stat(and)	=	mul
prec(isPal)	=	15	stat(isPal)	=	mul
prec(a__isPal)	=	15	stat(a__isPal)	=	mul
prec(a)	=	19	stat(a)	=	mul
prec(e)	=	20	stat(e)	=	mul
prec(i)	=	17	stat(i)	=	mul
prec(o)	=	21	stat(o)	=	mul
prec(u)	=	22	stat(u)	=	mul
prec(U11)	=	3	stat(U11)	=	mul
prec(isNeList)	=	2	stat(isNeList)	=	mul
prec(U21)	=	6	stat(U21)	=	mul
prec(U22)	=	5	stat(U22)	=	mul
prec(isList)	=	4	stat(isList)	=	mul
prec(U31)	=	0	stat(U31)	=	mul
prec(U41)	=	8	stat(U41)	=	mul
prec(U42)	=	7	stat(U42)	=	mul
prec(U51)	=	10	stat(U51)	=	mul
prec(U52)	=	9	stat(U52)	=	mul
prec(U61)	=	11	stat(U61)	=	mul
prec(U71)	=	14	stat(U71)	=	lex
prec(isNePal)	=	13	stat(isNePal)	=	mul

π(a____)	=	[1,2]
π(__)	=	[1,2]
π(mark)	=	1
π(nil)	=	[]
π(a__U11)	=	[1,2]
π(tt)	=	[]
π(a__U12)	=	1
π(a__isNeList)	=	[1]
π(a__U21)	=	[1,2,3]
π(a__U22)	=	[1,2]
π(a__isList)	=	[1]
π(a__U23)	=	1
π(a__U31)	=	[1,2]
π(a__U32)	=	1
π(a__isQid)	=	1
π(a__U41)	=	[1,2,3]
π(a__U42)	=	[1,2]
π(a__U43)	=	1
π(a__U51)	=	[1,2,3]
π(a__U52)	=	[1,2]
π(a__U53)	=	1
π(a__U61)	=	[1,2]
π(a__U62)	=	1
π(a__U71)	=	[1,2]
π(a__U72)	=	1
π(a__isNePal)	=	[1]
π(a__and)	=	[1,2]
π(a__isPalListKind)	=	[1]
π(isPalListKind)	=	[1]
π(and)	=	[1,2]
π(isPal)	=	[1]
π(a__isPal)	=	[1]
π(a)	=	[]
π(e)	=	[]
π(i)	=	[]
π(o)	=	[]
π(u)	=	[]
π(U11)	=	[1,2]
π(U12)	=	1
π(isNeList)	=	[1]
π(U21)	=	[1,2,3]
π(U22)	=	[1,2]
π(isList)	=	[1]
π(U23)	=	1
π(U31)	=	[1,2]
π(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]

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__U11(tt,V)	→	a__U12(a__isNeList(V))	(4)
a__U21(tt,V1,V2)	→	a__U22(a__isList(V1),V2)	(6)
a__U22(tt,V2)	→	a__U23(a__isList(V2))	(7)
a__U31(tt,V)	→	a__U32(a__isQid(V))	(9)
a__U41(tt,V1,V2)	→	a__U42(a__isList(V1),V2)	(11)
a__U42(tt,V2)	→	a__U43(a__isNeList(V2))	(12)
a__U51(tt,V1,V2)	→	a__U52(a__isNeList(V1),V2)	(14)
a__U52(tt,V2)	→	a__U53(a__isList(V2))	(15)
a__U61(tt,V)	→	a__U62(a__isQid(V))	(17)
a__U71(tt,V)	→	a__U72(a__isNePal(V))	(19)
a__and(tt,X)	→	mark(X)	(21)
a__isList(V)	→	a__U11(a__isPalListKind(V),V)	(22)
a__isList(nil)	→	tt	(23)
a__isList(__(V1,V2))	→	a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(24)
a__isNeList(V)	→	a__U31(a__isPalListKind(V),V)	(25)
a__isNeList(__(V1,V2))	→	a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(26)
a__isNeList(__(V1,V2))	→	a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(27)
a__isNePal(V)	→	a__U61(a__isPalListKind(V),V)	(28)
a__isNePal(__(I,__(P,I)))	→	a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(29)
a__isPal(V)	→	a__U71(a__isPalListKind(V),V)	(30)
a__isPal(nil)	→	tt	(31)
a__isPalListKind(a)	→	tt	(32)
a__isPalListKind(e)	→	tt	(33)
a__isPalListKind(i)	→	tt	(34)
a__isPalListKind(nil)	→	tt	(35)
a__isPalListKind(o)	→	tt	(36)
a__isPalListKind(u)	→	tt	(37)
a__isPalListKind(__(V1,V2))	→	a__and(a__isPalListKind(V1),isPalListKind(V2))	(38)
a__isQid(a)	→	tt	(39)
a__isQid(e)	→	tt	(40)
a__isQid(o)	→	tt	(42)
a__isQid(u)	→	tt	(43)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[a__U12(x₁)]	=	2 + 2 · x₁
[tt]	=	1
[a__U23(x₁)]	=	2 + 2 · x₁
[a__U32(x₁)]	=	2 + 2 · x₁
[a__U43(x₁)]	=	2 + 2 · x₁
[a__U53(x₁)]	=	2 + 2 · x₁
[a__U62(x₁)]	=	2 + 2 · x₁
[a__U72(x₁)]	=	2 + 2 · x₁
[a__isQid(x₁)]	=	2 + 2 · x₁
[i]	=	1
[mark(x₁)]	=	2 · x₁
[__(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a____(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[U11(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U11(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U12(x₁)]	=	1 + 2 · x₁
[isNeList(x₁)]	=	1 + 1 · x₁
[a__isNeList(x₁)]	=	2 + 2 · x₁
[U21(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 1 · x₃
[a__U21(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U22(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[isList(x₁)]	=	1 + 1 · x₁
[a__isList(x₁)]	=	2 + 2 · x₁
[U23(x₁)]	=	1 + 2 · x₁
[U31(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U31(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U32(x₁)]	=	1 + 2 · x₁
[isQid(x₁)]	=	1 + 2 · x₁
[U41(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U41(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U42(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U42(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U43(x₁)]	=	1 + 2 · x₁
[U51(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U51(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U52(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__U52(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U53(x₁)]	=	1 + 2 · x₁
[U61(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U61(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U62(x₁)]	=	1 + 2 · x₁
[U71(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U71(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U72(x₁)]	=	1 + 2 · x₁
[isNePal(x₁)]	=	1 + 1 · x₁
[a__isNePal(x₁)]	=	2 + 2 · x₁
[and(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__and(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[isPalListKind(x₁)]	=	1 + 1 · x₁
[a__isPalListKind(x₁)]	=	2 + 2 · x₁
[isPal(x₁)]	=	1 + 2 · x₁
[a__isPal(x₁)]	=	2 + 2 · x₁
[nil]	=	1
[a]	=	1
[e]	=	1
[o]	=	1
[u]	=	1

all of the following rules can be deleted.

a__U12(tt)	→	tt	(5)
a__U23(tt)	→	tt	(8)
a__U32(tt)	→	tt	(10)
a__U43(tt)	→	tt	(13)
a__U53(tt)	→	tt	(16)
a__U62(tt)	→	tt	(18)
a__U72(tt)	→	tt	(20)
a__isQid(i)	→	tt	(41)
mark(nil)	→	nil	(69)
mark(tt)	→	tt	(70)
mark(a)	→	a	(71)
mark(e)	→	e	(72)
mark(i)	→	i	(73)
mark(o)	→	o	(74)
mark(u)	→	u	(75)
a____(X1,X2)	→	__(X1,X2)	(76)
a__U11(X1,X2)	→	U11(X1,X2)	(77)
a__U12(X)	→	U12(X)	(78)
a__isNeList(X)	→	isNeList(X)	(79)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(80)
a__U22(X1,X2)	→	U22(X1,X2)	(81)
a__isList(X)	→	isList(X)	(82)
a__U23(X)	→	U23(X)	(83)
a__U31(X1,X2)	→	U31(X1,X2)	(84)
a__U32(X)	→	U32(X)	(85)
a__isQid(X)	→	isQid(X)	(86)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(87)
a__U42(X1,X2)	→	U42(X1,X2)	(88)
a__U43(X)	→	U43(X)	(89)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(90)
a__U52(X1,X2)	→	U52(X1,X2)	(91)
a__U53(X)	→	U53(X)	(92)
a__U61(X1,X2)	→	U61(X1,X2)	(93)
a__U62(X)	→	U62(X)	(94)
a__U71(X1,X2)	→	U71(X1,X2)	(95)
a__U72(X)	→	U72(X)	(96)
a__isNePal(X)	→	isNePal(X)	(97)
a__and(X1,X2)	→	and(X1,X2)	(98)
a__isPalListKind(X)	→	isPalListKind(X)	(99)
a__isPal(X)	→	isPal(X)	(100)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[mark(x₁)]	=	2 + 2 · x₁
[__(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a____(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[U11(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[a__U11(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U12(x₁)]	=	2 + 2 · x₁
[a__U12(x₁)]	=	1 + 2 · x₁
[isNeList(x₁)]	=	2 · x₁
[a__isNeList(x₁)]	=	1 + 2 · x₁
[U21(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U21(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	1 + 2 · x₁ + 1 · x₂
[a__U22(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[isList(x₁)]	=	2 · x₁
[a__isList(x₁)]	=	1 + 2 · x₁
[U23(x₁)]	=	1 + 2 · x₁
[a__U23(x₁)]	=	1 + 1 · x₁
[U31(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U31(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U32(x₁)]	=	2 + 2 · x₁
[a__U32(x₁)]	=	1 + 2 · x₁
[isQid(x₁)]	=	1 · x₁
[a__isQid(x₁)]	=	1 + 2 · x₁
[U41(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U41(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₃
[U42(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[a__U42(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U43(x₁)]	=	1 + 2 · x₁
[a__U43(x₁)]	=	1 + 1 · x₁
[U51(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U51(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U52(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U52(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U53(x₁)]	=	2 + 2 · x₁
[a__U53(x₁)]	=	1 + 2 · x₁
[U61(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U61(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U62(x₁)]	=	1 + 2 · x₁
[a__U62(x₁)]	=	1 + 1 · x₁
[U71(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[a__U71(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U72(x₁)]	=	2 + 2 · x₁
[a__U72(x₁)]	=	1 + 2 · x₁
[isNePal(x₁)]	=	1 + 2 · x₁
[a__isNePal(x₁)]	=	2 · x₁
[and(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[a__and(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[isPalListKind(x₁)]	=	1 + 2 · x₁
[a__isPalListKind(x₁)]	=	2 · x₁
[isPal(x₁)]	=	1 · x₁
[a__isPal(x₁)]	=	1 + 2 · x₁

all of the following rules can be deleted.

mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(44)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(45)
mark(U12(X))	→	a__U12(mark(X))	(46)
mark(isNeList(X))	→	a__isNeList(X)	(47)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(48)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(49)
mark(isList(X))	→	a__isList(X)	(50)
mark(U23(X))	→	a__U23(mark(X))	(51)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(52)
mark(U32(X))	→	a__U32(mark(X))	(53)
mark(isQid(X))	→	a__isQid(X)	(54)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(55)
mark(U42(X1,X2))	→	a__U42(mark(X1),X2)	(56)
mark(U43(X))	→	a__U43(mark(X))	(57)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(58)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(59)
mark(U53(X))	→	a__U53(mark(X))	(60)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(61)
mark(U62(X))	→	a__U62(mark(X))	(62)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(63)
mark(U72(X))	→	a__U72(mark(X))	(64)
mark(isNePal(X))	→	a__isNePal(X)	(65)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(66)
mark(isPalListKind(X))	→	a__isPalListKind(X)	(67)
mark(isPal(X))	→	a__isPal(X)	(68)

1.1.1.1 R is empty

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