Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_complete_noand_C)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the

prec(__)	=	30	stat(__)	=	lex
prec(nil)	=	31	stat(nil)	=	mul
prec(U11)	=	8	stat(U11)	=	mul
prec(tt)	=	1	stat(tt)	=	mul
prec(U12)	=	7	stat(U12)	=	lex
prec(isPalListKind)	=	2	stat(isPalListKind)	=	mul
prec(isNeList)	=	6	stat(isNeList)	=	mul
prec(U21)	=	15	stat(U21)	=	mul
prec(U22)	=	14	stat(U22)	=	lex
prec(U23)	=	13	stat(U23)	=	lex
prec(U24)	=	12	stat(U24)	=	lex
prec(U25)	=	11	stat(U25)	=	mul
prec(isList)	=	11	stat(isList)	=	mul
prec(U26)	=	9	stat(U26)	=	mul
prec(U31)	=	5	stat(U31)	=	mul
prec(U32)	=	4	stat(U32)	=	mul
prec(U33)	=	3	stat(U33)	=	mul
prec(U41)	=	18	stat(U41)	=	lex
prec(U42)	=	17	stat(U42)	=	lex
prec(U43)	=	16	stat(U43)	=	mul
prec(U44)	=	11	stat(U44)	=	mul
prec(U45)	=	10	stat(U45)	=	mul
prec(U51)	=	22	stat(U51)	=	mul
prec(U52)	=	21	stat(U52)	=	lex
prec(U53)	=	20	stat(U53)	=	mul
prec(U54)	=	19	stat(U54)	=	mul
prec(U55)	=	11	stat(U55)	=	mul
prec(U61)	=	24	stat(U61)	=	mul
prec(U62)	=	23	stat(U62)	=	mul
prec(U63)	=	0	stat(U63)	=	mul
prec(U71)	=	29	stat(U71)	=	lex
prec(U72)	=	28	stat(U72)	=	lex
prec(U73)	=	2	stat(U73)	=	mul
prec(isPal)	=	27	stat(isPal)	=	mul
prec(U81)	=	26	stat(U81)	=	mul
prec(U82)	=	25	stat(U82)	=	mul
prec(isNePal)	=	25	stat(isNePal)	=	mul
prec(U91)	=	2	stat(U91)	=	mul
prec(a)	=	1	stat(a)	=	mul
prec(e)	=	1	stat(e)	=	mul
prec(i)	=	32	stat(i)	=	mul
prec(o)	=	1	stat(o)	=	mul
prec(u)	=	1	stat(u)	=	mul
prec(top)	=	33	stat(top)	=	mul

π(active)	=	1
π(__)	=	[1,2]
π(mark)	=	1
π(nil)	=	[]
π(U11)	=	[1,2]
π(tt)	=	[]
π(U12)	=	[1,2]
π(isPalListKind)	=	[1]
π(U13)	=	1
π(isNeList)	=	[1]
π(U21)	=	[1,2,3]
π(U22)	=	[1,3,2]
π(U23)	=	[3,2,1]
π(U24)	=	[2,1,3]
π(U25)	=	[1,2]
π(isList)	=	[1]
π(U26)	=	[1]
π(U31)	=	[1,2]
π(U32)	=	[1,2]
π(U33)	=	[1]
π(isQid)	=	1
π(U41)	=	[2,1,3]
π(U42)	=	[3,1,2]
π(U43)	=	[1,2,3]
π(U44)	=	[1,2,3]
π(U45)	=	[1,2]
π(U46)	=	1
π(U51)	=	[1,2,3]
π(U52)	=	[3,1,2]
π(U53)	=	[1,2,3]
π(U54)	=	[1,2,3]
π(U55)	=	[1,2]
π(U56)	=	1
π(U61)	=	[1,2]
π(U62)	=	[1,2]
π(U63)	=	[1]
π(U71)	=	[2,3,1]
π(U72)	=	[2,1]
π(U73)	=	[1,2]
π(isPal)	=	[1]
π(U74)	=	1
π(U81)	=	[1,2]
π(U82)	=	[1,2]
π(U83)	=	1
π(isNePal)	=	[1]
π(U91)	=	[1,2]
π(U92)	=	1
π(a)	=	[]
π(e)	=	[]
π(i)	=	[]
π(o)	=	[]
π(u)	=	[]
π(proper)	=	1
π(ok)	=	1
π(top)	=	[1]

