Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_C)

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)
active(__(X1,X2))	→	__(active(X1),X2)	(20)
active(__(X1,X2))	→	__(X1,active(X2))	(21)
active(and(X1,X2))	→	and(active(X1),X2)	(22)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(24)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
proper(nil)	→	ok(nil)	(27)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
proper(tt)	→	ok(tt)	(29)
proper(isList(X))	→	isList(proper(X))	(30)
proper(isNeList(X))	→	isNeList(proper(X))	(31)
proper(isQid(X))	→	isQid(proper(X))	(32)
proper(isNePal(X))	→	isNePal(proper(X))	(33)
proper(isPal(X))	→	isPal(proper(X))	(34)
proper(a)	→	ok(a)	(35)
proper(e)	→	ok(e)	(36)
proper(i)	→	ok(i)	(37)
proper(o)	→	ok(o)	(38)
proper(u)	→	ok(u)	(39)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isNeList(ok(X))	→	ok(isNeList(X))	(43)
isQid(ok(X))	→	ok(isQid(X))	(44)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
isPal(ok(X))	→	ok(isPal(X))	(46)
top(mark(X))	→	top(proper(X))	(47)
top(ok(X))	→	top(active(X))	(48)

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.

isPal^#(ok(X))	→	isPal^#(X)	(49)
proper^#(isPal(X))	→	isPal^#(proper(X))	(50)
active^#(isList(__(V1,V2)))	→	isList^#(V1)	(51)
proper^#(isNePal(X))	→	proper^#(X)	(52)
proper^#(isQid(X))	→	proper^#(X)	(53)
active^#(and(X1,X2))	→	active^#(X1)	(54)
active^#(and(X1,X2))	→	and^#(active(X1),X2)	(55)
isQid^#(ok(X))	→	isQid^#(X)	(56)
proper^#(__(X1,X2))	→	__^#(proper(X1),proper(X2))	(57)
active^#(__(__(X,Y),Z))	→	__^#(Y,Z)	(58)
proper^#(__(X1,X2))	→	proper^#(X1)	(59)
proper^#(and(X1,X2))	→	and^#(proper(X1),proper(X2))	(60)
top^#(mark(X))	→	proper^#(X)	(61)
proper^#(and(X1,X2))	→	proper^#(X2)	(62)
active^#(__(X1,X2))	→	active^#(X2)	(63)
active^#(isNeList(__(V1,V2)))	→	isNeList^#(V2)	(64)
__^#(ok(X1),ok(X2))	→	__^#(X1,X2)	(65)
active^#(isNeList(__(V1,V2)))	→	and^#(isList(V1),isNeList(V2))	(66)
proper^#(isList(X))	→	proper^#(X)	(67)
proper^#(isList(X))	→	isList^#(proper(X))	(68)
proper^#(isQid(X))	→	isQid^#(proper(X))	(69)
active^#(isNeList(__(V1,V2)))	→	isList^#(V1)	(70)
active^#(isNeList(__(V1,V2)))	→	and^#(isNeList(V1),isList(V2))	(71)
active^#(isNePal(V))	→	isQid^#(V)	(72)
active^#(isList(__(V1,V2)))	→	isList^#(V2)	(73)
active^#(__(__(X,Y),Z))	→	__^#(X,__(Y,Z))	(74)
proper^#(__(X1,X2))	→	proper^#(X2)	(75)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(76)
active^#(isNePal(__(I,__(P,I))))	→	isPal^#(P)	(77)
top^#(ok(X))	→	top^#(active(X))	(78)
proper^#(and(X1,X2))	→	proper^#(X1)	(79)
active^#(isPal(V))	→	isNePal^#(V)	(80)
active^#(isNeList(__(V1,V2)))	→	isList^#(V2)	(81)
top^#(mark(X))	→	top^#(proper(X))	(82)
proper^#(isPal(X))	→	proper^#(X)	(83)
active^#(isList(__(V1,V2)))	→	and^#(isList(V1),isList(V2))	(84)
proper^#(isNeList(X))	→	proper^#(X)	(85)
proper^#(isNePal(X))	→	isNePal^#(proper(X))	(86)
active^#(__(X1,X2))	→	active^#(X1)	(87)
isNePal^#(ok(X))	→	isNePal^#(X)	(88)
active^#(isNeList(__(V1,V2)))	→	isNeList^#(V1)	(89)
active^#(isNePal(__(I,__(P,I))))	→	isQid^#(I)	(90)
active^#(__(X1,X2))	→	__^#(active(X1),X2)	(91)
active^#(isList(V))	→	isNeList^#(V)	(92)
proper^#(isNeList(X))	→	isNeList^#(proper(X))	(93)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(94)
isList^#(ok(X))	→	isList^#(X)	(95)
isNeList^#(ok(X))	→	isNeList^#(X)	(96)
active^#(isNeList(V))	→	isQid^#(V)	(97)
top^#(ok(X))	→	active^#(X)	(98)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(99)
and^#(ok(X1),ok(X2))	→	and^#(X1,X2)	(100)
active^#(__(X1,X2))	→	__^#(X1,active(X2))	(101)
active^#(isNePal(__(I,__(P,I))))	→	and^#(isQid(I),isPal(P))	(102)

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

