Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_complete_C)

The rewrite relation of the following TRS is considered.

There are 142 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(__)	=	19	stat(__)	=	lex
prec(nil)	=	20	stat(nil)	=	mul
prec(U11)	=	6	stat(U11)	=	lex
prec(tt)	=	1	stat(tt)	=	mul
prec(isNeList)	=	5	stat(isNeList)	=	mul
prec(U21)	=	9	stat(U21)	=	lex
prec(U22)	=	8	stat(U22)	=	mul
prec(isList)	=	7	stat(isList)	=	mul
prec(U31)	=	3	stat(U31)	=	mul
prec(isQid)	=	2	stat(isQid)	=	mul
prec(U41)	=	11	stat(U41)	=	lex
prec(U42)	=	10	stat(U42)	=	mul
prec(U43)	=	0	stat(U43)	=	mul
prec(U51)	=	13	stat(U51)	=	lex
prec(U52)	=	12	stat(U52)	=	mul
prec(U61)	=	15	stat(U61)	=	lex
prec(U62)	=	14	stat(U62)	=	lex
prec(U71)	=	17	stat(U71)	=	lex
prec(isNePal)	=	17	stat(isNePal)	=	lex
prec(and)	=	16	stat(and)	=	mul
prec(isPalListKind)	=	4	stat(isPalListKind)	=	mul
prec(isPal)	=	18	stat(isPal)	=	mul
prec(a)	=	21	stat(a)	=	mul
prec(e)	=	1	stat(e)	=	mul
prec(i)	=	22	stat(i)	=	mul
prec(o)	=	23	stat(o)	=	mul
prec(u)	=	24	stat(u)	=	mul

