Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_iGM)

The rewrite relation of the following TRS is considered.

active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(X,nil))	→	mark(X)	(2)
active(__(nil,X))	→	mark(X)	(3)
active(and(tt,X))	→	mark(X)	(4)
active(isList(V))	→	mark(isNeList(V))	(5)
active(isList(nil))	→	mark(tt)	(6)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
active(isNeList(V))	→	mark(isQid(V))	(8)
active(isNeList(__(V1,V2)))	→	mark(and(isList(V1),isNeList(V2)))	(9)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
active(isNePal(V))	→	mark(isQid(V))	(11)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
active(isPal(V))	→	mark(isNePal(V))	(13)
active(isPal(nil))	→	mark(tt)	(14)
active(isQid(a))	→	mark(tt)	(15)
active(isQid(e))	→	mark(tt)	(16)
active(isQid(i))	→	mark(tt)	(17)
active(isQid(o))	→	mark(tt)	(18)
active(isQid(u))	→	mark(tt)	(19)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(20)
mark(nil)	→	active(nil)	(21)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(22)
mark(tt)	→	active(tt)	(23)
mark(isList(X))	→	active(isList(X))	(24)
mark(isNeList(X))	→	active(isNeList(X))	(25)
mark(isQid(X))	→	active(isQid(X))	(26)
mark(isNePal(X))	→	active(isNePal(X))	(27)
mark(isPal(X))	→	active(isPal(X))	(28)
mark(a)	→	active(a)	(29)
mark(e)	→	active(e)	(30)
mark(i)	→	active(i)	(31)
mark(o)	→	active(o)	(32)
mark(u)	→	active(u)	(33)
__(mark(X1),X2)	→	__(X1,X2)	(34)
__(X1,mark(X2))	→	__(X1,X2)	(35)
__(active(X1),X2)	→	__(X1,X2)	(36)
__(X1,active(X2))	→	__(X1,X2)	(37)
and(mark(X1),X2)	→	and(X1,X2)	(38)
and(X1,mark(X2))	→	and(X1,X2)	(39)
and(active(X1),X2)	→	and(X1,X2)	(40)
and(X1,active(X2))	→	and(X1,X2)	(41)
isList(mark(X))	→	isList(X)	(42)
isList(active(X))	→	isList(X)	(43)
isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)
isQid(mark(X))	→	isQid(X)	(46)
isQid(active(X))	→	isQid(X)	(47)
isNePal(mark(X))	→	isNePal(X)	(48)
isNePal(active(X))	→	isNePal(X)	(49)
isPal(mark(X))	→	isPal(X)	(50)
isPal(active(X))	→	isPal(X)	(51)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