The 1^st component contains the pair

top^#(mark(X))	→	top^#(proper(X))	(82)
top^#(ok(X))	→	top^#(active(X))	(78)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(top^#)	=	1
π(__^#)	=	2
π(proper)	=	1
π(ok)	=	1
π(active)	=	1

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

prec(a)	=	6	status(a)	=	[]	list-extension(a)	=	Lex
prec(isNeList)	=	6	status(isNeList)	=	[1]	list-extension(isNeList)	=	Lex
prec(isPal)	=	8	status(isPal)	=	[1]	list-extension(isPal)	=	Lex
prec(u)	=	4	status(u)	=	[]	list-extension(u)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(and)	=	6	status(and)	=	[2, 1]	list-extension(and)	=	Lex
prec(isNeList^#)	=	0	status(isNeList^#)	=	[]	list-extension(isNeList^#)	=	Lex
prec(isNePal)	=	6	status(isNePal)	=	[1]	list-extension(isNePal)	=	Lex
prec(isQid^#)	=	0	status(isQid^#)	=	[]	list-extension(isQid^#)	=	Lex
prec(isPal^#)	=	0	status(isPal^#)	=	[]	list-extension(isPal^#)	=	Lex
prec(isQid)	=	6	status(isQid)	=	[]	list-extension(isQid)	=	Lex
prec(o)	=	4	status(o)	=	[]	list-extension(o)	=	Lex
prec(isList)	=	7	status(isList)	=	[1]	list-extension(isList)	=	Lex
prec(isNePal^#)	=	0	status(isNePal^#)	=	[]	list-extension(isNePal^#)	=	Lex
prec(nil)	=	6	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(mark)	=	5	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(isList^#)	=	0	status(isList^#)	=	[]	list-extension(isList^#)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(i)	=	4	status(i)	=	[]	list-extension(i)	=	Lex
prec(e)	=	4	status(e)	=	[]	list-extension(e)	=	Lex
prec(active^#)	=	0	status(active^#)	=	[]	list-extension(active^#)	=	Lex
prec(tt)	=	1	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(and^#)	=	0	status(and^#)	=	[2, 1]	list-extension(and^#)	=	Lex
prec(__)	=	8	status(__)	=	[1, 2]	list-extension(__)	=	Lex

and the following Max-polynomial interpretation

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

together with the usable rules

active(isQid(o))	→	mark(tt)	(18)
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)
active(__(X1,X2))	→	__(X1,active(X2))	(21)
proper(e)	→	ok(e)	(36)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
active(isQid(u))	→	mark(tt)	(19)
proper(isQid(X))	→	isQid(proper(X))	(32)
active(isQid(i))	→	mark(tt)	(17)
proper(nil)	→	ok(nil)	(27)
proper(isPal(X))	→	isPal(proper(X))	(34)
active(and(X1,X2))	→	and(active(X1),X2)	(22)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
isQid(ok(X))	→	ok(isQid(X))	(44)
active(isList(V))	→	mark(isNeList(V))	(5)
proper(isNePal(X))	→	isNePal(proper(X))	(33)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
proper(u)	→	ok(u)	(39)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
active(__(X1,X2))	→	__(active(X1),X2)	(20)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
proper(isList(X))	→	isList(proper(X))	(30)
active(isPal(nil))	→	mark(tt)	(14)
proper(isNeList(X))	→	isNeList(proper(X))	(31)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(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)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
active(isList(nil))	→	mark(tt)	(6)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isPal(ok(X))	→	ok(isPal(X))	(46)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)
active(__(X,nil))	→	mark(X)	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(82)

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

top^#(ok(X))

→

top^#(active(X))

(78)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(isQid(o))	→	mark(tt)	(18)
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)
active(__(X1,X2))	→	__(X1,active(X2))	(21)
proper(e)	→	ok(e)	(36)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
active(isQid(u))	→	mark(tt)	(19)
proper(isQid(X))	→	isQid(proper(X))	(32)
active(isQid(i))	→	mark(tt)	(17)
proper(nil)	→	ok(nil)	(27)
proper(isPal(X))	→	isPal(proper(X))	(34)
active(and(X1,X2))	→	and(active(X1),X2)	(22)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
isQid(ok(X))	→	ok(isQid(X))	(44)
active(isList(V))	→	mark(isNeList(V))	(5)
proper(isNePal(X))	→	isNePal(proper(X))	(33)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
proper(u)	→	ok(u)	(39)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
active(__(X1,X2))	→	__(active(X1),X2)	(20)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
proper(isList(X))	→	isList(proper(X))	(30)
active(isPal(nil))	→	mark(tt)	(14)
proper(isNeList(X))	→	isNeList(proper(X))	(31)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(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)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
active(isList(nil))	→	mark(tt)	(6)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isPal(ok(X))	→	ok(isPal(X))	(46)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)
active(__(X,nil))	→	mark(X)	(2)

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

top^#(ok(X))

→

top^#(active(X))

(78)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

active^#(__(X1,X2))	→	active^#(X2)	(63)
active^#(__(X1,X2))	→	active^#(X1)	(87)
active^#(and(X1,X2))	→	active^#(X1)	(54)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(isQid(o))	→	mark(tt)	(18)
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)
active(__(X1,X2))	→	__(X1,active(X2))	(21)
proper(e)	→	ok(e)	(36)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
active(isQid(u))	→	mark(tt)	(19)
proper(isQid(X))	→	isQid(proper(X))	(32)
active(isQid(i))	→	mark(tt)	(17)
proper(nil)	→	ok(nil)	(27)
proper(isPal(X))	→	isPal(proper(X))	(34)
active(and(X1,X2))	→	and(active(X1),X2)	(22)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
isQid(ok(X))	→	ok(isQid(X))	(44)
active(isList(V))	→	mark(isNeList(V))	(5)
proper(isNePal(X))	→	isNePal(proper(X))	(33)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
proper(u)	→	ok(u)	(39)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
active(__(X1,X2))	→	__(active(X1),X2)	(20)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
proper(isList(X))	→	isList(proper(X))	(30)
active(isPal(nil))	→	mark(tt)	(14)
proper(isNeList(X))	→	isNeList(proper(X))	(31)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(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)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
active(isList(nil))	→	mark(tt)	(6)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isPal(ok(X))	→	ok(isPal(X))	(46)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)
active(__(X,nil))	→	mark(X)	(2)

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

active^#(and(X1,X2))

→

active^#(X1)

(54)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(__(X1,X2))	→	active^#(X2)	(63)
active^#(__(X1,X2))	→	active^#(X1)	(87)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(isNeList(V))	→	mark(isQid(V))	(8)
proper(e)	→	ok(e)	(36)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
proper(isQid(X))	→	isQid(proper(X))	(32)
proper(nil)	→	ok(nil)	(27)
proper(isPal(X))	→	isPal(proper(X))	(34)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
isQid(ok(X))	→	ok(isQid(X))	(44)
proper(isNePal(X))	→	isNePal(proper(X))	(33)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
proper(isList(X))	→	isList(proper(X))	(30)
proper(isNeList(X))	→	isNeList(proper(X))	(31)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(24)
active(isNePal(V))	→	mark(isQid(V))	(11)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isPal(ok(X))	→	ok(isPal(X))	(46)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)

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

active^#(__(X1,X2))	→	active^#(X2)	(63)
active^#(__(X1,X2))	→	active^#(X1)	(87)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

proper^#(__(X1,X2))	→	proper^#(X2)	(75)
proper^#(isList(X))	→	proper^#(X)	(67)
proper^#(and(X1,X2))	→	proper^#(X2)	(62)
proper^#(__(X1,X2))	→	proper^#(X1)	(59)
proper^#(isNeList(X))	→	proper^#(X)	(85)
proper^#(isPal(X))	→	proper^#(X)	(83)
proper^#(isQid(X))	→	proper^#(X)	(53)
proper^#(and(X1,X2))	→	proper^#(X1)	(79)
proper^#(isNePal(X))	→	proper^#(X)	(52)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
proper(isQid(X))	→	isQid(proper(X))	(32)
proper(nil)	→	ok(nil)	(27)
proper(isPal(X))	→	isPal(proper(X))	(34)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
isQid(ok(X))	→	ok(isQid(X))	(44)
proper(isNePal(X))	→	isNePal(proper(X))	(33)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
proper(isList(X))	→	isList(proper(X))	(30)
proper(isNeList(X))	→	isNeList(proper(X))	(31)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(24)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isPal(ok(X))	→	ok(isPal(X))	(46)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)

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