π(active)	=	1
π(__)	=	[1,2]
π(mark)	=	1
π(nil)	=	[]
π(U11)	=	[1,2]
π(tt)	=	[]
π(U12)	=	1
π(isNeList)	=	[1]
π(U21)	=	[1,2,3]
π(U22)	=	[1,2]
π(isList)	=	[1]
π(U23)	=	1
π(U31)	=	[1,2]
π(U32)	=	1
π(isQid)	=	[1]
π(U41)	=	[2,3,1]
π(U42)	=	[1,2]
π(U43)	=	[1]
π(U51)	=	[1,2,3]
π(U52)	=	[1,2]
π(U53)	=	1
π(U61)	=	[2,1]
π(U62)	=	[1]
π(U71)	=	[2,1]
π(U72)	=	1
π(isNePal)	=	[1]
π(and)	=	[1,2]
π(isPalListKind)	=	[1]
π(isPal)	=	[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(isNeList(V)))	(4)
active(U21(tt,V1,V2))	→	mark(U22(isList(V1),V2))	(6)
active(U22(tt,V2))	→	mark(U23(isList(V2)))	(7)
active(U31(tt,V))	→	mark(U32(isQid(V)))	(9)
active(U41(tt,V1,V2))	→	mark(U42(isList(V1),V2))	(11)
active(U42(tt,V2))	→	mark(U43(isNeList(V2)))	(12)
active(U43(tt))	→	mark(tt)	(13)
active(U51(tt,V1,V2))	→	mark(U52(isNeList(V1),V2))	(14)
active(U52(tt,V2))	→	mark(U53(isList(V2)))	(15)
active(U61(tt,V))	→	mark(U62(isQid(V)))	(17)
active(U62(tt))	→	mark(tt)	(18)
active(U71(tt,V))	→	mark(U72(isNePal(V)))	(19)
active(and(tt,X))	→	mark(X)	(21)
active(isList(V))	→	mark(U11(isPalListKind(V),V))	(22)
active(isList(nil))	→	mark(tt)	(23)
active(isList(__(V1,V2)))	→	mark(U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2))	(24)
active(isNeList(V))	→	mark(U31(isPalListKind(V),V))	(25)
active(isNeList(__(V1,V2)))	→	mark(U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2))	(26)
active(isNeList(__(V1,V2)))	→	mark(U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2))	(27)
active(isNePal(V))	→	mark(U61(isPalListKind(V),V))	(28)
active(isNePal(__(I,__(P,I))))	→	mark(and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))))	(29)
active(isPal(V))	→	mark(U71(isPalListKind(V),V))	(30)
active(isPal(nil))	→	mark(tt)	(31)
active(isPalListKind(a))	→	mark(tt)	(32)
active(isPalListKind(e))	→	mark(tt)	(33)
active(isPalListKind(i))	→	mark(tt)	(34)
active(isPalListKind(nil))	→	mark(tt)	(35)
active(isPalListKind(o))	→	mark(tt)	(36)
active(isPalListKind(u))	→	mark(tt)	(37)
active(isPalListKind(__(V1,V2)))	→	mark(and(isPalListKind(V1),isPalListKind(V2)))	(38)
active(isQid(a))	→	mark(tt)	(39)
active(isQid(e))	→	mark(tt)	(40)
active(isQid(i))	→	mark(tt)	(41)
active(isQid(o))	→	mark(tt)	(42)
active(isQid(u))	→	mark(tt)	(43)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U12(x₁)]	=	1 + 1 · x₁
[tt]	=	0
[mark(x₁)]	=	1 · x₁
[U23(x₁)]	=	2 · x₁
[U32(x₁)]	=	2 · x₁
[U53(x₁)]	=	2 · x₁
[U72(x₁)]	=	2 · x₁
[__(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U21(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U31(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U41(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U42(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U43(x₁)]	=	2 · x₁
[U51(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U52(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U61(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U62(x₁)]	=	1 · x₁
[U71(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[and(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	1 · x₁
[isQid(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	1 · x₁
[isPal(x₁)]	=	1 · x₁
[a]	=	0
[e]	=	0
[i]	=	0
[o]	=	0
[u]	=	0
[top(x₁)]	=	2 · x₁

all of the following rules can be deleted.

active(U12(tt))

→

mark(tt)

(5)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U23(x₁)]	=	2 + 2 · x₁
[tt]	=	0
[mark(x₁)]	=	1 + 1 · x₁
[U32(x₁)]	=	1 + 1 · x₁
[U53(x₁)]	=	1 + 2 · x₁
[U72(x₁)]	=	2 + 2 · x₁
[__(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U12(x₁)]	=	2 · x₁
[U21(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U31(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U41(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U42(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U43(x₁)]	=	2 · x₁
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U52(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U61(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U62(x₁)]	=	2 · x₁
[U71(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[and(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[proper(x₁)]	=	1 · x₁
[nil]	=	0
[ok(x₁)]	=	1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	1 · x₁
[isQid(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	2 · x₁
[isPal(x₁)]	=	1 · x₁
[a]	=	0
[e]	=	0
[i]	=	0
[o]	=	0
[u]	=	0
[top(x₁)]	=	1 · x₁

all of the following rules can be deleted.

active(U23(tt))	→	mark(tt)	(8)
active(U72(tt))	→	mark(tt)	(20)
__(mark(X1),X2)	→	mark(__(X1,X2))	(64)
__(X1,mark(X2))	→	mark(__(X1,X2))	(65)
U11(mark(X1),X2)	→	mark(U11(X1,X2))	(66)
U12(mark(X))	→	mark(U12(X))	(67)
U21(mark(X1),X2,X3)	→	mark(U21(X1,X2,X3))	(68)
U22(mark(X1),X2)	→	mark(U22(X1,X2))	(69)
U23(mark(X))	→	mark(U23(X))	(70)
U31(mark(X1),X2)	→	mark(U31(X1,X2))	(71)
U41(mark(X1),X2,X3)	→	mark(U41(X1,X2,X3))	(73)
U43(mark(X))	→	mark(U43(X))	(75)
U51(mark(X1),X2,X3)	→	mark(U51(X1,X2,X3))	(76)
U52(mark(X1),X2)	→	mark(U52(X1,X2))	(77)
U53(mark(X))	→	mark(U53(X))	(78)
U61(mark(X1),X2)	→	mark(U61(X1,X2))	(79)
U62(mark(X))	→	mark(U62(X))	(80)
U71(mark(X1),X2)	→	mark(U71(X1,X2))	(81)
U72(mark(X))	→	mark(U72(X))	(82)
and(mark(X1),X2)	→	mark(and(X1,X2))	(83)
top(mark(X))	→	top(proper(X))	(141)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	2 · x₁
[U32(x₁)]	=	2 · x₁
[tt]	=	1
[mark(x₁)]	=	2 + 1 · x₁
[U53(x₁)]	=	2 · x₁
[__(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U11(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U12(x₁)]	=	2 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U23(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U42(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U43(x₁)]	=	1 · x₁
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 2 · x₃
[U52(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U61(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U62(x₁)]	=	2 · x₁
[U71(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U72(x₁)]	=	2 · x₁
[and(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[proper(x₁)]	=	2 · x₁
[nil]	=	0
[ok(x₁)]	=	2 · x₁
[isNeList(x₁)]	=	2 · x₁
[isList(x₁)]	=	1 · x₁
[isQid(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	2 · x₁
[isPalListKind(x₁)]	=	2 · x₁
[isPal(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(U32(tt))	→	mark(tt)	(10)
active(U53(tt))	→	mark(tt)	(16)
U32(mark(X))	→	mark(U32(X))	(72)
U42(mark(X1),X2)	→	mark(U42(X1,X2))	(74)

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₁)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U22(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U23(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U32(x₁)]	=	1 · x₁
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 1 · x₃
[U42(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U43(x₁)]	=	1 · x₁
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 1 · x₂ + 1 · x₃
[U52(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U53(x₁)]	=	2 · x₁
[U61(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U62(x₁)]	=	1 + 2 · x₁
[U71(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U72(x₁)]	=	1 · x₁
[and(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[proper(x₁)]	=	2 · x₁
[nil]	=	1
[ok(x₁)]	=	1 · x₁
[tt]	=	1
[isNeList(x₁)]	=	2 · x₁
[isList(x₁)]	=	1 + 1 · x₁
[isQid(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	2 · x₁
[isPalListKind(x₁)]	=	1 · x₁
[isPal(x₁)]	=	2 · x₁
[a]	=	1
[e]	=	1
[i]	=	0
[o]	=	0
[u]	=	0
[top(x₁)]	=	1 · x₁

all of the following rules can be deleted.

proper(nil)	→	ok(nil)	(85)
proper(tt)	→	ok(tt)	(87)
proper(isList(X))	→	isList(proper(X))	(92)
proper(U62(X))	→	U62(proper(X))	(104)
proper(a)	→	ok(a)	(111)
proper(e)	→	ok(e)	(112)

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₁ + 1 · x₂
[U12(x₁)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U23(x₁)]	=	1 · x₁
[U31(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U32(x₁)]	=	1 · x₁
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 1 · x₃
[U42(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U43(x₁)]	=	2 · x₁
[U51(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 1 · x₃
[U52(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U53(x₁)]	=	2 · x₁
[U61(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U62(x₁)]	=	2 · x₁
[U71(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U72(x₁)]	=	2 + 1 · x₁
[and(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[proper(x₁)]	=	2 · x₁
[isNeList(x₁)]	=	2 · x₁
[isQid(x₁)]	=	2 · x₁
[isNePal(x₁)]	=	2 · x₁
[isPalListKind(x₁)]	=	1 + 1 · x₁
[isPal(x₁)]	=	2 · x₁
[i]	=	0
[ok(x₁)]	=	1 · x₁
[o]	=	1
[u]	=	0
[isList(x₁)]	=	2 · x₁
[top(x₁)]	=	1 · x₁

all of the following rules can be deleted.

proper(U72(X))	→	U72(proper(X))	(106)
proper(isPalListKind(X))	→	isPalListKind(proper(X))	(109)
proper(o)	→	ok(o)	(114)

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₁)]	=	2 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U23(x₁)]	=	2 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U32(x₁)]	=	1 · x₁
[U41(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U42(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U43(x₁)]	=	2 + 1 · x₁
[U51(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₂ + 1 · x₃
[U52(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U53(x₁)]	=	1 + 1 · x₁
[U61(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[U62(x₁)]	=	1 · x₁
[U71(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U72(x₁)]	=	2 · x₁
[and(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[proper(x₁)]	=	2 · x₁
[isNeList(x₁)]	=	2 + 2 · x₁
[isQid(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	1 · x₁
[isPal(x₁)]	=	1 + 2 · x₁
[i]	=	1
[ok(x₁)]	=	1 · x₁
[u]	=	0
[isList(x₁)]	=	1 · x₁
[isPalListKind(x₁)]	=	1 · x₁
[top(x₁)]	=	2 · x₁

all of the following rules can be deleted.

proper(isNeList(X))	→	isNeList(proper(X))	(89)
proper(U43(X))	→	U43(proper(X))	(99)
proper(U51(X1,X2,X3))	→	U51(proper(X1),proper(X2),proper(X3))	(100)
proper(U53(X))	→	U53(proper(X))	(102)
proper(isPal(X))	→	isPal(proper(X))	(110)
proper(i)	→	ok(i)	(113)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[__(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U11(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U12(x₁)]	=	1 · x₁
[U21(x₁, x₂, x₃)]	=	1 · x₁ + 1 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U23(x₁)]	=	1 + 1 · x₁
[U31(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U32(x₁)]	=	2 · x₁
[U41(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 1 · x₃
[U42(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[U43(x₁)]	=	2 · x₁
[U51(x₁, x₂, x₃)]	=	1 · x₁ + 2 · x₂ + 2 · x₃
[U52(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U53(x₁)]	=	2 · x₁
[U61(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[U62(x₁)]	=	1 · x₁
[U71(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[U72(x₁)]	=	1 · x₁
[and(x₁, x₂)]	=	1 · x₁ + 2 · x₂
[proper(x₁)]	=	2 · x₁
[isQid(x₁)]	=	1 + 1 · x₁
[isNePal(x₁)]	=	2 · x₁
[u]	=	2
[ok(x₁)]	=	1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isList(x₁)]	=	2 · x₁
[isPalListKind(x₁)]	=	1 · x₁
[isPal(x₁)]	=	2 · x₁
[top(x₁)]	=	1 · x₁

all of the following rules can be deleted.

proper(U23(X))	→	U23(proper(X))	(93)
proper(isQid(X))	→	isQid(proper(X))	(96)
proper(U41(X1,X2,X3))	→	U41(proper(X1),proper(X2),proper(X3))	(97)
proper(u)	→	ok(u)	(115)

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)	=	27	weight(active)	=	3
prec(U12)	=	22	weight(U12)	=	5
prec(U23)	=	10	weight(U23)	=	5
prec(U32)	=	23	weight(U32)	=	5
prec(U43)	=	20	weight(U43)	=	5
prec(U53)	=	11	weight(U53)	=	5
prec(U62)	=	12	weight(U62)	=	5
prec(U72)	=	13	weight(U72)	=	5
prec(proper)	=	28	weight(proper)	=	0
prec(isNePal)	=	15	weight(isNePal)	=	5
prec(ok)	=	9	weight(ok)	=	4
prec(isNeList)	=	16	weight(isNeList)	=	5
prec(isList)	=	17	weight(isList)	=	5
prec(isQid)	=	21	weight(isQid)	=	5
prec(isPalListKind)	=	24	weight(isPalListKind)	=	5
prec(isPal)	=	25	weight(isPal)	=	5
prec(top)	=	26	weight(top)	=	1
prec(__)	=	4	weight(__)	=	0
prec(U11)	=	14	weight(U11)	=	0
prec(U21)	=	0	weight(U21)	=	0
prec(U22)	=	18	weight(U22)	=	0
prec(U31)	=	1	weight(U31)	=	0
prec(U41)	=	5	weight(U41)	=	0
prec(U42)	=	6	weight(U42)	=	0
prec(U51)	=	2	weight(U51)	=	0
prec(U52)	=	8	weight(U52)	=	0
prec(U61)	=	19	weight(U61)	=	0
prec(U71)	=	3	weight(U71)	=	0
prec(and)	=	7	weight(and)	=	0

all of the following rules can be deleted.

active(__(X1,X2))	→	__(active(X1),X2)	(44)
active(__(X1,X2))	→	__(X1,active(X2))	(45)
active(U11(X1,X2))	→	U11(active(X1),X2)	(46)
active(U12(X))	→	U12(active(X))	(47)
active(U21(X1,X2,X3))	→	U21(active(X1),X2,X3)	(48)
active(U22(X1,X2))	→	U22(active(X1),X2)	(49)
active(U23(X))	→	U23(active(X))	(50)
active(U31(X1,X2))	→	U31(active(X1),X2)	(51)
active(U32(X))	→	U32(active(X))	(52)
active(U41(X1,X2,X3))	→	U41(active(X1),X2,X3)	(53)
active(U42(X1,X2))	→	U42(active(X1),X2)	(54)
active(U43(X))	→	U43(active(X))	(55)
active(U51(X1,X2,X3))	→	U51(active(X1),X2,X3)	(56)
active(U52(X1,X2))	→	U52(active(X1),X2)	(57)
active(U53(X))	→	U53(active(X))	(58)
active(U61(X1,X2))	→	U61(active(X1),X2)	(59)
active(U62(X))	→	U62(active(X))	(60)
active(U71(X1,X2))	→	U71(active(X1),X2)	(61)
active(U72(X))	→	U72(active(X))	(62)
active(and(X1,X2))	→	and(active(X1),X2)	(63)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(84)
proper(U11(X1,X2))	→	U11(proper(X1),proper(X2))	(86)
proper(U12(X))	→	U12(proper(X))	(88)
proper(U21(X1,X2,X3))	→	U21(proper(X1),proper(X2),proper(X3))	(90)
proper(U22(X1,X2))	→	U22(proper(X1),proper(X2))	(91)
proper(U31(X1,X2))	→	U31(proper(X1),proper(X2))	(94)
proper(U32(X))	→	U32(proper(X))	(95)
proper(U42(X1,X2))	→	U42(proper(X1),proper(X2))	(98)
proper(U52(X1,X2))	→	U52(proper(X1),proper(X2))	(101)
proper(U61(X1,X2))	→	U61(proper(X1),proper(X2))	(103)
proper(U71(X1,X2))	→	U71(proper(X1),proper(X2))	(105)
proper(isNePal(X))	→	isNePal(proper(X))	(107)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(108)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(116)
U11(ok(X1),ok(X2))	→	ok(U11(X1,X2))	(117)
U12(ok(X))	→	ok(U12(X))	(118)
isNeList(ok(X))	→	ok(isNeList(X))	(119)
U21(ok(X1),ok(X2),ok(X3))	→	ok(U21(X1,X2,X3))	(120)
U22(ok(X1),ok(X2))	→	ok(U22(X1,X2))	(121)
isList(ok(X))	→	ok(isList(X))	(122)
U23(ok(X))	→	ok(U23(X))	(123)
U31(ok(X1),ok(X2))	→	ok(U31(X1,X2))	(124)
U32(ok(X))	→	ok(U32(X))	(125)
isQid(ok(X))	→	ok(isQid(X))	(126)
U41(ok(X1),ok(X2),ok(X3))	→	ok(U41(X1,X2,X3))	(127)
U42(ok(X1),ok(X2))	→	ok(U42(X1,X2))	(128)
U43(ok(X))	→	ok(U43(X))	(129)
U51(ok(X1),ok(X2),ok(X3))	→	ok(U51(X1,X2,X3))	(130)
U52(ok(X1),ok(X2))	→	ok(U52(X1,X2))	(131)
U53(ok(X))	→	ok(U53(X))	(132)
U61(ok(X1),ok(X2))	→	ok(U61(X1,X2))	(133)
U62(ok(X))	→	ok(U62(X))	(134)
U71(ok(X1),ok(X2))	→	ok(U71(X1,X2))	(135)
U72(ok(X))	→	ok(U72(X))	(136)
isNePal(ok(X))	→	ok(isNePal(X))	(137)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(138)
isPalListKind(ok(X))	→	ok(isPalListKind(X))	(139)
isPal(ok(X))	→	ok(isPal(X))	(140)
top(ok(X))	→	top(active(X))	(142)

1.1.1.1.1.1.1.1.1.1 R is empty

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