isList^#(active(X))	→	isList^#(X)	(52)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(53)
active^#(isNePal(__(I,__(P,I))))	→	isPal^#(P)	(54)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(55)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(56)
active^#(isNeList(__(V1,V2)))	→	isNeList^#(V1)	(57)
active^#(isList(__(V1,V2)))	→	isList^#(V2)	(58)
active^#(isList(__(V1,V2)))	→	isList^#(V1)	(59)
mark^#(__(X1,X2))	→	mark^#(X1)	(60)
isPal^#(mark(X))	→	isPal^#(X)	(61)
active^#(isNeList(__(V1,V2)))	→	isList^#(V2)	(62)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(63)
active^#(isQid(a))	→	mark^#(tt)	(64)
mark^#(u)	→	active^#(u)	(65)
active^#(isQid(o))	→	mark^#(tt)	(66)
active^#(isQid(i))	→	mark^#(tt)	(67)
mark^#(isQid(X))	→	active^#(isQid(X))	(68)
mark^#(__(X1,X2))	→	mark^#(X2)	(69)
isList^#(mark(X))	→	isList^#(X)	(70)
mark^#(o)	→	active^#(o)	(71)
mark^#(and(X1,X2))	→	mark^#(X1)	(72)
active^#(__(__(X,Y),Z))	→	__^#(X,__(Y,Z))	(73)
active^#(isList(__(V1,V2)))	→	and^#(isList(V1),isList(V2))	(74)
isNeList^#(mark(X))	→	isNeList^#(X)	(75)
and^#(active(X1),X2)	→	and^#(X1,X2)	(76)
isQid^#(active(X))	→	isQid^#(X)	(77)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(78)
mark^#(isNePal(X))	→	active^#(isNePal(X))	(79)
mark^#(tt)	→	active^#(tt)	(80)
active^#(isNeList(V))	→	isQid^#(V)	(81)
mark^#(isList(X))	→	active^#(isList(X))	(82)
active^#(isNeList(__(V1,V2)))	→	and^#(isNeList(V1),isList(V2))	(83)
active^#(isNeList(V))	→	mark^#(isQid(V))	(84)
active^#(isList(nil))	→	mark^#(tt)	(85)
active^#(isPal(nil))	→	mark^#(tt)	(86)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(87)
isPal^#(active(X))	→	isPal^#(X)	(88)
__^#(active(X1),X2)	→	__^#(X1,X2)	(89)
mark^#(i)	→	active^#(i)	(90)
mark^#(isPal(X))	→	active^#(isPal(X))	(91)
active^#(isList(V))	→	mark^#(isNeList(V))	(92)
isNeList^#(active(X))	→	isNeList^#(X)	(93)
active^#(isNeList(__(V1,V2)))	→	isNeList^#(V2)	(94)
and^#(X1,active(X2))	→	and^#(X1,X2)	(95)
active^#(isList(__(V1,V2)))	→	mark^#(and(isList(V1),isList(V2)))	(96)
isNePal^#(mark(X))	→	isNePal^#(X)	(97)
active^#(isQid(e))	→	mark^#(tt)	(98)
isNePal^#(active(X))	→	isNePal^#(X)	(99)
active^#(and(tt,X))	→	mark^#(X)	(100)
isQid^#(mark(X))	→	isQid^#(X)	(101)
active^#(isNeList(__(V1,V2)))	→	mark^#(and(isNeList(V1),isList(V2)))	(102)
active^#(__(nil,X))	→	mark^#(X)	(103)
active^#(isNePal(__(I,__(P,I))))	→	isQid^#(I)	(104)
active^#(isNePal(V))	→	isQid^#(V)	(105)
mark^#(isNeList(X))	→	active^#(isNeList(X))	(106)
active^#(isNePal(__(I,__(P,I))))	→	and^#(isQid(I),isPal(P))	(107)
active^#(isQid(u))	→	mark^#(tt)	(108)
active^#(isNeList(__(V1,V2)))	→	mark^#(and(isList(V1),isNeList(V2)))	(109)
mark^#(e)	→	active^#(e)	(110)
active^#(isNeList(__(V1,V2)))	→	isList^#(V1)	(111)
mark^#(nil)	→	active^#(nil)	(112)
active^#(isNePal(__(I,__(P,I))))	→	mark^#(and(isQid(I),isPal(P)))	(113)
active^#(__(__(X,Y),Z))	→	__^#(Y,Z)	(114)
mark^#(__(X1,X2))	→	__^#(mark(X1),mark(X2))	(115)
active^#(isNePal(V))	→	mark^#(isQid(V))	(116)
active^#(isPal(V))	→	isNePal^#(V)	(117)
mark^#(a)	→	active^#(a)	(118)
active^#(__(X,nil))	→	mark^#(X)	(119)
mark^#(and(X1,X2))	→	and^#(mark(X1),X2)	(120)
__^#(X1,active(X2))	→	__^#(X1,X2)	(121)
active^#(isPal(V))	→	mark^#(isNePal(V))	(122)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(123)
active^#(isList(V))	→	isNeList^#(V)	(124)
active^#(isNeList(__(V1,V2)))	→	and^#(isList(V1),isNeList(V2))	(125)

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

