Certification Problem

Input (TPDB TRS_Innermost/Transformed_CSR_innermost_04/PALINDROME_complete_noand_GM)

The rewrite relation of the following TRS is considered.

There are 154 ruless (increase limit for explicit display).

The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the

prec(a____)	=	30	stat(a____)	=	lex
prec(__)	=	30	stat(__)	=	lex
prec(nil)	=	14	stat(nil)	=	mul
prec(a__U11)	=	4	stat(a__U11)	=	mul
prec(tt)	=	14	stat(tt)	=	mul
prec(a__U12)	=	3	stat(a__U12)	=	mul
prec(a__isNeList)	=	3	stat(a__isNeList)	=	mul
prec(a__U21)	=	18	stat(a__U21)	=	mul
prec(a__U22)	=	17	stat(a__U22)	=	mul
prec(a__U23)	=	16	stat(a__U23)	=	mul
prec(a__U24)	=	15	stat(a__U24)	=	mul
prec(a__U25)	=	6	stat(a__U25)	=	mul
prec(a__isList)	=	6	stat(a__isList)	=	mul
prec(a__U31)	=	2	stat(a__U31)	=	mul
prec(a__U32)	=	1	stat(a__U32)	=	mul
prec(a__isQid)	=	0	stat(a__isQid)	=	mul
prec(a__U41)	=	24	stat(a__U41)	=	mul
prec(a__U42)	=	23	stat(a__U42)	=	mul
prec(a__U43)	=	22	stat(a__U43)	=	mul
prec(a__U44)	=	21	stat(a__U44)	=	mul
prec(a__U45)	=	20	stat(a__U45)	=	mul
prec(a__U46)	=	19	stat(a__U46)	=	mul
prec(a__U51)	=	27	stat(a__U51)	=	mul
prec(a__U52)	=	26	stat(a__U52)	=	mul
prec(a__U53)	=	25	stat(a__U53)	=	mul
prec(a__U54)	=	14	stat(a__U54)	=	mul
prec(a__U55)	=	6	stat(a__U55)	=	mul
prec(a__U56)	=	5	stat(a__U56)	=	mul
prec(a__U61)	=	7	stat(a__U61)	=	mul
prec(a__U62)	=	0	stat(a__U62)	=	mul
prec(a__U71)	=	28	stat(a__U71)	=	mul
prec(a__U72)	=	13	stat(a__U72)	=	mul
prec(a__U73)	=	8	stat(a__U73)	=	mul
prec(a__isPal)	=	12	stat(a__isPal)	=	mul
prec(a__U81)	=	11	stat(a__U81)	=	mul
prec(a__U82)	=	10	stat(a__U82)	=	mul
prec(a__isNePal)	=	9	stat(a__isNePal)	=	mul
prec(a__U91)	=	29	stat(a__U91)	=	mul
prec(a)	=	31	stat(a)	=	mul
prec(e)	=	32	stat(e)	=	mul
prec(i)	=	33	stat(i)	=	mul
prec(o)	=	14	stat(o)	=	mul
prec(u)	=	34	stat(u)	=	mul
prec(U11)	=	4	stat(U11)	=	mul
prec(U12)	=	3	stat(U12)	=	mul
prec(isNeList)	=	3	stat(isNeList)	=	mul
prec(U21)	=	18	stat(U21)	=	mul
prec(U22)	=	17	stat(U22)	=	mul
prec(U23)	=	16	stat(U23)	=	mul
prec(U24)	=	15	stat(U24)	=	mul
prec(U25)	=	6	stat(U25)	=	mul
prec(isList)	=	6	stat(isList)	=	mul
prec(U31)	=	2	stat(U31)	=	mul
prec(U32)	=	1	stat(U32)	=	mul
prec(isQid)	=	0	stat(isQid)	=	mul
prec(U41)	=	24	stat(U41)	=	mul
prec(U42)	=	23	stat(U42)	=	mul
prec(U43)	=	22	stat(U43)	=	mul
prec(U44)	=	21	stat(U44)	=	mul
prec(U45)	=	20	stat(U45)	=	mul
prec(U46)	=	19	stat(U46)	=	mul
prec(U51)	=	27	stat(U51)	=	mul
prec(U52)	=	26	stat(U52)	=	mul
prec(U53)	=	25	stat(U53)	=	mul
prec(U54)	=	14	stat(U54)	=	mul
prec(U55)	=	6	stat(U55)	=	mul
prec(U56)	=	5	stat(U56)	=	mul
prec(U61)	=	7	stat(U61)	=	mul
prec(U62)	=	0	stat(U62)	=	mul
prec(U71)	=	28	stat(U71)	=	mul
prec(U72)	=	13	stat(U72)	=	mul
prec(U73)	=	8	stat(U73)	=	mul
prec(isPal)	=	12	stat(isPal)	=	mul
prec(U81)	=	11	stat(U81)	=	mul
prec(U82)	=	10	stat(U82)	=	mul
prec(isNePal)	=	9	stat(isNePal)	=	mul
prec(U91)	=	29	stat(U91)	=	mul