all of the following rules can be deleted.

active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(X,nil))	→	mark(X)	(2)
active(__(nil,X))	→	mark(X)	(3)
active(U11(tt,V))	→	mark(U12(isPalListKind(V),V))	(4)
active(U12(tt,V))	→	mark(U13(isNeList(V)))	(5)
active(U21(tt,V1,V2))	→	mark(U22(isPalListKind(V1),V1,V2))	(7)
active(U22(tt,V1,V2))	→	mark(U23(isPalListKind(V2),V1,V2))	(8)
active(U23(tt,V1,V2))	→	mark(U24(isPalListKind(V2),V1,V2))	(9)
active(U24(tt,V1,V2))	→	mark(U25(isList(V1),V2))	(10)
active(U25(tt,V2))	→	mark(U26(isList(V2)))	(11)
active(U26(tt))	→	mark(tt)	(12)
active(U31(tt,V))	→	mark(U32(isPalListKind(V),V))	(13)
active(U32(tt,V))	→	mark(U33(isQid(V)))	(14)
active(U33(tt))	→	mark(tt)	(15)
active(U41(tt,V1,V2))	→	mark(U42(isPalListKind(V1),V1,V2))	(16)
active(U42(tt,V1,V2))	→	mark(U43(isPalListKind(V2),V1,V2))	(17)
active(U43(tt,V1,V2))	→	mark(U44(isPalListKind(V2),V1,V2))	(18)
active(U44(tt,V1,V2))	→	mark(U45(isList(V1),V2))	(19)
active(U45(tt,V2))	→	mark(U46(isNeList(V2)))	(20)
active(U51(tt,V1,V2))	→	mark(U52(isPalListKind(V1),V1,V2))	(22)
active(U52(tt,V1,V2))	→	mark(U53(isPalListKind(V2),V1,V2))	(23)
active(U53(tt,V1,V2))	→	mark(U54(isPalListKind(V2),V1,V2))	(24)
active(U54(tt,V1,V2))	→	mark(U55(isNeList(V1),V2))	(25)
active(U55(tt,V2))	→	mark(U56(isList(V2)))	(26)
active(U61(tt,V))	→	mark(U62(isPalListKind(V),V))	(28)
active(U62(tt,V))	→	mark(U63(isQid(V)))	(29)
active(U63(tt))	→	mark(tt)	(30)
active(U71(tt,I,P))	→	mark(U72(isPalListKind(I),P))	(31)
active(U72(tt,P))	→	mark(U73(isPal(P),P))	(32)
active(U73(tt,P))	→	mark(U74(isPalListKind(P)))	(33)
active(U81(tt,V))	→	mark(U82(isPalListKind(V),V))	(35)
active(U82(tt,V))	→	mark(U83(isNePal(V)))	(36)
active(U91(tt,V2))	→	mark(U92(isPalListKind(V2)))	(38)
active(isList(V))	→	mark(U11(isPalListKind(V),V))	(40)
active(isList(nil))	→	mark(tt)	(41)
active(isList(__(V1,V2)))	→	mark(U21(isPalListKind(V1),V1,V2))	(42)
active(isNeList(V))	→	mark(U31(isPalListKind(V),V))	(43)
active(isNeList(__(V1,V2)))	→	mark(U41(isPalListKind(V1),V1,V2))	(44)
active(isNeList(__(V1,V2)))	→	mark(U51(isPalListKind(V1),V1,V2))	(45)
active(isNePal(V))	→	mark(U61(isPalListKind(V),V))	(46)
active(isNePal(__(I,__(P,I))))	→	mark(U71(isQid(I),I,P))	(47)
active(isPal(V))	→	mark(U81(isPalListKind(V),V))	(48)
active(isPal(nil))	→	mark(tt)	(49)
active(isPalListKind(a))	→	mark(tt)	(50)
active(isPalListKind(e))	→	mark(tt)	(51)
active(isPalListKind(i))	→	mark(tt)	(52)
active(isPalListKind(nil))	→	mark(tt)	(53)
active(isPalListKind(o))	→	mark(tt)	(54)
active(isPalListKind(u))	→	mark(tt)	(55)
active(isPalListKind(__(V1,V2)))	→	mark(U91(isPalListKind(V1),V2))	(56)
active(isQid(i))	→	mark(tt)	(59)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U13(x₁)]	=	1 · x₁
[tt]	=	0
[mark(x₁)]	=	1 · x₁
[U46(x₁)]	=	1 · x₁
[U56(x₁)]	=	2 · x₁
[U74(x₁)]	=	1 · x₁
[U83(x₁)]	=	2 · x₁
[U92(x₁)]	=	2 · x₁
[isQid(x₁)]	=	2 · x₁
[a]	=	0
[e]	=	0
[o]	=	1
[u]	=	0
[__(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U21(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U23(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U24(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U25(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U26(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U32(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U33(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U42(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U43(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U44(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U51(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U52(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U54(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U55(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U61(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U63(x₁)]	=	1 · x₁
[U71(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U72(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U73(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U81(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U82(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U91(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	1 · x₁
[isNeList(x₁)]	=	2 · x₁
[isList(x₁)]	=	1 · x₁
[isPal(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	2 · x₁
[i]	=	0
[top(x₁)]	=	2 · x₁

all of the following rules can be deleted.

active(isQid(o))

→

mark(tt)

(60)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U13(x₁)]	=	2 · x₁
[tt]	=	0
[mark(x₁)]	=	1 · x₁
[U46(x₁)]	=	2 · x₁
[U56(x₁)]	=	2 · x₁
[U74(x₁)]	=	1 · x₁
[U83(x₁)]	=	2 · x₁
[U92(x₁)]	=	2 + 1 · x₁
[isQid(x₁)]	=	1 · x₁
[a]	=	1
[e]	=	0
[u]	=	2
[__(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U21(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U23(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U24(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U25(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U26(x₁)]	=	1 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U32(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U33(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U42(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U43(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U44(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U52(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U53(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U54(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U55(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U61(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U63(x₁)]	=	2 · x₁
[U71(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U72(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U73(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U81(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U82(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U91(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	2 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	1 · x₁
[isPal(x₁)]	=	2 · x₁
[isNePal(x₁)]	=	1 · x₁
[i]	=	0
[o]	=	0
[top(x₁)]	=	1 · x₁

all of the following rules can be deleted.

active(U92(tt))	→	mark(tt)	(39)
active(isQid(a))	→	mark(tt)	(57)
active(isQid(u))	→	mark(tt)	(61)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U13(x₁)]	=	1 · x₁
[tt]	=	0
[mark(x₁)]	=	1 · x₁
[U46(x₁)]	=	1 · x₁
[U56(x₁)]	=	1 · x₁
[U74(x₁)]	=	1 · x₁
[U83(x₁)]	=	2 · x₁
[isQid(x₁)]	=	1 · x₁
[e]	=	1
[__(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U22(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U23(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U24(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U25(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U26(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U32(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U33(x₁)]	=	1 · x₁
[U41(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U42(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U43(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U44(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U52(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U53(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U54(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U55(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U61(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U63(x₁)]	=	1 · x₁
[U71(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U72(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U73(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U81(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U82(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U91(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U92(x₁)]	=	2 · x₁
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	2 · x₁
[isNeList(x₁)]	=	2 · x₁
[isList(x₁)]	=	2 · x₁
[isPal(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	2 · x₁
[a]	=	0
[i]	=	0
[o]	=	0
[u]	=	0
[top(x₁)]	=	2 · x₁

all of the following rules can be deleted.

active(isQid(e))

→

mark(tt)

(58)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U13(x₁)]	=	1 + 2 · x₁
[tt]	=	0
[mark(x₁)]	=	1 · x₁
[U46(x₁)]	=	2 · x₁
[U56(x₁)]	=	2 · x₁
[U74(x₁)]	=	1 · x₁
[U83(x₁)]	=	2 · x₁
[__(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U22(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U23(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U24(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U25(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U26(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U32(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U33(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U42(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U43(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U44(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U52(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U54(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U55(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U61(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U63(x₁)]	=	2 · x₁
[U71(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U72(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U73(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U81(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U82(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U91(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U92(x₁)]	=	2 · x₁
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	2 · x₁
[isQid(x₁)]	=	2 · x₁
[isPal(x₁)]	=	2 · x₁
[isNePal(x₁)]	=	2 · x₁
[a]	=	0
[e]	=	0
[i]	=	0
[o]	=	0
[u]	=	0
[top(x₁)]	=	2 · x₁

all of the following rules can be deleted.

active(U13(tt))

→

mark(tt)

(6)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U46(x₁)]	=	1 + 2 · x₁
[tt]	=	0
[mark(x₁)]	=	1 · x₁
[U56(x₁)]	=	2 · x₁
[U74(x₁)]	=	1 + 2 · x₁
[U83(x₁)]	=	1 + 1 · x₁
[__(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U13(x₁)]	=	2 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U22(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U23(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U24(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U25(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U26(x₁)]	=	1 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U32(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U33(x₁)]	=	1 · x₁
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U42(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U43(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U44(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U52(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U54(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U55(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U61(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U63(x₁)]	=	1 · x₁
[U71(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U72(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U73(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U81(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U82(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U91(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U92(x₁)]	=	2 · x₁
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	2 · x₁
[isQid(x₁)]	=	1 · x₁
[isPal(x₁)]	=	2 · x₁
[isNePal(x₁)]	=	2 · x₁
[a]	=	0
[e]	=	0
[i]	=	0
[o]	=	0
[u]	=	0
[top(x₁)]	=	2 · x₁

all of the following rules can be deleted.

active(U46(tt))	→	mark(tt)	(21)
active(U74(tt))	→	mark(tt)	(34)
active(U83(tt))	→	mark(tt)	(37)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U56(x₁)]	=	2 · x₁
[tt]	=	2
[mark(x₁)]	=	1 · x₁
[__(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U13(x₁)]	=	2 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U22(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U23(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U24(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U25(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U26(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U32(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U33(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U42(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U43(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U44(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U45(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U46(x₁)]	=	1 · x₁
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U52(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U54(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U55(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U61(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U63(x₁)]	=	1 · x₁
[U71(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U72(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U73(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U74(x₁)]	=	2 · x₁
[U81(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U82(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U83(x₁)]	=	2 · x₁
[U91(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U92(x₁)]	=	2 · x₁
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	1 · x₁
[isQid(x₁)]	=	2 · x₁
[isPal(x₁)]	=	2 · x₁
[isNePal(x₁)]	=	2 · x₁
[a]	=	0
[e]	=	0
[i]	=	0
[o]	=	0
[u]	=	0
[top(x₁)]	=	2 · x₁

all of the following rules can be deleted.

active(U56(tt))

→

mark(tt)

(27)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[__(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U13(x₁)]	=	2 · x₁
[U21(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U22(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U23(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U24(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U25(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U26(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U32(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U33(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U42(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U43(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U44(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U46(x₁)]	=	2 · x₁
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U52(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U54(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U55(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U56(x₁)]	=	2 · x₁
[U61(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U62(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U63(x₁)]	=	2 · x₁
[U71(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U72(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U73(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U74(x₁)]	=	2 · x₁
[U81(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U82(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U83(x₁)]	=	2 · x₁
[U91(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U92(x₁)]	=	2 · x₁
[mark(x₁)]	=	2 + 1 · x₁
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	2 · x₁
[tt]	=	0
[isPalListKind(x₁)]	=	1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	1 · x₁
[isQid(x₁)]	=	2 · x₁
[isPal(x₁)]	=	2 · x₁
[isNePal(x₁)]	=	2 · x₁
[a]	=	0
[e]	=	0
[i]	=	0
[o]	=	0
[u]	=	0
[top(x₁)]	=	1 · x₁

all of the following rules can be deleted.

__(mark(X1),X2)	→	mark(__(X1,X2))	(100)
__(X1,mark(X2))	→	mark(__(X1,X2))	(101)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(102)
U12(mark(X1),X2)	→	mark(U12(X1,X2))	(103)
U13(mark(X))	→	mark(U13(X))	(104)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(105)
U22(mark(X1),X2,X3)	→	mark(U22(X1,X2,X3))	(106)
U23(mark(X1),X2,X3)	→	mark(U23(X1,X2,X3))	(107)
U24(mark(X1),X2,X3)	→	mark(U24(X1,X2,X3))	(108)
U25(mark(X1),X2)	→	mark(U25(X1,X2))	(109)
U26(mark(X))	→	mark(U26(X))	(110)
U31(mark(X1),X2)	→	mark(U31(X1,X2))	(111)
U32(mark(X1),X2)	→	mark(U32(X1,X2))	(112)
U33(mark(X))	→	mark(U33(X))	(113)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(114)
U42(mark(X1),X2,X3)	→	mark(U42(X1,X2,X3))	(115)
U43(mark(X1),X2,X3)	→	mark(U43(X1,X2,X3))	(116)
U44(mark(X1),X2,X3)	→	mark(U44(X1,X2,X3))	(117)
U45(mark(X1),X2)	→	mark(U45(X1,X2))	(118)
U46(mark(X))	→	mark(U46(X))	(119)
U51(mark(X1),X2,X3)	→	mark(U51(X1,X2,X3))	(120)
U52(mark(X1),X2,X3)	→	mark(U52(X1,X2,X3))	(121)
U53(mark(X1),X2,X3)	→	mark(U53(X1,X2,X3))	(122)
U54(mark(X1),X2,X3)	→	mark(U54(X1,X2,X3))	(123)
U55(mark(X1),X2)	→	mark(U55(X1,X2))	(124)
U56(mark(X))	→	mark(U56(X))	(125)
U61(mark(X1),X2)	→	mark(U61(X1,X2))	(126)
U62(mark(X1),X2)	→	mark(U62(X1,X2))	(127)
U63(mark(X))	→	mark(U63(X))	(128)
U71(mark(X1),X2,X3)	→	mark(U71(X1,X2,X3))	(129)
U72(mark(X1),X2)	→	mark(U72(X1,X2))	(130)
U73(mark(X1),X2)	→	mark(U73(X1,X2))	(131)
U74(mark(X))	→	mark(U74(X))	(132)
U81(mark(X1),X2)	→	mark(U81(X1,X2))	(133)
U82(mark(X1),X2)	→	mark(U82(X1,X2))	(134)
U83(mark(X))	→	mark(U83(X))	(135)
U91(mark(X1),X2)	→	mark(U91(X1,X2))	(136)
U92(mark(X))	→	mark(U92(X))	(137)
top(mark(X))	→	top(proper(X))	(231)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[__(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U11(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U12(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U13(x₁)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U23(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U24(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U25(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U26(x₁)]	=	1 + 1 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U32(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U33(x₁)]	=	1 · x₁
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U42(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U43(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U44(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U46(x₁)]	=	2 + 1 · x₁
[U51(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U52(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U54(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U55(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U56(x₁)]	=	2 · x₁
[U61(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U63(x₁)]	=	1 · x₁
[U71(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U72(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U73(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U74(x₁)]	=	1 + 1 · x₁
[U81(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U82(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U83(x₁)]	=	2 · x₁
[U91(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U92(x₁)]	=	2 · x₁
[proper(x₁)]	=	2 · x₁
[nil]	=	2
[ok(x₁)]	=	1 · x₁
[tt]	=	2
[isPalListKind(x₁)]	=	1 + 1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	1 + 1 · x₁
[isQid(x₁)]	=	1 + 2 · x₁
[isPal(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	1 · x₁
[a]	=	2
[e]	=	2
[i]	=	2
[o]	=	2
[u]	=	2
[top(x₁)]	=	2 · x₁

all of the following rules can be deleted.

proper(nil)	→	ok(nil)	(139)
proper(tt)	→	ok(tt)	(141)
proper(isPalListKind(X))	→	isPalListKind(proper(X))	(143)
proper(isList(X))	→	isList(proper(X))	(151)
proper(U26(X))	→	U26(proper(X))	(152)
proper(isQid(X))	→	isQid(proper(X))	(156)
proper(U46(X))	→	U46(proper(X))	(162)
proper(U73(X1,X2))	→	U73(proper(X1),proper(X2))	(174)
proper(U74(X))	→	U74(proper(X))	(176)
proper(a)	→	ok(a)	(183)
proper(e)	→	ok(e)	(184)
proper(i)	→	ok(i)	(185)
proper(o)	→	ok(o)	(186)
proper(u)	→	ok(u)	(187)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 + 2 · x₁
[__(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U13(x₁)]	=	1 + 2 · x₁
[U21(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U23(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U24(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U25(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U26(x₁)]	=	1 + 2 · x₁
[U31(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U32(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U33(x₁)]	=	1 + 2 · x₁
[U41(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U42(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U43(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U44(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U45(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U46(x₁)]	=	1 + 2 · x₁
[U51(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U52(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U53(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U54(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U55(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U56(x₁)]	=	1 + 2 · x₁
[U61(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U63(x₁)]	=	1 + 2 · x₁
[U71(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 2 · x₂ + 2 · x₃
[U72(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U73(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U74(x₁)]	=	1 + 2 · x₁
[U81(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U82(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U83(x₁)]	=	1 + 2 · x₁
[U91(x₁, x₂)]	=	1 + 2 · x₁ + 1 · x₂
[U92(x₁)]	=	1 + 2 · x₁
[proper(x₁)]	=	2 · x₁
[isNeList(x₁)]	=	1 + 2 · x₁
[isPal(x₁)]	=	1 + 2 · x₁
[isNePal(x₁)]	=	2 · x₁
[ok(x₁)]	=	2 + 2 · x₁
[isPalListKind(x₁)]	=	1 + 2 · x₁
[isList(x₁)]	=	1 + 2 · x₁
[isQid(x₁)]	=	1 + 2 · x₁
[top(x₁)]	=	1 · x₁

all of the following rules can be deleted.

active(__(X1,X2))	→	__(active(X1),X2)	(62)
active(U21(X1,X2,X3))	→	U21(active(X1),X2,X3)	(67)
active(U22(X1,X2,X3))	→	U22(active(X1),X2,X3)	(68)
active(U23(X1,X2,X3))	→	U23(active(X1),X2,X3)	(69)
active(U24(X1,X2,X3))	→	U24(active(X1),X2,X3)	(70)
active(U41(X1,X2,X3))	→	U41(active(X1),X2,X3)	(76)
active(U42(X1,X2,X3))	→	U42(active(X1),X2,X3)	(77)
active(U43(X1,X2,X3))	→	U43(active(X1),X2,X3)	(78)
active(U44(X1,X2,X3))	→	U44(active(X1),X2,X3)	(79)
active(U51(X1,X2,X3))	→	U51(active(X1),X2,X3)	(82)
active(U52(X1,X2,X3))	→	U52(active(X1),X2,X3)	(83)
active(U53(X1,X2,X3))	→	U53(active(X1),X2,X3)	(84)
active(U54(X1,X2,X3))	→	U54(active(X1),X2,X3)	(85)
active(U71(X1,X2,X3))	→	U71(active(X1),X2,X3)	(91)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(138)
proper(U11(X1,X2))	→	U11(proper(X1),proper(X2))	(140)
proper(U12(X1,X2))	→	U12(proper(X1),proper(X2))	(142)
proper(U13(X))	→	U13(proper(X))	(144)
proper(isNeList(X))	→	isNeList(proper(X))	(145)
proper(U21(X1,X2,X3))	→	U21(proper(X1),proper(X2),proper(X3))	(146)
proper(U22(X1,X2,X3))	→	U22(proper(X1),proper(X2),proper(X3))	(147)
proper(U23(X1,X2,X3))	→	U23(proper(X1),proper(X2),proper(X3))	(148)
proper(U24(X1,X2,X3))	→	U24(proper(X1),proper(X2),proper(X3))	(149)
proper(U25(X1,X2))	→	U25(proper(X1),proper(X2))	(150)
proper(U31(X1,X2))	→	U31(proper(X1),proper(X2))	(153)
proper(U32(X1,X2))	→	U32(proper(X1),proper(X2))	(154)
proper(U33(X))	→	U33(proper(X))	(155)
proper(U41(X1,X2,X3))	→	U41(proper(X1),proper(X2),proper(X3))	(157)
proper(U42(X1,X2,X3))	→	U42(proper(X1),proper(X2),proper(X3))	(158)
proper(U43(X1,X2,X3))	→	U43(proper(X1),proper(X2),proper(X3))	(159)
proper(U44(X1,X2,X3))	→	U44(proper(X1),proper(X2),proper(X3))	(160)
proper(U45(X1,X2))	→	U45(proper(X1),proper(X2))	(161)
proper(U51(X1,X2,X3))	→	U51(proper(X1),proper(X2),proper(X3))	(163)
proper(U52(X1,X2,X3))	→	U52(proper(X1),proper(X2),proper(X3))	(164)
proper(U53(X1,X2,X3))	→	U53(proper(X1),proper(X2),proper(X3))	(165)
proper(U54(X1,X2,X3))	→	U54(proper(X1),proper(X2),proper(X3))	(166)
proper(U55(X1,X2))	→	U55(proper(X1),proper(X2))	(167)
proper(U56(X))	→	U56(proper(X))	(168)
proper(U61(X1,X2))	→	U61(proper(X1),proper(X2))	(169)
proper(U62(X1,X2))	→	U62(proper(X1),proper(X2))	(170)
proper(U63(X))	→	U63(proper(X))	(171)
proper(U71(X1,X2,X3))	→	U71(proper(X1),proper(X2),proper(X3))	(172)
proper(U72(X1,X2))	→	U72(proper(X1),proper(X2))	(173)
proper(isPal(X))	→	isPal(proper(X))	(175)
proper(U81(X1,X2))	→	U81(proper(X1),proper(X2))	(177)
proper(U82(X1,X2))	→	U82(proper(X1),proper(X2))	(178)
proper(U83(X))	→	U83(proper(X))	(179)
proper(U91(X1,X2))	→	U91(proper(X1),proper(X2))	(181)
proper(U92(X))	→	U92(proper(X))	(182)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(188)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(189)
U12(ok(X1),ok(X2))	→	ok(U12(X1,X2))	(190)
isPalListKind(ok(X))	→	ok(isPalListKind(X))	(191)
U13(ok(X))	→	ok(U13(X))	(192)
isNeList(ok(X))	→	ok(isNeList(X))	(193)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(194)
U22(ok(X1),ok(X2),ok(X3))	→	ok(U22(X1,X2,X3))	(195)
U23(ok(X1),ok(X2),ok(X3))	→	ok(U23(X1,X2,X3))	(196)
U24(ok(X1),ok(X2),ok(X3))	→	ok(U24(X1,X2,X3))	(197)
U25(ok(X1),ok(X2))	→	ok(U25(X1,X2))	(198)
isList(ok(X))	→	ok(isList(X))	(199)
U26(ok(X))	→	ok(U26(X))	(200)
U31(ok(X1),ok(X2))	→	ok(U31(X1,X2))	(201)
U32(ok(X1),ok(X2))	→	ok(U32(X1,X2))	(202)
U33(ok(X))	→	ok(U33(X))	(203)
isQid(ok(X))	→	ok(isQid(X))	(204)
U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(205)
U42(ok(X1),ok(X2),ok(X3))	→	ok(U42(X1,X2,X3))	(206)
U43(ok(X1),ok(X2),ok(X3))	→	ok(U43(X1,X2,X3))	(207)
U44(ok(X1),ok(X2),ok(X3))	→	ok(U44(X1,X2,X3))	(208)
U45(ok(X1),ok(X2))	→	ok(U45(X1,X2))	(209)
U46(ok(X))	→	ok(U46(X))	(210)
U51(ok(X1),ok(X2),ok(X3))	→	ok(U51(X1,X2,X3))	(211)
U52(ok(X1),ok(X2),ok(X3))	→	ok(U52(X1,X2,X3))	(212)
U53(ok(X1),ok(X2),ok(X3))	→	ok(U53(X1,X2,X3))	(213)
U54(ok(X1),ok(X2),ok(X3))	→	ok(U54(X1,X2,X3))	(214)
U55(ok(X1),ok(X2))	→	ok(U55(X1,X2))	(215)
U56(ok(X))	→	ok(U56(X))	(216)
U61(ok(X1),ok(X2))	→	ok(U61(X1,X2))	(217)
U62(ok(X1),ok(X2))	→	ok(U62(X1,X2))	(218)
U63(ok(X))	→	ok(U63(X))	(219)
U71(ok(X1),ok(X2),ok(X3))	→	ok(U71(X1,X2,X3))	(220)
U72(ok(X1),ok(X2))	→	ok(U72(X1,X2))	(221)
U73(ok(X1),ok(X2))	→	ok(U73(X1,X2))	(222)
isPal(ok(X))	→	ok(isPal(X))	(223)
U74(ok(X))	→	ok(U74(X))	(224)
U81(ok(X1),ok(X2))	→	ok(U81(X1,X2))	(225)
U82(ok(X1),ok(X2))	→	ok(U82(X1,X2))	(226)
U83(ok(X))	→	ok(U83(X))	(227)
isNePal(ok(X))	→	ok(isNePal(X))	(228)
U91(ok(X1),ok(X2))	→	ok(U91(X1,X2))	(229)
U92(ok(X))	→	ok(U92(X))	(230)
top(ok(X))	→	top(active(X))	(232)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	2 · x₁
[__(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[U11(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U12(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U13(x₁)]	=	1 · x₁
[U25(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U26(x₁)]	=	1 + 2 · x₁
[U31(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[U32(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U33(x₁)]	=	1 + 1 · x₁
[U45(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U46(x₁)]	=	1 + 1 · x₁
[U55(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U56(x₁)]	=	1 + 1 · x₁
[U61(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U62(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U63(x₁)]	=	1 + 1 · x₁
[U72(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U73(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U74(x₁)]	=	1 + 1 · x₁
[U81(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U82(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U83(x₁)]	=	1 + 1 · x₁
[U91(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[U92(x₁)]	=	1 + 1 · x₁
[proper(x₁)]	=	2 + 2 · x₁
[isNePal(x₁)]	=	1 + 1 · x₁

all of the following rules can be deleted.

active(__(X1,X2))	→	__(X1,active(X2))	(63)
active(U11(X1,X2))	→	U11(active(X1),X2)	(64)
active(U12(X1,X2))	→	U12(active(X1),X2)	(65)
active(U25(X1,X2))	→	U25(active(X1),X2)	(71)
active(U26(X))	→	U26(active(X))	(72)
active(U31(X1,X2))	→	U31(active(X1),X2)	(73)
active(U32(X1,X2))	→	U32(active(X1),X2)	(74)
active(U33(X))	→	U33(active(X))	(75)
active(U45(X1,X2))	→	U45(active(X1),X2)	(80)
active(U46(X))	→	U46(active(X))	(81)
active(U55(X1,X2))	→	U55(active(X1),X2)	(86)
active(U56(X))	→	U56(active(X))	(87)
active(U61(X1,X2))	→	U61(active(X1),X2)	(88)
active(U62(X1,X2))	→	U62(active(X1),X2)	(89)
active(U63(X))	→	U63(active(X))	(90)
active(U72(X1,X2))	→	U72(active(X1),X2)	(92)
active(U73(X1,X2))	→	U73(active(X1),X2)	(93)
active(U74(X))	→	U74(active(X))	(94)
active(U81(X1,X2))	→	U81(active(X1),X2)	(95)
active(U82(X1,X2))	→	U82(active(X1),X2)	(96)
active(U83(X))	→	U83(active(X))	(97)
active(U91(X1,X2))	→	U91(active(X1),X2)	(98)
active(U92(X))	→	U92(active(X))	(99)
proper(isNePal(X))	→	isNePal(proper(X))	(180)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

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

prec(active)	=	1		weight(active)	=	2
prec(U13)	=	0		weight(U13)	=	1

all of the following rules can be deleted.

active(U13(X))

→

U13(active(X))

(66)

1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

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