The 1^st component contains the pair

mark^#(isPal(X))	→	active^#(isPal(X))	(91)
active^#(isList(V))	→	mark^#(isNeList(V))	(92)
active^#(isPal(V))	→	mark^#(isNePal(V))	(122)
active^#(isNeList(V))	→	mark^#(isQid(V))	(84)
active^#(__(X,nil))	→	mark^#(X)	(119)
mark^#(isList(X))	→	active^#(isList(X))	(82)
active^#(isNePal(V))	→	mark^#(isQid(V))	(116)
mark^#(isNePal(X))	→	active^#(isNePal(X))	(79)
active^#(isNePal(__(I,__(P,I))))	→	mark^#(and(isQid(I),isPal(P)))	(113)
active^#(isNeList(__(V1,V2)))	→	mark^#(and(isList(V1),isNeList(V2)))	(109)
mark^#(and(X1,X2))	→	mark^#(X1)	(72)
mark^#(isQid(X))	→	active^#(isQid(X))	(68)
mark^#(__(X1,X2))	→	mark^#(X2)	(69)
mark^#(isNeList(X))	→	active^#(isNeList(X))	(106)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(63)
active^#(__(nil,X))	→	mark^#(X)	(103)
active^#(isNeList(__(V1,V2)))	→	mark^#(and(isNeList(V1),isList(V2)))	(102)
active^#(and(tt,X))	→	mark^#(X)	(100)
mark^#(__(X1,X2))	→	mark^#(X1)	(60)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(56)
active^#(isList(__(V1,V2)))	→	mark^#(and(isList(V1),isList(V2)))	(96)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(55)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	1
[isNeList(x₁)]	=	2
[isPal(x₁)]	=	2
[u]	=	1
[and(x₁, x₂)]	=	2
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	2
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	1
[o]	=	1
[mark^#(x₁)]	=	2
[isList(x₁)]	=	2
[isNePal^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[i]	=	1
[e]	=	1
[active(x₁)]	=	4
[active^#(x₁)]	=	x₁ + 0
[tt]	=	4
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	2

together with the usable rules

isPal(mark(X))	→	isPal(X)	(50)
__(active(X1),X2)	→	__(X1,X2)	(36)
__(mark(X1),X2)	→	__(X1,X2)	(34)
isNeList(mark(X))	→	isNeList(X)	(44)
and(X1,mark(X2))	→	and(X1,X2)	(39)
isNePal(active(X))	→	isNePal(X)	(49)
isNeList(active(X))	→	isNeList(X)	(45)
isPal(active(X))	→	isPal(X)	(51)
and(active(X1),X2)	→	and(X1,X2)	(40)
and(mark(X1),X2)	→	and(X1,X2)	(38)
isNePal(mark(X))	→	isNePal(X)	(48)
isQid(active(X))	→	isQid(X)	(47)
__(X1,active(X2))	→	__(X1,X2)	(37)
and(X1,active(X2))	→	and(X1,X2)	(41)
isList(mark(X))	→	isList(X)	(42)
isQid(mark(X))	→	isQid(X)	(46)
__(X1,mark(X2))	→	__(X1,X2)	(35)
isList(active(X))	→	isList(X)	(43)

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

mark^#(isQid(X))

→

active^#(isQid(X))

(68)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(and(tt,X))	→	mark^#(X)	(100)
active^#(isNeList(V))	→	mark^#(isQid(V))	(84)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(56)
active^#(__(nil,X))	→	mark^#(X)	(103)
mark^#(isNePal(X))	→	active^#(isNePal(X))	(79)
mark^#(and(X1,X2))	→	mark^#(X1)	(72)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(63)
mark^#(isPal(X))	→	active^#(isPal(X))	(91)
active^#(isList(V))	→	mark^#(isNeList(V))	(92)
active^#(isNeList(__(V1,V2)))	→	mark^#(and(isNeList(V1),isList(V2)))	(102)
active^#(isList(__(V1,V2)))	→	mark^#(and(isList(V1),isList(V2)))	(96)
mark^#(__(X1,X2))	→	mark^#(X2)	(69)
mark^#(__(X1,X2))	→	mark^#(X1)	(60)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(55)
mark^#(isNeList(X))	→	active^#(isNeList(X))	(106)
active^#(isNePal(__(I,__(P,I))))	→	mark^#(and(isQid(I),isPal(P)))	(113)
mark^#(isList(X))	→	active^#(isList(X))	(82)
active^#(isNePal(V))	→	mark^#(isQid(V))	(116)
active^#(isNeList(__(V1,V2)))	→	mark^#(and(isList(V1),isNeList(V2)))	(109)
active^#(isPal(V))	→	mark^#(isNePal(V))	(122)
active^#(__(X,nil))	→	mark^#(X)	(119)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	1
[isNeList(x₁)]	=	x₁ + 34106
[isPal(x₁)]	=	x₁ + 34107
[u]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 12330
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 34106
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	34105
[o]	=	0
[mark^#(x₁)]	=	x₁ + 0
[isList(x₁)]	=	x₁ + 34107
[isNePal^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 0
[isList^#(x₁)]	=	0
[i]	=	16468
[e]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[tt]	=	584
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 46438

together with the usable rules

active(isQid(o))	→	mark(tt)	(18)
isPal(mark(X))	→	isPal(X)	(50)
active(and(tt,X))	→	mark(X)	(4)
active(isQid(a))	→	mark(tt)	(15)
active(isNeList(V))	→	mark(isQid(V))	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
active(isQid(e))	→	mark(tt)	(16)
mark(nil)	→	active(nil)	(21)
__(active(X1),X2)	→	__(X1,X2)	(36)
mark(isQid(X))	→	active(isQid(X))	(26)
active(isQid(u))	→	mark(tt)	(19)
mark(o)	→	active(o)	(32)
active(isQid(i))	→	mark(tt)	(17)
mark(isNePal(X))	→	active(isNePal(X))	(27)
__(mark(X1),X2)	→	__(X1,X2)	(34)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(22)
mark(isPal(X))	→	active(isPal(X))	(28)
isNeList(mark(X))	→	isNeList(X)	(44)
active(isList(V))	→	mark(isNeList(V))	(5)
mark(u)	→	active(u)	(33)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
and(X1,mark(X2))	→	and(X1,X2)	(39)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(20)
mark(isNeList(X))	→	active(isNeList(X))	(25)
isNePal(active(X))	→	isNePal(X)	(49)
mark(e)	→	active(e)	(30)
active(isPal(nil))	→	mark(tt)	(14)
mark(i)	→	active(i)	(31)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
isNeList(active(X))	→	isNeList(X)	(45)
mark(tt)	→	active(tt)	(23)
mark(isList(X))	→	active(isList(X))	(24)
active(isNePal(V))	→	mark(isQid(V))	(11)
active(isNeList(__(V1,V2)))	→	mark(and(isList(V1),isNeList(V2)))	(9)
active(isPal(V))	→	mark(isNePal(V))	(13)
isPal(active(X))	→	isPal(X)	(51)
and(active(X1),X2)	→	and(X1,X2)	(40)
active(isList(nil))	→	mark(tt)	(6)
and(mark(X1),X2)	→	and(X1,X2)	(38)
isNePal(mark(X))	→	isNePal(X)	(48)
isQid(active(X))	→	isQid(X)	(47)
__(X1,active(X2))	→	__(X1,X2)	(37)
and(X1,active(X2))	→	and(X1,X2)	(41)
isList(mark(X))	→	isList(X)	(42)
isQid(mark(X))	→	isQid(X)	(46)
__(X1,mark(X2))	→	__(X1,X2)	(35)
mark(a)	→	active(a)	(29)
isList(active(X))	→	isList(X)	(43)
active(__(X,nil))	→	mark(X)	(2)

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

active^#(and(tt,X))	→	mark^#(X)	(100)
active^#(isNeList(V))	→	mark^#(isQid(V))	(84)
active^#(__(nil,X))	→	mark^#(X)	(103)
mark^#(and(X1,X2))	→	mark^#(X1)	(72)
active^#(isList(V))	→	mark^#(isNeList(V))	(92)
active^#(isNeList(__(V1,V2)))	→	mark^#(and(isNeList(V1),isList(V2)))	(102)
active^#(isList(__(V1,V2)))	→	mark^#(and(isList(V1),isList(V2)))	(96)
mark^#(__(X1,X2))	→	mark^#(X2)	(69)
mark^#(__(X1,X2))	→	mark^#(X1)	(60)
active^#(isNePal(__(I,__(P,I))))	→	mark^#(and(isQid(I),isPal(P)))	(113)
active^#(isNePal(V))	→	mark^#(isQid(V))	(116)
active^#(isNeList(__(V1,V2)))	→	mark^#(and(isList(V1),isNeList(V2)))	(109)
active^#(isPal(V))	→	mark^#(isNePal(V))	(122)
active^#(__(X,nil))	→	mark^#(X)	(119)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(56)
mark^#(isNePal(X))	→	active^#(isNePal(X))	(79)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(63)
mark^#(isPal(X))	→	active^#(isPal(X))	(91)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(55)
mark^#(isNeList(X))	→	active^#(isNeList(X))	(106)
mark^#(isList(X))	→	active^#(isList(X))	(82)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	1
[isNeList(x₁)]	=	1
[isPal(x₁)]	=	625
[u]	=	1
[and(x₁, x₂)]	=	7066
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	2034
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	1
[o]	=	1
[mark^#(x₁)]	=	25537
[isList(x₁)]	=	25536
[isNePal^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	1
[isList^#(x₁)]	=	0
[i]	=	12330
[e]	=	0
[active(x₁)]	=	1
[active^#(x₁)]	=	x₁ + 0
[tt]	=	0
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	25537

together with the usable rules

active(isQid(o))	→	mark(tt)	(18)
isPal(mark(X))	→	isPal(X)	(50)
active(and(tt,X))	→	mark(X)	(4)
active(isQid(a))	→	mark(tt)	(15)
active(isNeList(V))	→	mark(isQid(V))	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
active(isQid(e))	→	mark(tt)	(16)
mark(nil)	→	active(nil)	(21)
__(active(X1),X2)	→	__(X1,X2)	(36)
mark(isQid(X))	→	active(isQid(X))	(26)
active(isQid(u))	→	mark(tt)	(19)
mark(o)	→	active(o)	(32)
active(isQid(i))	→	mark(tt)	(17)
mark(isNePal(X))	→	active(isNePal(X))	(27)
__(mark(X1),X2)	→	__(X1,X2)	(34)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(22)
mark(isPal(X))	→	active(isPal(X))	(28)
isNeList(mark(X))	→	isNeList(X)	(44)
active(isList(V))	→	mark(isNeList(V))	(5)
mark(u)	→	active(u)	(33)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
and(X1,mark(X2))	→	and(X1,X2)	(39)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(20)
mark(isNeList(X))	→	active(isNeList(X))	(25)
isNePal(active(X))	→	isNePal(X)	(49)
mark(e)	→	active(e)	(30)
active(isPal(nil))	→	mark(tt)	(14)
mark(i)	→	active(i)	(31)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
isNeList(active(X))	→	isNeList(X)	(45)
mark(tt)	→	active(tt)	(23)
mark(isList(X))	→	active(isList(X))	(24)
active(isNePal(V))	→	mark(isQid(V))	(11)
active(isNeList(__(V1,V2)))	→	mark(and(isList(V1),isNeList(V2)))	(9)
active(isPal(V))	→	mark(isNePal(V))	(13)
isPal(active(X))	→	isPal(X)	(51)
and(active(X1),X2)	→	and(X1,X2)	(40)
active(isList(nil))	→	mark(tt)	(6)
and(mark(X1),X2)	→	and(X1,X2)	(38)
isNePal(mark(X))	→	isNePal(X)	(48)
isQid(active(X))	→	isQid(X)	(47)
__(X1,active(X2))	→	__(X1,X2)	(37)
and(X1,active(X2))	→	and(X1,X2)	(41)
isList(mark(X))	→	isList(X)	(42)
isQid(mark(X))	→	isQid(X)	(46)
__(X1,mark(X2))	→	__(X1,X2)	(35)
mark(a)	→	active(a)	(29)
isList(active(X))	→	isList(X)	(43)
active(__(X,nil))	→	mark(X)	(2)

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

mark^#(isNePal(X))	→	active^#(isNePal(X))	(79)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(63)
mark^#(isPal(X))	→	active^#(isPal(X))	(91)
mark^#(isNeList(X))	→	active^#(isNeList(X))	(106)
mark^#(isList(X))	→	active^#(isList(X))	(82)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(56)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(55)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(and)	=	2
π(__^#)	=	1
π(isNePal^#)	=	1
π(mark)	=	1
π(isList^#)	=	1
π(active)	=	1
π(active^#)	=	1
π(and^#)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(a)	=	3	status(a)	=	[]	list-extension(a)	=	Lex
prec(isNeList)	=	0	status(isNeList)	=	[]	list-extension(isNeList)	=	Lex
prec(isPal)	=	2	status(isPal)	=	[]	list-extension(isPal)	=	Lex
prec(u)	=	3	status(u)	=	[]	list-extension(u)	=	Lex
prec(isNeList^#)	=	0	status(isNeList^#)	=	[]	list-extension(isNeList^#)	=	Lex
prec(isNePal)	=	2	status(isNePal)	=	[]	list-extension(isNePal)	=	Lex
prec(isQid^#)	=	0	status(isQid^#)	=	[]	list-extension(isQid^#)	=	Lex
prec(isPal^#)	=	0	status(isPal^#)	=	[]	list-extension(isPal^#)	=	Lex
prec(isQid)	=	0	status(isQid)	=	[]	list-extension(isQid)	=	Lex
prec(o)	=	2	status(o)	=	[]	list-extension(o)	=	Lex
prec(mark^#)	=	1	status(mark^#)	=	[1]	list-extension(mark^#)	=	Lex
prec(isList)	=	0	status(isList)	=	[]	list-extension(isList)	=	Lex
prec(nil)	=	1	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(i)	=	2	status(i)	=	[]	list-extension(i)	=	Lex
prec(e)	=	3	status(e)	=	[]	list-extension(e)	=	Lex
prec(tt)	=	0	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(__)	=	2	status(__)	=	[1, 2]	list-extension(__)	=	Lex

and the following Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	0
[isPal(x₁)]	=	0
[u]	=	0
[isNeList^#(x₁)]	=	0
[isNePal(x₁)]	=	0
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	0
[o]	=	0
[mark^#(x₁)]	=	x₁ + 0
[isList(x₁)]	=	0
[nil]	=	0
[i]	=	0
[e]	=	0
[tt]	=	0
[__(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)

together with the usable rules

active(isQid(o))	→	mark(tt)	(18)
isPal(mark(X))	→	isPal(X)	(50)
active(and(tt,X))	→	mark(X)	(4)
active(isQid(a))	→	mark(tt)	(15)
active(isNeList(V))	→	mark(isQid(V))	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
active(isQid(e))	→	mark(tt)	(16)
mark(nil)	→	active(nil)	(21)
__(active(X1),X2)	→	__(X1,X2)	(36)
mark(isQid(X))	→	active(isQid(X))	(26)
active(isQid(u))	→	mark(tt)	(19)
mark(o)	→	active(o)	(32)
active(isQid(i))	→	mark(tt)	(17)
mark(isNePal(X))	→	active(isNePal(X))	(27)
__(mark(X1),X2)	→	__(X1,X2)	(34)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(22)
mark(isPal(X))	→	active(isPal(X))	(28)
isNeList(mark(X))	→	isNeList(X)	(44)
active(isList(V))	→	mark(isNeList(V))	(5)
mark(u)	→	active(u)	(33)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
and(X1,mark(X2))	→	and(X1,X2)	(39)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(20)
mark(isNeList(X))	→	active(isNeList(X))	(25)
isNePal(active(X))	→	isNePal(X)	(49)
mark(e)	→	active(e)	(30)
active(isPal(nil))	→	mark(tt)	(14)
mark(i)	→	active(i)	(31)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
isNeList(active(X))	→	isNeList(X)	(45)
mark(tt)	→	active(tt)	(23)
mark(isList(X))	→	active(isList(X))	(24)
active(isNePal(V))	→	mark(isQid(V))	(11)
active(isNeList(__(V1,V2)))	→	mark(and(isList(V1),isNeList(V2)))	(9)
active(isPal(V))	→	mark(isNePal(V))	(13)
isPal(active(X))	→	isPal(X)	(51)
and(active(X1),X2)	→	and(X1,X2)	(40)
active(isList(nil))	→	mark(tt)	(6)
and(mark(X1),X2)	→	and(X1,X2)	(38)
isNePal(mark(X))	→	isNePal(X)	(48)
isQid(active(X))	→	isQid(X)	(47)
__(X1,active(X2))	→	__(X1,X2)	(37)
and(X1,active(X2))	→	and(X1,X2)	(41)
isList(mark(X))	→	isList(X)	(42)
isQid(mark(X))	→	isQid(X)	(46)
__(X1,mark(X2))	→	__(X1,X2)	(35)
mark(a)	→	active(a)	(29)
isList(active(X))	→	isList(X)	(43)
active(__(X,nil))	→	mark(X)	(2)

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

active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(56)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(55)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

isNePal^#(active(X))	→	isNePal^#(X)	(99)
isNePal^#(mark(X))	→	isNePal^#(X)	(97)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	437
[isPal(x₁)]	=	0
[u]	=	0
[and(x₁, x₂)]	=	0
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	1
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	32573
[o]	=	0
[mark^#(x₁)]	=	0
[isList(x₁)]	=	0
[isNePal^#(x₁)]	=	x₁ + 0
[nil]	=	25532
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[i]	=	14459
[e]	=	29273
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	0
[tt]	=	32575
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	59112

together with the usable rules

isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)

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

isNePal^#(active(X))	→	isNePal^#(X)	(99)
isNePal^#(mark(X))	→	isNePal^#(X)	(97)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

__^#(X1,mark(X2))	→	__^#(X1,X2)	(123)
__^#(active(X1),X2)	→	__^#(X1,X2)	(89)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(87)
__^#(X1,active(X2))	→	__^#(X1,X2)	(121)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	21096
[isPal(x₁)]	=	0
[u]	=	0
[and(x₁, x₂)]	=	0
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	x₁ + x₂ + 0
[isNePal(x₁)]	=	1
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	32573
[o]	=	0
[mark^#(x₁)]	=	0
[isList(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	25532
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[i]	=	5592
[e]	=	29273
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	0
[tt]	=	32575
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	59112

together with the usable rules

isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)

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

__^#(X1,mark(X2))	→	__^#(X1,X2)	(123)
__^#(active(X1),X2)	→	__^#(X1,X2)	(89)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(87)
__^#(X1,active(X2))	→	__^#(X1,X2)	(121)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

isQid^#(active(X))	→	isQid^#(X)	(77)
isQid^#(mark(X))	→	isQid^#(X)	(101)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	15082
[isPal(x₁)]	=	0
[u]	=	0
[and(x₁, x₂)]	=	0
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	1
[isQid^#(x₁)]	=	x₁ + 0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	16146
[o]	=	0
[mark^#(x₁)]	=	0
[isList(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	35774
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[i]	=	25011
[e]	=	23641
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	0
[tt]	=	16148
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	1

together with the usable rules

isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)

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

isQid^#(active(X))	→	isQid^#(X)	(77)
isQid^#(mark(X))	→	isQid^#(X)	(101)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

isPal^#(active(X))	→	isPal^#(X)	(88)
isPal^#(mark(X))	→	isPal^#(X)	(61)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	28472
[isPal(x₁)]	=	0
[u]	=	0
[and(x₁, x₂)]	=	0
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	1
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	x₁ + 0
[isQid(x₁)]	=	56944
[o]	=	0
[mark^#(x₁)]	=	0
[isList(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	11592
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[i]	=	52626
[e]	=	28255
[active(x₁)]	=	x₁ + 28472
[active^#(x₁)]	=	0
[tt]	=	85416
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	1

together with the usable rules

isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)

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

isPal^#(active(X))	→	isPal^#(X)	(88)
isPal^#(mark(X))	→	isPal^#(X)	(61)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

and^#(mark(X1),X2)	→	and^#(X1,X2)	(78)
and^#(active(X1),X2)	→	and^#(X1,X2)	(76)
and^#(X1,active(X2))	→	and^#(X1,X2)	(95)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(53)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	6438
[isPal(x₁)]	=	0
[u]	=	0
[and(x₁, x₂)]	=	0
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	1
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	26351
[o]	=	0
[mark^#(x₁)]	=	0
[isList(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	24928
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[i]	=	30968
[e]	=	28255
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	0
[tt]	=	26353
[and^#(x₁, x₂)]	=	x₂ + 0
[__(x₁, x₂)]	=	32157

together with the usable rules

isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)

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

and^#(X1,active(X2))	→	and^#(X1,X2)	(95)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(53)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

and^#(active(X1),X2)	→	and^#(X1,X2)	(76)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(78)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	14757
[isPal(x₁)]	=	0
[u]	=	0
[and(x₁, x₂)]	=	0
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	1
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	23613
[o]	=	0
[mark^#(x₁)]	=	0
[isList(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	37749
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[i]	=	15289
[e]	=	18841
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	0
[tt]	=	23615
[and^#(x₁, x₂)]	=	x₁ + 0
[__(x₁, x₂)]	=	32157

together with the usable rules

isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)

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

and^#(active(X1),X2)	→	and^#(X1,X2)	(76)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(78)

could be deleted.

1.1.6.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

isList^#(mark(X))	→	isList^#(X)	(70)
isList^#(active(X))	→	isList^#(X)	(52)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	30216
[isPal(x₁)]	=	0
[u]	=	0
[and(x₁, x₂)]	=	0
[isNeList^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	1
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	62219
[o]	=	0
[mark^#(x₁)]	=	0
[isList(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	12095
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	x₁ + 0
[i]	=	15289
[e]	=	24817
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	0
[tt]	=	62221
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	26557

together with the usable rules

isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)

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

isList^#(mark(X))	→	isList^#(X)	(70)
isList^#(active(X))	→	isList^#(X)	(52)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

isNeList^#(active(X))	→	isNeList^#(X)	(93)
isNeList^#(mark(X))	→	isNeList^#(X)	(75)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	24848
[isPal(x₁)]	=	0
[u]	=	0
[and(x₁, x₂)]	=	0
[isNeList^#(x₁)]	=	x₁ + 0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	1
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	24850
[o]	=	0
[mark^#(x₁)]	=	0
[isList(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	41566
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[i]	=	10883
[e]	=	22280
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	0
[tt]	=	24852
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	31675

together with the usable rules

isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)

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

isNeList^#(active(X))	→	isNeList^#(X)	(93)
isNeList^#(mark(X))	→	isNeList^#(X)	(75)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.