proper^#(__(X1,X2))	→	proper^#(X2)	(75)
proper^#(and(X1,X2))	→	proper^#(X2)	(62)
proper^#(__(X1,X2))	→	proper^#(X1)	(59)
proper^#(isPal(X))	→	proper^#(X)	(83)
proper^#(and(X1,X2))	→	proper^#(X1)	(79)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

proper^#(isQid(X))	→	proper^#(X)	(53)
proper^#(isNePal(X))	→	proper^#(X)	(52)
proper^#(isList(X))	→	proper^#(X)	(67)
proper^#(isNeList(X))	→	proper^#(X)	(85)

1.1.3.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
proper(isQid(X))	→	isQid(proper(X))	(32)
proper(nil)	→	ok(nil)	(27)
proper(isPal(X))	→	isPal(proper(X))	(34)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
isQid(ok(X))	→	ok(isQid(X))	(44)
proper(isNePal(X))	→	isNePal(proper(X))	(33)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
proper(isList(X))	→	isList(proper(X))	(30)
proper(isNeList(X))	→	isNeList(proper(X))	(31)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(24)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isPal(ok(X))	→	ok(isPal(X))	(46)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)

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

proper^#(isNePal(X))	→	proper^#(X)	(52)
proper^#(isNeList(X))	→	proper^#(X)	(85)