π(a____)	=	[1,2]
π(__)	=	[1,2]
π(mark)	=	1
π(nil)	=	[]
π(a__U11)	=	[1,2]
π(tt)	=	[]
π(a__U12)	=	[1,2]
π(a__isPalListKind)	=	1
π(a__U13)	=	1
π(a__isNeList)	=	[1]
π(a__U21)	=	[1,2,3]
π(a__U22)	=	[1,2,3]
π(a__U23)	=	[1,2,3]
π(a__U24)	=	[1,2,3]
π(a__U25)	=	[1,2]
π(a__isList)	=	[1]
π(a__U26)	=	1
π(a__U31)	=	[1,2]
π(a__U32)	=	[1,2]
π(a__U33)	=	1
π(a__isQid)	=	[1]
π(a__U41)	=	[1,2,3]
π(a__U42)	=	[1,2,3]
π(a__U43)	=	[1,2,3]
π(a__U44)	=	[1,2,3]
π(a__U45)	=	[1,2]
π(a__U46)	=	[1]
π(a__U51)	=	[1,2,3]
π(a__U52)	=	[1,2,3]
π(a__U53)	=	[1,2,3]
π(a__U54)	=	[1,2,3]
π(a__U55)	=	[1,2]
π(a__U56)	=	[1]
π(a__U61)	=	[1,2]
π(a__U62)	=	[1,2]
π(a__U63)	=	1
π(a__U71)	=	[1,2,3]
π(a__U72)	=	[1,2]
π(a__U73)	=	[1,2]
π(a__isPal)	=	[1]
π(a__U74)	=	1
π(a__U81)	=	[1,2]
π(a__U82)	=	[1,2]
π(a__U83)	=	1
π(a__isNePal)	=	[1]
π(a__U91)	=	[1,2]
π(a__U92)	=	1
π(a)	=	[]
π(e)	=	[]
π(i)	=	[]
π(o)	=	[]
π(u)	=	[]
π(U11)	=	[1,2]
π(U12)	=	[1,2]
π(isPalListKind)	=	1
π(U13)	=	1
π(isNeList)	=	[1]
π(U21)	=	[1,2,3]
π(U22)	=	[1,2,3]
π(U23)	=	[1,2,3]
π(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

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__isPalListKind(V),V)	(4)
a__U12(tt,V)	→	a__U13(a__isNeList(V))	(5)
a__U21(tt,V1,V2)	→	a__U22(a__isPalListKind(V1),V1,V2)	(7)
a__U22(tt,V1,V2)	→	a__U23(a__isPalListKind(V2),V1,V2)	(8)
a__U23(tt,V1,V2)	→	a__U24(a__isPalListKind(V2),V1,V2)	(9)
a__U24(tt,V1,V2)	→	a__U25(a__isList(V1),V2)	(10)
a__U25(tt,V2)	→	a__U26(a__isList(V2))	(11)
a__U31(tt,V)	→	a__U32(a__isPalListKind(V),V)	(13)
a__U32(tt,V)	→	a__U33(a__isQid(V))	(14)
a__U41(tt,V1,V2)	→	a__U42(a__isPalListKind(V1),V1,V2)	(16)
a__U42(tt,V1,V2)	→	a__U43(a__isPalListKind(V2),V1,V2)	(17)
a__U43(tt,V1,V2)	→	a__U44(a__isPalListKind(V2),V1,V2)	(18)
a__U44(tt,V1,V2)	→	a__U45(a__isList(V1),V2)	(19)
a__U45(tt,V2)	→	a__U46(a__isNeList(V2))	(20)
a__U46(tt)	→	tt	(21)
a__U51(tt,V1,V2)	→	a__U52(a__isPalListKind(V1),V1,V2)	(22)
a__U52(tt,V1,V2)	→	a__U53(a__isPalListKind(V2),V1,V2)	(23)
a__U53(tt,V1,V2)	→	a__U54(a__isPalListKind(V2),V1,V2)	(24)
a__U54(tt,V1,V2)	→	a__U55(a__isNeList(V1),V2)	(25)
a__U55(tt,V2)	→	a__U56(a__isList(V2))	(26)
a__U56(tt)	→	tt	(27)
a__U61(tt,V)	→	a__U62(a__isPalListKind(V),V)	(28)
a__U62(tt,V)	→	a__U63(a__isQid(V))	(29)
a__U71(tt,I,P)	→	a__U72(a__isPalListKind(I),P)	(31)
a__U72(tt,P)	→	a__U73(a__isPal(P),P)	(32)
a__U73(tt,P)	→	a__U74(a__isPalListKind(P))	(33)
a__U81(tt,V)	→	a__U82(a__isPalListKind(V),V)	(35)
a__U82(tt,V)	→	a__U83(a__isNePal(V))	(36)
a__U91(tt,V2)	→	a__U92(a__isPalListKind(V2))	(38)
a__isList(V)	→	a__U11(a__isPalListKind(V),V)	(40)
a__isList(nil)	→	tt	(41)
a__isList(__(V1,V2))	→	a__U21(a__isPalListKind(V1),V1,V2)	(42)
a__isNeList(V)	→	a__U31(a__isPalListKind(V),V)	(43)
a__isNeList(__(V1,V2))	→	a__U41(a__isPalListKind(V1),V1,V2)	(44)
a__isNeList(__(V1,V2))	→	a__U51(a__isPalListKind(V1),V1,V2)	(45)
a__isNePal(V)	→	a__U61(a__isPalListKind(V),V)	(46)
a__isNePal(__(I,__(P,I)))	→	a__U71(a__isQid(I),I,P)	(47)
a__isPal(V)	→	a__U81(a__isPalListKind(V),V)	(48)
a__isPal(nil)	→	tt	(49)
a__isPalListKind(a)	→	tt	(50)
a__isPalListKind(e)	→	tt	(51)
a__isPalListKind(i)	→	tt	(52)
a__isPalListKind(u)	→	tt	(55)
a__isPalListKind(__(V1,V2))	→	a__U91(a__isPalListKind(V1),V2)	(56)
a__isQid(a)	→	tt	(57)
a__isQid(e)	→	tt	(58)
a__isQid(i)	→	tt	(59)
a__isQid(o)	→	tt	(60)
a__isQid(u)	→	tt	(61)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[a__U13(x₁)]	=	2 + 2 · x₁
[tt]	=	1
[a__U26(x₁)]	=	2 + 2 · x₁
[a__U33(x₁)]	=	2 + 2 · x₁
[a__U63(x₁)]	=	2 + 2 · x₁
[a__U74(x₁)]	=	2 + 2 · x₁
[a__U83(x₁)]	=	2 + 2 · x₁
[a__U92(x₁)]	=	2 + 2 · x₁
[a__isPalListKind(x₁)]	=	2 + 2 · x₁
[nil]	=	1
[o]	=	1
[mark(x₁)]	=	2 · x₁
[__(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a____(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U11(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U12(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[isPalListKind(x₁)]	=	1 + 2 · x₁
[U13(x₁)]	=	1 + 2 · x₁
[isNeList(x₁)]	=	1 + 2 · x₁
[a__isNeList(x₁)]	=	2 + 2 · x₁
[U21(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U21(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U22(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U23(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[a__U23(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U24(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U24(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U25(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U25(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[isList(x₁)]	=	1 + 2 · x₁
[a__isList(x₁)]	=	2 + 2 · x₁
[U26(x₁)]	=	1 + 2 · x₁
[U31(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U31(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U32(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U32(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U33(x₁)]	=	1 + 2 · x₁
[isQid(x₁)]	=	1 + 2 · x₁
[a__isQid(x₁)]	=	2 + 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₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U42(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U43(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U43(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U44(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U44(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U45(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U46(x₁)]	=	1 + 1 · x₁
[a__U46(x₁)]	=	2 + 1 · 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₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U52(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U53(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U54(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U54(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U55(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U55(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U56(x₁)]	=	1 + 1 · x₁
[a__U56(x₁)]	=	2 + 1 · x₁
[U61(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U61(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U62(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U63(x₁)]	=	1 + 2 · x₁
[U71(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[a__U71(x₁, x₂, x₃)]	=	2 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U72(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U72(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U73(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U73(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[isPal(x₁)]	=	1 + 2 · x₁
[a__isPal(x₁)]	=	2 + 2 · x₁
[U74(x₁)]	=	1 + 2 · x₁
[U81(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U81(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U82(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[a__U82(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U83(x₁)]	=	1 + 2 · x₁
[isNePal(x₁)]	=	1 + 2 · x₁
[a__isNePal(x₁)]	=	2 + 2 · x₁
[U91(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[a__U91(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U92(x₁)]	=	1 + 2 · x₁
[a]	=	1
[e]	=	1
[i]	=	1
[u]	=	1

all of the following rules can be deleted.

a__U13(tt)	→	tt	(6)
a__U26(tt)	→	tt	(12)
a__U33(tt)	→	tt	(15)
a__U63(tt)	→	tt	(30)
a__U74(tt)	→	tt	(34)
a__U83(tt)	→	tt	(37)
a__U92(tt)	→	tt	(39)
a__isPalListKind(nil)	→	tt	(53)
a__isPalListKind(o)	→	tt	(54)
mark(nil)	→	nil	(105)
mark(tt)	→	tt	(106)
mark(a)	→	a	(107)
mark(e)	→	e	(108)
mark(i)	→	i	(109)
mark(o)	→	o	(110)
mark(u)	→	u	(111)
a____(X1,X2)	→	__(X1,X2)	(112)
a__U11(X1,X2)	→	U11(X1,X2)	(113)
a__U12(X1,X2)	→	U12(X1,X2)	(114)
a__isPalListKind(X)	→	isPalListKind(X)	(115)
a__U13(X)	→	U13(X)	(116)
a__isNeList(X)	→	isNeList(X)	(117)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(118)
a__U22(X1,X2,X3)	→	U22(X1,X2,X3)	(119)
a__U23(X1,X2,X3)	→	U23(X1,X2,X3)	(120)
a__U24(X1,X2,X3)	→	U24(X1,X2,X3)	(121)
a__U25(X1,X2)	→	U25(X1,X2)	(122)
a__isList(X)	→	isList(X)	(123)
a__U26(X)	→	U26(X)	(124)
a__U31(X1,X2)	→	U31(X1,X2)	(125)
a__U32(X1,X2)	→	U32(X1,X2)	(126)
a__U33(X)	→	U33(X)	(127)
a__isQid(X)	→	isQid(X)	(128)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(129)
a__U42(X1,X2,X3)	→	U42(X1,X2,X3)	(130)
a__U43(X1,X2,X3)	→	U43(X1,X2,X3)	(131)
a__U44(X1,X2,X3)	→	U44(X1,X2,X3)	(132)
a__U45(X1,X2)	→	U45(X1,X2)	(133)
a__U46(X)	→	U46(X)	(134)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(135)
a__U52(X1,X2,X3)	→	U52(X1,X2,X3)	(136)
a__U53(X1,X2,X3)	→	U53(X1,X2,X3)	(137)
a__U54(X1,X2,X3)	→	U54(X1,X2,X3)	(138)
a__U55(X1,X2)	→	U55(X1,X2)	(139)
a__U56(X)	→	U56(X)	(140)
a__U61(X1,X2)	→	U61(X1,X2)	(141)
a__U62(X1,X2)	→	U62(X1,X2)	(142)
a__U63(X)	→	U63(X)	(143)
a__U71(X1,X2,X3)	→	U71(X1,X2,X3)	(144)
a__U72(X1,X2)	→	U72(X1,X2)	(145)
a__U73(X1,X2)	→	U73(X1,X2)	(146)
a__isPal(X)	→	isPal(X)	(147)
a__U74(X)	→	U74(X)	(148)
a__U81(X1,X2)	→	U81(X1,X2)	(149)
a__U82(X1,X2)	→	U82(X1,X2)	(150)
a__U83(X)	→	U83(X)	(151)
a__isNePal(X)	→	isNePal(X)	(152)
a__U91(X1,X2)	→	U91(X1,X2)	(153)
a__U92(X)	→	U92(X)	(154)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[mark(x₁)]	=	1 + 2 · x₁
[__(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a____(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U11(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U11(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[a__U12(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[isPalListKind(x₁)]	=	2 · x₁
[a__isPalListKind(x₁)]	=	2 · x₁
[U13(x₁)]	=	2 + 2 · x₁
[a__U13(x₁)]	=	1 + 1 · x₁
[isNeList(x₁)]	=	2 + 1 · x₁
[a__isNeList(x₁)]	=	2 + 2 · x₁
[U21(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 1 · x₃
[a__U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 1 · x₂ + 1 · x₃
[a__U22(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U23(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U23(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U24(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 1 · x₂ + 1 · x₃
[a__U24(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U25(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[a__U25(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[isList(x₁)]	=	1 · x₁
[a__isList(x₁)]	=	2 · x₁
[U26(x₁)]	=	2 · x₁
[a__U26(x₁)]	=	1 · x₁
[U31(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[a__U31(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U32(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[a__U32(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U33(x₁)]	=	2 + 2 · x₁
[a__U33(x₁)]	=	2 · x₁
[isQid(x₁)]	=	2 · x₁
[a__isQid(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 1 · x₂ + 2 · x₃
[a__U41(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U42(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U42(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U43(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U43(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U44(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 1 · x₂ + 1 · x₃
[a__U44(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U45(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U46(x₁)]	=	2 + 2 · x₁
[a__U46(x₁)]	=	1 + 1 · x₁
[U51(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U51(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U52(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U52(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 2 · x₂ + 2 · x₃
[a__U53(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U54(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 1 · x₃
[a__U54(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U55(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[a__U55(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U56(x₁)]	=	2 + 2 · x₁
[a__U56(x₁)]	=	1 + 1 · x₁
[U61(x₁, x₂)]	=	1 + 2 · x₁ + 1 · x₂
[a__U61(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[a__U62(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U63(x₁)]	=	2 + 2 · x₁
[a__U63(x₁)]	=	1 + 1 · x₁
[U71(x₁, x₂, x₃)]	=	2 + 2 · x₁ + 1 · x₂ + 2 · x₃
[a__U71(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U72(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U72(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U73(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U73(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[isPal(x₁)]	=	1 · x₁
[a__isPal(x₁)]	=	1 + 2 · x₁
[U74(x₁)]	=	2 + 2 · x₁
[a__U74(x₁)]	=	1 + 1 · x₁
[U81(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[a__U81(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U82(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U82(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U83(x₁)]	=	2 + 2 · x₁
[a__U83(x₁)]	=	1 + 1 · x₁
[isNePal(x₁)]	=	2 · x₁
[a__isNePal(x₁)]	=	1 + 2 · x₁
[U91(x₁, x₂)]	=	2 + 2 · x₁ + 2 · x₂
[a__U91(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U92(x₁)]	=	2 + 2 · x₁
[a__U92(x₁)]	=	2 · x₁

all of the following rules can be deleted.

mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(62)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(63)
mark(U12(X1,X2))	→	a__U12(mark(X1),X2)	(64)
mark(isPalListKind(X))	→	a__isPalListKind(X)	(65)
mark(U13(X))	→	a__U13(mark(X))	(66)
mark(isNeList(X))	→	a__isNeList(X)	(67)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(68)
mark(U22(X1,X2,X3))	→	a__U22(mark(X1),X2,X3)	(69)
mark(U23(X1,X2,X3))	→	a__U23(mark(X1),X2,X3)	(70)
mark(U24(X1,X2,X3))	→	a__U24(mark(X1),X2,X3)	(71)
mark(U25(X1,X2))	→	a__U25(mark(X1),X2)	(72)
mark(isList(X))	→	a__isList(X)	(73)
mark(U32(X1,X2))	→	a__U32(mark(X1),X2)	(76)
mark(U33(X))	→	a__U33(mark(X))	(77)
mark(isQid(X))	→	a__isQid(X)	(78)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(79)
mark(U42(X1,X2,X3))	→	a__U42(mark(X1),X2,X3)	(80)
mark(U43(X1,X2,X3))	→	a__U43(mark(X1),X2,X3)	(81)
mark(U44(X1,X2,X3))	→	a__U44(mark(X1),X2,X3)	(82)
mark(U45(X1,X2))	→	a__U45(mark(X1),X2)	(83)
mark(U46(X))	→	a__U46(mark(X))	(84)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(85)
mark(U52(X1,X2,X3))	→	a__U52(mark(X1),X2,X3)	(86)
mark(U53(X1,X2,X3))	→	a__U53(mark(X1),X2,X3)	(87)
mark(U54(X1,X2,X3))	→	a__U54(mark(X1),X2,X3)	(88)
mark(U55(X1,X2))	→	a__U55(mark(X1),X2)	(89)
mark(U56(X))	→	a__U56(mark(X))	(90)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(91)
mark(U62(X1,X2))	→	a__U62(mark(X1),X2)	(92)
mark(U63(X))	→	a__U63(mark(X))	(93)
mark(U71(X1,X2,X3))	→	a__U71(mark(X1),X2,X3)	(94)
mark(U72(X1,X2))	→	a__U72(mark(X1),X2)	(95)
mark(U73(X1,X2))	→	a__U73(mark(X1),X2)	(96)
mark(U74(X))	→	a__U74(mark(X))	(98)
mark(U81(X1,X2))	→	a__U81(mark(X1),X2)	(99)
mark(U82(X1,X2))	→	a__U82(mark(X1),X2)	(100)
mark(U83(X))	→	a__U83(mark(X))	(101)
mark(U91(X1,X2))	→	a__U91(mark(X1),X2)	(103)
mark(U92(X))	→	a__U92(mark(X))	(104)

1.1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

prec(mark)	=	7	weight(mark)	=	3
prec(U26)	=	0	weight(U26)	=	2
prec(a__U26)	=	8	weight(a__U26)	=	1
prec(isPal)	=	2	weight(isPal)	=	1
prec(a__isPal)	=	4	weight(a__isPal)	=	4
prec(isNePal)	=	1	weight(isNePal)	=	1
prec(a__isNePal)	=	5	weight(a__isNePal)	=	3
prec(U31)	=	6	weight(U31)	=	1
prec(a__U31)	=	3	weight(a__U31)	=	0

all of the following rules can be deleted.

mark(U26(X))	→	a__U26(mark(X))	(74)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(75)
mark(isPal(X))	→	a__isPal(X)	(97)
mark(isNePal(X))	→	a__isNePal(X)	(102)

1.1.1.1.1 R is empty

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