Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_noand_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)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U22(tt)	→	tt	(6)
a__U31(tt)	→	tt	(7)
a__U41(tt,V2)	→	a__U42(a__isNeList(V2))	(8)
a__U42(tt)	→	tt	(9)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U52(tt)	→	tt	(11)
a__U61(tt)	→	tt	(12)
a__U71(tt,P)	→	a__U72(a__isPal(P))	(13)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isList(nil)	→	tt	(17)
a__isList(__(V1,V2))	→	a__U21(a__isList(V1),V2)	(18)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNeList(__(V1,V2))	→	a__U51(a__isNeList(V1),V2)	(21)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isNePal(__(I,__(P,I)))	→	a__U71(a__isQid(I),P)	(23)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isPal(nil)	→	tt	(25)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(i)	→	tt	(28)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[a__U72(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[tt]

0	0	0
0	0	0
0	0	0

[a__U61(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U22(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a____(x₁, x₂)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[nil]

1	0	0
0	0	0
0	0	0

[a__U71(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__isNePal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U52(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[u]

0	0	0
0	0	0
0	0	0

[U41(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__U81(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isPal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[isNeList(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a]

0	0	0
0	0	0
0	0	0

[U21(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U42(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U41(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U72(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isList(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isQid(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[o]

0	0	0
0	0	0
0	0	0

[isList(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U52(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U31(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U42(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[e]

0	0	0
0	0	0
0	0	0

[i]

1	0	0
0	0	0
0	0	0

[a__isNeList(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U31(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U51(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[isPal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U21(x₁, x₂)]

1	0	0
0	0	0
0	1	1

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U71(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U61(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U81(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[isQid(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U51(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U22(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

a____(X,nil)	→	mark(X)	(2)
a____(nil,X)	→	mark(X)	(3)
a__isList(nil)	→	tt	(17)
a__isPal(nil)	→	tt	(25)
a__isQid(i)	→	tt	(28)

1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[a__U72(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[tt]

1	0	0
0	0	0
0	0	0

[a__U61(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U22(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[a____(x₁, x₂)]

1	0	0
0	0	0
0	0	1

· x₁ +

1	0	0
0	0	1
0	1	1

· x₂ +

1	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__U71(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

1	0	0
0	0	0
0	0	0

[a__isNePal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U52(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[u]

1	0	0
0	0	0
0	0	0

[U41(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	1
0	0	0
0	0	0

· x₂ +

1	0	0
0	0	0
0	0	0

[a__U81(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isPal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[isNeList(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a]

1	0	0
0	0	0
0	0	0

[U21(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U42(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U41(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	1
0	0	0
0	0	0

· x₂ +

1	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	0	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	1	1

· x₂ +

1	0	0
0	0	0
0	0	0

[U72(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isList(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isQid(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[o]

1	0	0
0	0	0
0	0	0

[isList(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U52(x₁)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[U31(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U42(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[e]

1	0	0
0	0	0
0	0	0

[i]

0	0	0
0	0	0
0	0	0

[a__isNeList(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U31(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U51(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[isPal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U21(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U71(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

1	0	0
0	0	0
0	0	0

[U61(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U81(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[isQid(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U51(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	1	1
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U22(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

a__U22(tt)	→	tt	(6)
a__U41(tt,V2)	→	a__U42(a__isNeList(V2))	(8)
a__U52(tt)	→	tt	(11)
a__U71(tt,P)	→	a__U72(a__isPal(P))	(13)
a__isList(__(V1,V2))	→	a__U21(a__isList(V1),V2)	(18)
a__isNeList(__(V1,V2))	→	a__U51(a__isNeList(V1),V2)	(21)
a__isNePal(__(I,__(P,I)))	→	a__U71(a__isQid(I),P)	(23)

1.1.1 Rule Removal

Using the linear polynomial interpretation over (3 x 3)-matrices with strict dimension 1 over the naturals

[a__U72(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[tt]

1	0	0
0	0	0
0	0	0

[a__U61(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U22(x₁)]

1	0	1
0	1	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[a____(x₁, x₂)]

1	0	1
0	0	0
0	0	1

· x₁ +

1	0	0
0	0	0
0	1	1

· x₂ +

0	0	0
0	0	0
0	0	0

[nil]

0	0	0
0	0	0
0	0	0

[a__U71(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__isNePal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U52(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[u]

1	0	0
0	0	0
0	0	0

[U41(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__U81(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isPal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[isNeList(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a]

1	0	0
0	0	0
0	0	0

[U21(x₁, x₂)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[a__U11(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U42(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[a__U41(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[__(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	1	1

· x₂ +

0	0	0
0	0	0
0	0	0

[U72(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isList(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__isQid(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[o]

1	0	0
0	0	0
0	0	0

[isList(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U52(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[U31(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U42(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[e]

1	0	0
0	0	0
0	0	0

[i]

0	0	0
0	0	0
0	0	0

[a__isNeList(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U31(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U51(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[isPal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[a__U21(x₁, x₂)]

1	1	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U71(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U61(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U81(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[isQid(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[U51(x₁, x₂)]

1	0	0
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

· x₂ +

0	0	0
0	0	0
0	0	0

[U22(x₁)]

1	0	1
0	0	0
0	0	0

· x₁ +

1	0	0
0	0	0
0	0	0

[isNePal(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

[mark(x₁)]

1	0	0
0	0	0
0	0	0

· x₁ +

0	0	0
0	0	0
0	0	0

all of the following rules can be deleted.

a__U42(tt)

→

(9)

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a____^#(__(X,Y),Z)	→	mark^#(Z)	(74)
a____^#(__(X,Y),Z)	→	mark^#(Y)	(75)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(76)
a____^#(__(X,Y),Z)	→	mark^#(X)	(77)
a____^#(__(X,Y),Z)	→	a____^#(mark(X),a____(mark(Y),mark(Z)))	(78)
a__U21^#(tt,V2)	→	a__isList^#(V2)	(79)
a__U21^#(tt,V2)	→	a__U22^#(a__isList(V2))	(80)
a__U51^#(tt,V2)	→	a__isList^#(V2)	(81)
a__U51^#(tt,V2)	→	a__U52^#(a__isList(V2))	(82)
a__isList^#(V)	→	a__isNeList^#(V)	(83)
a__isList^#(V)	→	a__U11^#(a__isNeList(V))	(84)
a__isNeList^#(V)	→	a__isQid^#(V)	(85)
a__isNeList^#(V)	→	a__U31^#(a__isQid(V))	(86)
a__isNeList^#(__(V1,V2))	→	a__isList^#(V1)	(87)
a__isNeList^#(__(V1,V2))	→	a__U41^#(a__isList(V1),V2)	(88)
a__isNePal^#(V)	→	a__isQid^#(V)	(89)
a__isNePal^#(V)	→	a__U61^#(a__isQid(V))	(90)
a__isPal^#(V)	→	a__isNePal^#(V)	(91)
a__isPal^#(V)	→	a__U81^#(a__isNePal(V))	(92)
mark^#(__(X1,X2))	→	mark^#(X2)	(93)
mark^#(__(X1,X2))	→	mark^#(X1)	(94)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(95)
mark^#(U11(X))	→	mark^#(X)	(96)
mark^#(U11(X))	→	a__U11^#(mark(X))	(97)
mark^#(U21(X1,X2))	→	mark^#(X1)	(98)
mark^#(U21(X1,X2))	→	a__U21^#(mark(X1),X2)	(99)
mark^#(U22(X))	→	mark^#(X)	(100)
mark^#(U22(X))	→	a__U22^#(mark(X))	(101)
mark^#(isList(X))	→	a__isList^#(X)	(102)
mark^#(U31(X))	→	mark^#(X)	(103)
mark^#(U31(X))	→	a__U31^#(mark(X))	(104)
mark^#(U41(X1,X2))	→	mark^#(X1)	(105)
mark^#(U41(X1,X2))	→	a__U41^#(mark(X1),X2)	(106)
mark^#(U42(X))	→	mark^#(X)	(107)
mark^#(U42(X))	→	a__U42^#(mark(X))	(108)
mark^#(isNeList(X))	→	a__isNeList^#(X)	(109)
mark^#(U51(X1,X2))	→	mark^#(X1)	(110)
mark^#(U51(X1,X2))	→	a__U51^#(mark(X1),X2)	(111)
mark^#(U52(X))	→	mark^#(X)	(112)
mark^#(U52(X))	→	a__U52^#(mark(X))	(113)
mark^#(U61(X))	→	mark^#(X)	(114)
mark^#(U61(X))	→	a__U61^#(mark(X))	(115)
mark^#(U71(X1,X2))	→	mark^#(X1)	(116)
mark^#(U71(X1,X2))	→	a__U71^#(mark(X1),X2)	(117)
mark^#(U72(X))	→	mark^#(X)	(118)
mark^#(U72(X))	→	a__U72^#(mark(X))	(119)
mark^#(isPal(X))	→	a__isPal^#(X)	(120)
mark^#(U81(X))	→	mark^#(X)	(121)
mark^#(U81(X))	→	a__U81^#(mark(X))	(122)
mark^#(isQid(X))	→	a__isQid^#(X)	(123)
mark^#(isNePal(X))	→	a__isNePal^#(X)	(124)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

mark^#(U81(X))	→	mark^#(X)	(121)
mark^#(__(X1,X2))	→	mark^#(X2)	(93)
mark^#(__(X1,X2))	→	mark^#(X1)	(94)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(95)
a____^#(__(X,Y),Z)	→	mark^#(Z)	(74)
mark^#(U11(X))	→	mark^#(X)	(96)
mark^#(U21(X1,X2))	→	mark^#(X1)	(98)
mark^#(U22(X))	→	mark^#(X)	(100)
mark^#(U31(X))	→	mark^#(X)	(103)
mark^#(U41(X1,X2))	→	mark^#(X1)	(105)
mark^#(U42(X))	→	mark^#(X)	(107)
mark^#(U51(X1,X2))	→	mark^#(X1)	(110)
mark^#(U52(X))	→	mark^#(X)	(112)
mark^#(U61(X))	→	mark^#(X)	(114)
mark^#(U71(X1,X2))	→	mark^#(X1)	(116)
mark^#(U72(X))	→	mark^#(X)	(118)
a____^#(__(X,Y),Z)	→	mark^#(Y)	(75)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(76)
a____^#(__(X,Y),Z)	→	mark^#(X)	(77)
a____^#(__(X,Y),Z)	→	a____^#(mark(X),a____(mark(Y),mark(Z)))	(78)

1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	6 · x₁ + 6
[tt]	=	1
[a__U61(x₁)]	=	0 · x₁ + 0
[a__U22(x₁)]	=	0 · x₁ + 0
[a____(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[nil]	=	0
[a__U71(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 7
[a__isNePal(x₁)]	=	0 · x₁ + 0
[U52(x₁)]	=	0 · x₁ + 1
[u]	=	2
[a__U81(x₁)]	=	0 · x₁ + 0
[U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__isPal(x₁)]	=	0 · x₁ + 0
[U11(x₁)]	=	0 · x₁ + 0
[isNeList(x₁)]	=	0 · x₁ + 1
[a]	=	4
[U21(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + -∞
[a____^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U11(x₁)]	=	0 · x₁ + 0
[U42(x₁)]	=	0 · x₁ + 5
[a__U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[__(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U72(x₁)]	=	6 · x₁ + 6
[a__isList(x₁)]	=	0 · x₁ + 1
[a__isQid(x₁)]	=	0 · x₁ + 0
[o]	=	1
[isList(x₁)]	=	0 · x₁ + 1
[a__U52(x₁)]	=	0 · x₁ + 1
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	0 · x₁ + 5
[mark^#(x₁)]	=	0 · x₁ + 0
[e]	=	4
[i]	=	2
[a__isNeList(x₁)]	=	0 · x₁ + 1
[a__U31(x₁)]	=	0 · x₁ + 0
[a__U51(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + 0
[isPal(x₁)]	=	0 · x₁ + -∞
[a__U21(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 0
[U71(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 7
[U61(x₁)]	=	0 · x₁ + 0
[U81(x₁)]	=	0 · x₁ + 0
[isQid(x₁)]	=	0 · x₁ + -∞
[U51(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + -∞
[U22(x₁)]	=	0 · x₁ + 0
[isNePal(x₁)]	=	0 · x₁ + -∞
[mark(x₁)]	=	0 · x₁ + 0

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pair

mark^#(U72(X))

→

mark^#(X)

(118)

could be deleted.

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	1 · x₁ + 0
[tt]	=	3
[a__U61(x₁)]	=	0 · x₁ + -∞
[a__U22(x₁)]	=	0 · x₁ + -∞
[a____(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[nil]	=	3
[a__U71(x₁, x₂)]	=	2 · x₁ + 0 · x₂ + -∞
[a__isNePal(x₁)]	=	4 · x₁ + 2
[U52(x₁)]	=	0 · x₁ + -∞
[u]	=	2
[a__U81(x₁)]	=	0 · x₁ + -∞
[U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__isPal(x₁)]	=	4 · x₁ + 3
[U11(x₁)]	=	0 · x₁ + -∞
[isNeList(x₁)]	=	4 · x₁ + 0
[a]	=	4
[U21(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + -∞
[a____^#(x₁, x₂)]	=	5 · x₁ + 5 · x₂ + -∞
[a__U11(x₁)]	=	0 · x₁ + -∞
[U42(x₁)]	=	0 · x₁ + -∞
[a__U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[__(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U72(x₁)]	=	1 · x₁ + 0
[a__isList(x₁)]	=	4 · x₁ + 0
[a__isQid(x₁)]	=	2 · x₁ + 0
[o]	=	2
[isList(x₁)]	=	4 · x₁ + 0
[a__U52(x₁)]	=	0 · x₁ + -∞
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	0 · x₁ + -∞
[mark^#(x₁)]	=	5 · x₁ + -∞
[e]	=	1
[i]	=	3
[a__isNeList(x₁)]	=	4 · x₁ + 0
[a__U31(x₁)]	=	0 · x₁ + -∞
[a__U51(x₁, x₂)]	=	0 · x₁ + 6 · x₂ + -∞
[isPal(x₁)]	=	4 · x₁ + 3
[a__U21(x₁, x₂)]	=	0 · x₁ + 4 · x₂ + -∞
[U71(x₁, x₂)]	=	2 · x₁ + 0 · x₂ + -∞
[U61(x₁)]	=	0 · x₁ + -∞
[U81(x₁)]	=	0 · x₁ + -∞
[isQid(x₁)]	=	2 · x₁ + 0
[U51(x₁, x₂)]	=	0 · x₁ + 6 · x₂ + -∞
[U22(x₁)]	=	0 · x₁ + -∞
[isNePal(x₁)]	=	4 · x₁ + 2
[mark(x₁)]	=	0 · x₁ + -∞

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pair

mark^#(U71(X1,X2))

→

mark^#(X1)

(116)

could be deleted.

1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	2 · x₁ + -∞
[tt]	=	0
[a__U61(x₁)]	=	0 · x₁ + -∞
[a__U22(x₁)]	=	0 · x₁ + -∞
[a____(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[nil]	=	2
[a__U71(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + -∞
[a__isNePal(x₁)]	=	-∞ · x₁ + 1
[U52(x₁)]	=	2 · x₁ + 2
[u]	=	1
[a__U81(x₁)]	=	1 · x₁ + 0
[U41(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[a__isPal(x₁)]	=	-∞ · x₁ + 4
[U11(x₁)]	=	0 · x₁ + 0
[isNeList(x₁)]	=	0 · x₁ + 0
[a]	=	0
[U21(x₁, x₂)]	=	4 · x₁ + 3 · x₂ + 0
[a____^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U11(x₁)]	=	0 · x₁ + 0
[U42(x₁)]	=	3 · x₁ + -∞
[a__U41(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[__(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U72(x₁)]	=	2 · x₁ + -∞
[a__isList(x₁)]	=	0 · x₁ + 0
[a__isQid(x₁)]	=	-∞ · x₁ + 0
[o]	=	4
[isList(x₁)]	=	0 · x₁ + 0
[a__U52(x₁)]	=	2 · x₁ + 2
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	3 · x₁ + -∞
[mark^#(x₁)]	=	0 · x₁ + 0
[e]	=	1
[i]	=	0
[a__isNeList(x₁)]	=	0 · x₁ + 0
[a__U31(x₁)]	=	0 · x₁ + -∞
[a__U51(x₁, x₂)]	=	2 · x₁ + 2 · x₂ + 0
[isPal(x₁)]	=	-∞ · x₁ + 4
[a__U21(x₁, x₂)]	=	4 · x₁ + 3 · x₂ + 0
[U71(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + -∞
[U61(x₁)]	=	0 · x₁ + -∞
[U81(x₁)]	=	1 · x₁ + 0
[isQid(x₁)]	=	-∞ · x₁ + 0
[U51(x₁, x₂)]	=	2 · x₁ + 2 · x₂ + 0
[U22(x₁)]	=	0 · x₁ + -∞
[isNePal(x₁)]	=	-∞ · x₁ + 1
[mark(x₁)]	=	0 · x₁ + -∞

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pair

mark^#(U52(X))

→

mark^#(X)

(112)

could be deleted.

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	0 · x₁ + 0
[tt]	=	0
[a__U61(x₁)]	=	0 · x₁ + 0
[a__U22(x₁)]	=	0 · x₁ + 0
[a____(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 1
[nil]	=	0
[a__U71(x₁, x₂)]	=	0 · x₁ + 5 · x₂ + 0
[a__isNePal(x₁)]	=	0 · x₁ + 0
[U52(x₁)]	=	6 · x₁ + 6
[u]	=	3
[a__U81(x₁)]	=	0 · x₁ + 0
[U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 1
[a__isPal(x₁)]	=	7 · x₁ + 2
[U11(x₁)]	=	0 · x₁ + 0
[isNeList(x₁)]	=	0 · x₁ + 0
[a]	=	2
[U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a____^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U11(x₁)]	=	0 · x₁ + 0
[U42(x₁)]	=	0 · x₁ + 0
[a__U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 1
[__(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 1
[U72(x₁)]	=	0 · x₁ + -∞
[a__isList(x₁)]	=	0 · x₁ + 0
[a__isQid(x₁)]	=	-∞ · x₁ + 0
[o]	=	2
[isList(x₁)]	=	0 · x₁ + -∞
[a__U52(x₁)]	=	6 · x₁ + 6
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	0 · x₁ + 0
[mark^#(x₁)]	=	0 · x₁ + 1
[e]	=	2
[i]	=	2
[a__isNeList(x₁)]	=	0 · x₁ + 0
[a__U31(x₁)]	=	0 · x₁ + 0
[a__U51(x₁, x₂)]	=	6 · x₁ + 6 · x₂ + 6
[isPal(x₁)]	=	7 · x₁ + 2
[a__U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U71(x₁, x₂)]	=	0 · x₁ + 5 · x₂ + 0
[U61(x₁)]	=	0 · x₁ + 0
[U81(x₁)]	=	0 · x₁ + 0
[isQid(x₁)]	=	-∞ · x₁ + 0
[U51(x₁, x₂)]	=	6 · x₁ + 6 · x₂ + 6
[U22(x₁)]	=	0 · x₁ + 0
[isNePal(x₁)]	=	0 · x₁ + -∞
[mark(x₁)]	=	0 · x₁ + 0

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pair

mark^#(U51(X1,X2))

→

mark^#(X1)

(110)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	0 · x₁ + -∞
[tt]	=	6
[a__U61(x₁)]	=	0 · x₁ + 0
[a__U22(x₁)]	=	0 · x₁ + -∞
[a____(x₁, x₂)]	=	3 · x₁ + 0 · x₂ + 0
[nil]	=	0
[a__U71(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + 2
[a__isNePal(x₁)]	=	1 · x₁ + 0
[U52(x₁)]	=	-∞ · x₁ + 0
[u]	=	6
[a__U81(x₁)]	=	0 · x₁ + 0
[U41(x₁, x₂)]	=	3 · x₁ + 0 · x₂ + -∞
[a__isPal(x₁)]	=	1 · x₁ + 0
[U11(x₁)]	=	0 · x₁ + -∞
[isNeList(x₁)]	=	0 · x₁ + -∞
[a]	=	6
[U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a____^#(x₁, x₂)]	=	3 · x₁ + 0 · x₂ + -∞
[a__U11(x₁)]	=	0 · x₁ + -∞
[U42(x₁)]	=	0 · x₁ + -∞
[a__U41(x₁, x₂)]	=	3 · x₁ + 0 · x₂ + -∞
[__(x₁, x₂)]	=	3 · x₁ + 0 · x₂ + 0
[U72(x₁)]	=	0 · x₁ + -∞
[a__isList(x₁)]	=	0 · x₁ + -∞
[a__isQid(x₁)]	=	0 · x₁ + -∞
[o]	=	7
[isList(x₁)]	=	0 · x₁ + -∞
[a__U52(x₁)]	=	-∞ · x₁ + 0
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	0 · x₁ + -∞
[mark^#(x₁)]	=	0 · x₁ + 0
[e]	=	7
[i]	=	0
[a__isNeList(x₁)]	=	0 · x₁ + -∞
[a__U31(x₁)]	=	0 · x₁ + -∞
[a__U51(x₁, x₂)]	=	-∞ · x₁ + -∞ · x₂ + 0
[isPal(x₁)]	=	1 · x₁ + 0
[a__U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U71(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + 2
[U61(x₁)]	=	0 · x₁ + 0
[U81(x₁)]	=	0 · x₁ + 0
[isQid(x₁)]	=	0 · x₁ + -∞
[U51(x₁, x₂)]	=	-∞ · x₁ + -∞ · x₂ + 0
[U22(x₁)]	=	0 · x₁ + -∞
[isNePal(x₁)]	=	1 · x₁ + 0
[mark(x₁)]	=	0 · x₁ + -∞

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

a____^#(__(X,Y),Z)	→	mark^#(Y)	(75)
a____^#(__(X,Y),Z)	→	mark^#(X)	(77)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	0 · x₁ + 0
[tt]	=	0
[a__U61(x₁)]	=	0 · x₁ + -∞
[a__U22(x₁)]	=	0 · x₁ + 0
[a____(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[nil]	=	5
[a__U71(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[a__isNePal(x₁)]	=	0 · x₁ + 3
[U52(x₁)]	=	-∞ · x₁ + 0
[u]	=	0
[a__U81(x₁)]	=	0 · x₁ + 0
[U41(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + -∞
[a__isPal(x₁)]	=	0 · x₁ + 4
[U11(x₁)]	=	0 · x₁ + -∞
[isNeList(x₁)]	=	0 · x₁ + -∞
[a]	=	0
[U21(x₁, x₂)]	=	1 · x₁ + 2 · x₂ + 4
[a____^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U11(x₁)]	=	0 · x₁ + -∞
[U42(x₁)]	=	0 · x₁ + -∞
[a__U41(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + -∞
[__(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U72(x₁)]	=	0 · x₁ + -∞
[a__isList(x₁)]	=	0 · x₁ + -∞
[a__isQid(x₁)]	=	0 · x₁ + -∞
[o]	=	0
[isList(x₁)]	=	0 · x₁ + -∞
[a__U52(x₁)]	=	-∞ · x₁ + 0
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	0 · x₁ + 0
[mark^#(x₁)]	=	0 · x₁ + 0
[e]	=	1
[i]	=	2
[a__isNeList(x₁)]	=	0 · x₁ + -∞
[a__U31(x₁)]	=	0 · x₁ + -∞
[a__U51(x₁, x₂)]	=	-∞ · x₁ + -∞ · x₂ + 0
[isPal(x₁)]	=	0 · x₁ + 4
[a__U21(x₁, x₂)]	=	1 · x₁ + 2 · x₂ + 4
[U71(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + -∞
[U61(x₁)]	=	0 · x₁ + -∞
[U81(x₁)]	=	0 · x₁ + -∞
[isQid(x₁)]	=	0 · x₁ + -∞
[U51(x₁, x₂)]	=	-∞ · x₁ + -∞ · x₂ + 0
[U22(x₁)]	=	0 · x₁ + 0
[isNePal(x₁)]	=	0 · x₁ + 3
[mark(x₁)]	=	0 · x₁ + 0

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pair

mark^#(U21(X1,X2))

→

mark^#(X1)

(98)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	5 · x₁ + -∞
[tt]	=	2
[a__U61(x₁)]	=	0 · x₁ + -∞
[a__U22(x₁)]	=	0 · x₁ + -∞
[a____(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[nil]	=	0
[a__U71(x₁, x₂)]	=	-∞ · x₁ + 2 · x₂ + 0
[a__isNePal(x₁)]	=	0 · x₁ + -∞
[U52(x₁)]	=	-∞ · x₁ + 0
[u]	=	2
[a__U81(x₁)]	=	0 · x₁ + -∞
[U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__isPal(x₁)]	=	3 · x₁ + -∞
[U11(x₁)]	=	0 · x₁ + -∞
[isNeList(x₁)]	=	0 · x₁ + -∞
[a]	=	2
[U21(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + -∞
[a____^#(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a__U11(x₁)]	=	0 · x₁ + -∞
[U42(x₁)]	=	4 · x₁ + 1
[a__U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[__(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U72(x₁)]	=	5 · x₁ + -∞
[a__isList(x₁)]	=	0 · x₁ + -∞
[a__isQid(x₁)]	=	0 · x₁ + -∞
[o]	=	4
[isList(x₁)]	=	0 · x₁ + -∞
[a__U52(x₁)]	=	-∞ · x₁ + 0
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	4 · x₁ + 1
[mark^#(x₁)]	=	0 · x₁ + 0
[e]	=	5
[i]	=	1
[a__isNeList(x₁)]	=	0 · x₁ + -∞
[a__U31(x₁)]	=	0 · x₁ + -∞
[a__U51(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[isPal(x₁)]	=	3 · x₁ + -∞
[a__U21(x₁, x₂)]	=	0 · x₁ + 1 · x₂ + -∞
[U71(x₁, x₂)]	=	-∞ · x₁ + 2 · x₂ + 0
[U61(x₁)]	=	0 · x₁ + -∞
[U81(x₁)]	=	0 · x₁ + -∞
[isQid(x₁)]	=	0 · x₁ + -∞
[U51(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U22(x₁)]	=	0 · x₁ + -∞
[isNePal(x₁)]	=	0 · x₁ + -∞
[mark(x₁)]	=	0 · x₁ + -∞

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pair

mark^#(U42(X))

→

mark^#(X)

(107)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	1 · x₁ + 0
[tt]	=	0
[a__U61(x₁)]	=	0 · x₁ + -∞
[a__U22(x₁)]	=	4 · x₁ + -∞
[a____(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[nil]	=	2
[a__U71(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + -∞
[a__isNePal(x₁)]	=	0 · x₁ + 0
[U52(x₁)]	=	0 · x₁ + -∞
[u]	=	2
[a__U81(x₁)]	=	0 · x₁ + -∞
[U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[a__isPal(x₁)]	=	5 · x₁ + 0
[U11(x₁)]	=	0 · x₁ + -∞
[isNeList(x₁)]	=	0 · x₁ + -∞
[a]	=	2
[U21(x₁, x₂)]	=	4 · x₁ + 4 · x₂ + 0
[a____^#(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + -∞
[a__U11(x₁)]	=	0 · x₁ + -∞
[U42(x₁)]	=	4 · x₁ + -∞
[a__U41(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[__(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[U72(x₁)]	=	1 · x₁ + 0
[a__isList(x₁)]	=	0 · x₁ + -∞
[a__isQid(x₁)]	=	0 · x₁ + -∞
[o]	=	3
[isList(x₁)]	=	0 · x₁ + -∞
[a__U52(x₁)]	=	0 · x₁ + -∞
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	4 · x₁ + -∞
[mark^#(x₁)]	=	1 · x₁ + -∞
[e]	=	2
[i]	=	4
[a__isNeList(x₁)]	=	0 · x₁ + -∞
[a__U31(x₁)]	=	0 · x₁ + -∞
[a__U51(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + -∞
[isPal(x₁)]	=	5 · x₁ + 0
[a__U21(x₁, x₂)]	=	4 · x₁ + 4 · x₂ + 0
[U71(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + -∞
[U61(x₁)]	=	0 · x₁ + -∞
[U81(x₁)]	=	0 · x₁ + -∞
[isQid(x₁)]	=	0 · x₁ + -∞
[U51(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + -∞
[U22(x₁)]	=	4 · x₁ + -∞
[isNePal(x₁)]	=	0 · x₁ + 0
[mark(x₁)]	=	0 · x₁ + -∞

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pair

mark^#(U22(X))

→

mark^#(X)

(100)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the rationals with delta = 1/64

[a__U72(x₁)]	=	0 · x₁ + 2
[tt]	=	0
[a__U61(x₁)]	=	2 · x₁ + 0
[a__U22(x₁)]	=	0 · x₁ + 0
[a____(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 1/2
[nil]	=	0
[a__U71(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 2
[a__isNePal(x₁)]	=	0 · x₁ + 0
[U52(x₁)]	=	0 · x₁ + 0
[u]	=	0
[a__U81(x₁)]	=	1 · x₁ + 0
[U41(x₁, x₂)]	=	2 · x₁ + 0 · x₂ + 0
[a__isPal(x₁)]	=	0 · x₁ + 0
[U11(x₁)]	=	5/2 · x₁ + 0
[isNeList(x₁)]	=	0 · x₁ + 0
[a]	=	0
[U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[a____^#(x₁, x₂)]	=	2 · x₁ + 2 · x₂ + 0
[a__U11(x₁)]	=	5/2 · x₁ + 0
[U42(x₁)]	=	0 · x₁ + 0
[a__U41(x₁, x₂)]	=	2 · x₁ + 0 · x₂ + 0
[__(x₁, x₂)]	=	1 · x₁ + 1 · x₂ + 1/2
[U72(x₁)]	=	0 · x₁ + 2
[a__isList(x₁)]	=	0 · x₁ + 0
[a__isQid(x₁)]	=	0 · x₁ + 0
[o]	=	0
[isList(x₁)]	=	0 · x₁ + 0
[a__U52(x₁)]	=	0 · x₁ + 0
[U31(x₁)]	=	1 · x₁ + 0
[a__U42(x₁)]	=	0 · x₁ + 0
[mark^#(x₁)]	=	2 · x₁ + 1
[e]	=	0
[i]	=	0
[a__isNeList(x₁)]	=	0 · x₁ + 0
[a__U31(x₁)]	=	1 · x₁ + 0
[a__U51(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 1
[isPal(x₁)]	=	0 · x₁ + 0
[a__U21(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 0
[U71(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 2
[U61(x₁)]	=	2 · x₁ + 0
[U81(x₁)]	=	1 · x₁ + 0
[isQid(x₁)]	=	0 · x₁ + 0
[U51(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + 1
[U22(x₁)]	=	0 · x₁ + 0
[isNePal(x₁)]	=	0 · x₁ + 0
[mark(x₁)]	=	1 · x₁ + 0

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

mark^#(__(X1,X2))	→	mark^#(X2)	(93)
mark^#(__(X1,X2))	→	mark^#(X1)	(94)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(95)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(76)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

a____^#(__(X,Y),Z)

→

a____^#(mark(X),a____(mark(Y),mark(Z)))

(78)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[a__U72(x₁)]	=	0 · x₁ + 4
[tt]	=	0
[a__U61(x₁)]	=	0 · x₁ + 0
[a__U22(x₁)]	=	-∞ · x₁ + 0
[a____(x₁, x₂)]	=	1 · x₁ + 0 · x₂ + 1
[nil]	=	6
[a__U71(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + 0
[a__isNePal(x₁)]	=	1 · x₁ + 0
[U52(x₁)]	=	-∞ · x₁ + 0
[u]	=	2
[U41(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + -∞
[a__U81(x₁)]	=	0 · x₁ + 0
[a__isPal(x₁)]	=	1 · x₁ + 0
[U11(x₁)]	=	0 · x₁ + -∞
[isNeList(x₁)]	=	0 · x₁ + -∞
[a]	=	4
[U21(x₁, x₂)]	=	-∞ · x₁ + -∞ · x₂ + 0
[a____^#(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[a__U11(x₁)]	=	0 · x₁ + -∞
[U42(x₁)]	=	-∞ · x₁ + 0
[a__U41(x₁, x₂)]	=	-∞ · x₁ + 0 · x₂ + -∞
[__(x₁, x₂)]	=	1 · x₁ + 0 · x₂ + 1
[U72(x₁)]	=	0 · x₁ + 4
[a__isList(x₁)]	=	0 · x₁ + 0
[a__isQid(x₁)]	=	0 · x₁ + -∞
[o]	=	4
[isList(x₁)]	=	0 · x₁ + -∞
[a__U52(x₁)]	=	-∞ · x₁ + 0
[U31(x₁)]	=	0 · x₁ + -∞
[a__U42(x₁)]	=	-∞ · x₁ + 0
[e]	=	5
[i]	=	7
[a__isNeList(x₁)]	=	0 · x₁ + -∞
[a__U31(x₁)]	=	0 · x₁ + -∞
[a__U51(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[isPal(x₁)]	=	1 · x₁ + -∞
[a__U21(x₁, x₂)]	=	-∞ · x₁ + -∞ · x₂ + 0
[U71(x₁, x₂)]	=	0 · x₁ + 2 · x₂ + -∞
[U61(x₁)]	=	0 · x₁ + -∞
[U81(x₁)]	=	0 · x₁ + -∞
[isQid(x₁)]	=	0 · x₁ + -∞
[U51(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + -∞
[U22(x₁)]	=	-∞ · x₁ + 0
[isNePal(x₁)]	=	1 · x₁ + 0
[mark(x₁)]	=	0 · x₁ + 0

together with the usable rules

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(tt)	→	tt	(4)
a__U21(tt,V2)	→	a__U22(a__isList(V2))	(5)
a__U31(tt)	→	tt	(7)
a__U51(tt,V2)	→	a__U52(a__isList(V2))	(10)
a__U61(tt)	→	tt	(12)
a__U72(tt)	→	tt	(14)
a__U81(tt)	→	tt	(15)
a__isList(V)	→	a__U11(a__isNeList(V))	(16)
a__isNeList(V)	→	a__U31(a__isQid(V))	(19)
a__isNeList(__(V1,V2))	→	a__U41(a__isList(V1),V2)	(20)
a__isNePal(V)	→	a__U61(a__isQid(V))	(22)
a__isPal(V)	→	a__U81(a__isNePal(V))	(24)
a__isQid(a)	→	tt	(26)
a__isQid(e)	→	tt	(27)
a__isQid(o)	→	tt	(29)
a__isQid(u)	→	tt	(30)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(31)
mark(U11(X))	→	a__U11(mark(X))	(32)
mark(U21(X1,X2))	→	a__U21(mark(X1),X2)	(33)
mark(U22(X))	→	a__U22(mark(X))	(34)
mark(isList(X))	→	a__isList(X)	(35)
mark(U31(X))	→	a__U31(mark(X))	(36)
mark(U41(X1,X2))	→	a__U41(mark(X1),X2)	(37)
mark(U42(X))	→	a__U42(mark(X))	(38)
mark(isNeList(X))	→	a__isNeList(X)	(39)
mark(U51(X1,X2))	→	a__U51(mark(X1),X2)	(40)
mark(U52(X))	→	a__U52(mark(X))	(41)
mark(U61(X))	→	a__U61(mark(X))	(42)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(43)
mark(U72(X))	→	a__U72(mark(X))	(44)
mark(isPal(X))	→	a__isPal(X)	(45)
mark(U81(X))	→	a__U81(mark(X))	(46)
mark(isQid(X))	→	a__isQid(X)	(47)
mark(isNePal(X))	→	a__isNePal(X)	(48)
mark(nil)	→	nil	(49)
mark(tt)	→	tt	(50)
mark(a)	→	a	(51)
mark(e)	→	e	(52)
mark(i)	→	i	(53)
mark(o)	→	o	(54)
mark(u)	→	u	(55)
a____(X1,X2)	→	__(X1,X2)	(56)
a__U11(X)	→	U11(X)	(57)
a__U21(X1,X2)	→	U21(X1,X2)	(58)
a__U22(X)	→	U22(X)	(59)
a__isList(X)	→	isList(X)	(60)
a__U31(X)	→	U31(X)	(61)
a__U41(X1,X2)	→	U41(X1,X2)	(62)
a__U42(X)	→	U42(X)	(63)
a__isNeList(X)	→	isNeList(X)	(64)
a__U51(X1,X2)	→	U51(X1,X2)	(65)
a__U52(X)	→	U52(X)	(66)
a__U61(X)	→	U61(X)	(67)
a__U71(X1,X2)	→	U71(X1,X2)	(68)
a__U72(X)	→	U72(X)	(69)
a__isPal(X)	→	isPal(X)	(70)
a__U81(X)	→	U81(X)	(71)
a__isQid(X)	→	isQid(X)	(72)
a__isNePal(X)	→	isNePal(X)	(73)

(w.r.t. the implicit argument filter of the reduction pair), the pair

a____^#(__(X,Y),Z)

→

a____^#(mark(X),a____(mark(Y),mark(Z)))

(78)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair

mark^#(U81(X))	→	mark^#(X)	(121)
mark^#(U11(X))	→	mark^#(X)	(96)
mark^#(U31(X))	→	mark^#(X)	(103)
mark^#(U41(X1,X2))	→	mark^#(X1)	(105)
mark^#(U61(X))	→	mark^#(X)	(114)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

mark^#(U81(X))	→	mark^#(X)	(121)

1	>	1
mark^#(U11(X))	→	mark^#(X)	(96)

1	>	1
mark^#(U31(X))	→	mark^#(X)	(103)

1	>	1
mark^#(U41(X1,X2))	→	mark^#(X1)	(105)

1	>	1
mark^#(U61(X))	→	mark^#(X)	(114)

1	>	1

As there is no critical graph in the transitive closure, there are no infinite chains.

The 2^nd component contains the pair

a__isNeList^#(__(V1,V2)) → a__isList^#(V1) (87)

a__isList^#(V) → a__isNeList^#(V) (83)

1.1.1.1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

a__isNeList^#(__(V1,V2)) → a__isList^#(V1) (87)

1 > 1

a__isList^#(V) → a__isNeList^#(V) (83)

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.