could be deleted.

1.1.3.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

proper^#(isQid(X))	→	proper^#(X)	(53)
proper^#(isList(X))	→	proper^#(X)	(67)

1.1.3.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(26)
proper(isQid(X))	→	isQid(proper(X))	(32)
proper(nil)	→	ok(nil)	(27)
proper(isPal(X))	→	isPal(proper(X))	(34)
proper(and(X1,X2))	→	and(proper(X1),proper(X2))	(28)
isQid(ok(X))	→	ok(isQid(X))	(44)
proper(isNePal(X))	→	isNePal(proper(X))	(33)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
proper(isList(X))	→	isList(proper(X))	(30)
proper(isNeList(X))	→	isNeList(proper(X))	(31)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(24)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isPal(ok(X))	→	ok(isPal(X))	(46)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)

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

proper^#(isQid(X))	→	proper^#(X)	(53)
proper^#(isList(X))	→	proper^#(X)	(67)

could be deleted.

1.1.3.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

isNeList^#(ok(X))

→

isNeList^#(X)

(96)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(nil)	→	ok(nil)	(27)
isQid(ok(X))	→	ok(isQid(X))	(44)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(24)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)

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

isNeList^#(ok(X))

→

isNeList^#(X)

(96)

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

isNePal^#(ok(X))

→

isNePal^#(X)

(88)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(nil)	→	ok(nil)	(27)
isQid(ok(X))	→	ok(isQid(X))	(44)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(24)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)

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

isNePal^#(ok(X))

→

isNePal^#(X)

(88)

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)	(76)
and^#(ok(X1),ok(X2))	→	and^#(X1,X2)	(100)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(nil)	→	ok(nil)	(27)
isQid(ok(X))	→	ok(isQid(X))	(44)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
__(mark(X1),X2)	→	mark(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(24)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(40)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)
isNeList(ok(X))	→	ok(isNeList(X))	(43)

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

and^#(ok(X1),ok(X2))

→

and^#(X1,X2)

(100)

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^#(mark(X1),X2)

→

and^#(X1,X2)

(76)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(nil)	→	ok(nil)	(27)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)

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

and^#(mark(X1),X2)

→

and^#(X1,X2)

(76)

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

isQid^#(ok(X))

→

isQid^#(X)

(56)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	x₁ + 1
[isPal(x₁)]	=	1
[u]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[isNeList^#(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 0
[isQid^#(x₁)]	=	x₁ + 0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	19458
[o]	=	0
[proper(x₁)]	=	19457
[ok(x₁)]	=	x₁ + 1
[isList(x₁)]	=	x₁ + 1
[isNePal^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[isList^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[i]	=	11028
[e]	=	19456
[active(x₁)]	=	19461
[active^#(x₁)]	=	0
[tt]	=	1
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(nil)	→	ok(nil)	(27)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)

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

isQid^#(ok(X))

→

isQid^#(X)

(56)

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

__^#(X1,mark(X2))	→	__^#(X1,X2)	(99)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(94)
__^#(ok(X1),ok(X2))	→	__^#(X1,X2)	(65)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(nil)	→	ok(nil)	(27)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)

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

__^#(X1,mark(X2))	→	__^#(X1,X2)	(99)
__^#(ok(X1),ok(X2))	→	__^#(X1,X2)	(65)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

__^#(mark(X1),X2)

→

__^#(X1,X2)

(94)

1.1.8.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

proper(e)	→	ok(e)	(36)
proper(nil)	→	ok(nil)	(27)
proper(u)	→	ok(u)	(39)
and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
isNePal(ok(X))	→	ok(isNePal(X))	(45)
proper(o)	→	ok(o)	(38)
proper(i)	→	ok(i)	(37)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
proper(a)	→	ok(a)	(35)
proper(tt)	→	ok(tt)	(29)

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

__^#(mark(X1),X2)

→

__^#(X1,X2)

(94)

could be deleted.

1.1.8.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

isList^#(ok(X))

→

isList^#(X)

(95)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[isNeList(x₁)]	=	x₁ + 1
[isPal(x₁)]	=	1
[u]	=	0
[top(x₁)]	=	0
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[isNeList^#(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 0
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	0
[isQid(x₁)]	=	17028
[o]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[isList(x₁)]	=	x₁ + 2631
[isNePal^#(x₁)]	=	0
[nil]	=	30479
[mark(x₁)]	=	x₁ + 38373
[isList^#(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[i]	=	1
[e]	=	1
[active(x₁)]	=	55401
[active^#(x₁)]	=	0
[tt]	=	17029
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

and(mark(X1),X2)	→	mark(and(X1,X2))	(25)
and(ok(X1),ok(X2))	→	ok(and(X1,X2))	(41)
isList(ok(X))	→	ok(isList(X))	(42)
isNeList(ok(X))	→	ok(isNeList(X))	(43)

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

isList^#(ok(X))

→

isList^#(X)

(95)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

isPal^#(ok(X))

→

isPal^#(X)

(49)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	1
[isNeList(x₁)]	=	2
[isPal(x₁)]	=	3011
[u]	=	29191
[top(x₁)]	=	0
[and(x₁, x₂)]	=	3
[isNeList^#(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	19504
[isQid^#(x₁)]	=	0
[isPal^#(x₁)]	=	x₁ + 0
[isQid(x₁)]	=	28580
[o]	=	28252
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 2
[isList(x₁)]	=	13856
[isNePal^#(x₁)]	=	0
[nil]	=	21885
[mark(x₁)]	=	4
[isList^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[i]	=	3103
[e]	=	32755
[active(x₁)]	=	1
[active^#(x₁)]	=	0
[tt]	=	17029
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	2

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair

isPal^#(ok(X))

→

isPal^#(X)

(49)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 0 components.