Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_complete_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,V)	→	a__U12(a__isNeList(V))	(4)
a__U12(tt)	→	tt	(5)
a__U21(tt,V1,V2)	→	a__U22(a__isList(V1),V2)	(6)
a__U22(tt,V2)	→	a__U23(a__isList(V2))	(7)
a__U23(tt)	→	tt	(8)
a__U31(tt,V)	→	a__U32(a__isQid(V))	(9)
a__U32(tt)	→	tt	(10)
a__U41(tt,V1,V2)	→	a__U42(a__isList(V1),V2)	(11)
a__U42(tt,V2)	→	a__U43(a__isNeList(V2))	(12)
a__U43(tt)	→	tt	(13)
a__U51(tt,V1,V2)	→	a__U52(a__isNeList(V1),V2)	(14)
a__U52(tt,V2)	→	a__U53(a__isList(V2))	(15)
a__U53(tt)	→	tt	(16)
a__U61(tt,V)	→	a__U62(a__isQid(V))	(17)
a__U62(tt)	→	tt	(18)
a__U71(tt,V)	→	a__U72(a__isNePal(V))	(19)
a__U72(tt)	→	tt	(20)
a__and(tt,X)	→	mark(X)	(21)
a__isList(V)	→	a__U11(a__isPalListKind(V),V)	(22)
a__isList(nil)	→	tt	(23)
a__isList(__(V1,V2))	→	a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(24)
a__isNeList(V)	→	a__U31(a__isPalListKind(V),V)	(25)
a__isNeList(__(V1,V2))	→	a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(26)
a__isNeList(__(V1,V2))	→	a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(27)
a__isNePal(V)	→	a__U61(a__isPalListKind(V),V)	(28)
a__isNePal(__(I,__(P,I)))	→	a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(29)
a__isPal(V)	→	a__U71(a__isPalListKind(V),V)	(30)
a__isPal(nil)	→	tt	(31)
a__isPalListKind(a)	→	tt	(32)
a__isPalListKind(e)	→	tt	(33)
a__isPalListKind(i)	→	tt	(34)
a__isPalListKind(nil)	→	tt	(35)
a__isPalListKind(o)	→	tt	(36)
a__isPalListKind(u)	→	tt	(37)
a__isPalListKind(__(V1,V2))	→	a__and(a__isPalListKind(V1),isPalListKind(V2))	(38)
a__isQid(a)	→	tt	(39)
a__isQid(e)	→	tt	(40)
a__isQid(i)	→	tt	(41)
a__isQid(o)	→	tt	(42)
a__isQid(u)	→	tt	(43)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(44)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(45)
mark(U12(X))	→	a__U12(mark(X))	(46)
mark(isNeList(X))	→	a__isNeList(X)	(47)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(48)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(49)
mark(isList(X))	→	a__isList(X)	(50)
mark(U23(X))	→	a__U23(mark(X))	(51)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(52)
mark(U32(X))	→	a__U32(mark(X))	(53)
mark(isQid(X))	→	a__isQid(X)	(54)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(55)
mark(U42(X1,X2))	→	a__U42(mark(X1),X2)	(56)
mark(U43(X))	→	a__U43(mark(X))	(57)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(58)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(59)
mark(U53(X))	→	a__U53(mark(X))	(60)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(61)
mark(U62(X))	→	a__U62(mark(X))	(62)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(63)
mark(U72(X))	→	a__U72(mark(X))	(64)
mark(isNePal(X))	→	a__isNePal(X)	(65)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(66)
mark(isPalListKind(X))	→	a__isPalListKind(X)	(67)
mark(isPal(X))	→	a__isPal(X)	(68)
mark(nil)	→	nil	(69)
mark(tt)	→	tt	(70)
mark(a)	→	a	(71)
mark(e)	→	e	(72)
mark(i)	→	i	(73)
mark(o)	→	o	(74)
mark(u)	→	u	(75)
a____(X1,X2)	→	__(X1,X2)	(76)
a__U11(X1,X2)	→	U11(X1,X2)	(77)
a__U12(X)	→	U12(X)	(78)
a__isNeList(X)	→	isNeList(X)	(79)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(80)
a__U22(X1,X2)	→	U22(X1,X2)	(81)
a__isList(X)	→	isList(X)	(82)
a__U23(X)	→	U23(X)	(83)
a__U31(X1,X2)	→	U31(X1,X2)	(84)
a__U32(X)	→	U32(X)	(85)
a__isQid(X)	→	isQid(X)	(86)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(87)
a__U42(X1,X2)	→	U42(X1,X2)	(88)
a__U43(X)	→	U43(X)	(89)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(90)
a__U52(X1,X2)	→	U52(X1,X2)	(91)
a__U53(X)	→	U53(X)	(92)
a__U61(X1,X2)	→	U61(X1,X2)	(93)
a__U62(X)	→	U62(X)	(94)
a__U71(X1,X2)	→	U71(X1,X2)	(95)
a__U72(X)	→	U72(X)	(96)
a__isNePal(X)	→	isNePal(X)	(97)
a__and(X1,X2)	→	and(X1,X2)	(98)
a__isPalListKind(X)	→	isPalListKind(X)	(99)
a__isPal(X)	→	isPal(X)	(100)

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.

a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(101)
a____^#(__(X,Y),Z)	→	mark^#(X)	(102)
mark^#(U42(X1,X2))	→	mark^#(X1)	(103)
a__U31^#(tt,V)	→	a__U32^#(a__isQid(V))	(104)
a__isList^#(__(V1,V2))	→	a__U21^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(105)
a__and^#(tt,X)	→	mark^#(X)	(106)
a__isList^#(V)	→	a__U11^#(a__isPalListKind(V),V)	(107)
mark^#(U62(X))	→	a__U62^#(mark(X))	(108)
mark^#(U42(X1,X2))	→	a__U42^#(mark(X1),X2)	(109)
mark^#(isList(X))	→	a__isList^#(X)	(110)
a__U42^#(tt,V2)	→	a__isNeList^#(V2)	(111)
a__isList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(112)
a__U52^#(tt,V2)	→	a__U53^#(a__isList(V2))	(113)
a__U61^#(tt,V)	→	a__U62^#(a__isQid(V))	(114)
mark^#(U62(X))	→	mark^#(X)	(115)
mark^#(U22(X1,X2))	→	mark^#(X1)	(116)
mark^#(U53(X))	→	a__U53^#(mark(X))	(117)
a__isPal^#(V)	→	a__U71^#(a__isPalListKind(V),V)	(118)
a__U71^#(tt,V)	→	a__U72^#(a__isNePal(V))	(119)
a__U61^#(tt,V)	→	a__isQid^#(V)	(120)
mark^#(U72(X))	→	a__U72^#(mark(X))	(121)
mark^#(__(X1,X2))	→	mark^#(X1)	(122)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(123)
mark^#(and(X1,X2))	→	mark^#(X1)	(124)
mark^#(U72(X))	→	mark^#(X)	(125)
a__isNeList^#(V)	→	a__isPalListKind^#(V)	(126)
a__isList^#(V)	→	a__isPalListKind^#(V)	(127)
a__U42^#(tt,V2)	→	a__U43^#(a__isNeList(V2))	(128)
mark^#(isQid(X))	→	a__isQid^#(X)	(129)
mark^#(U31(X1,X2))	→	mark^#(X1)	(130)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(131)
mark^#(isNeList(X))	→	a__isNeList^#(X)	(132)
mark^#(U32(X))	→	mark^#(X)	(133)
a__U22^#(tt,V2)	→	a__isList^#(V2)	(134)
a__U71^#(tt,V)	→	a__isNePal^#(V)	(135)
a__U11^#(tt,V)	→	a__isNeList^#(V)	(136)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(137)
a__isNeList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(138)
mark^#(U52(X1,X2))	→	mark^#(X1)	(139)
a__isNeList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(138)
mark^#(U71(X1,X2))	→	mark^#(X1)	(140)
a__U51^#(tt,V1,V2)	→	a__isNeList^#(V1)	(141)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(142)
mark^#(U21(X1,X2,X3))	→	a__U21^#(mark(X1),X2,X3)	(143)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isList(V1),V2)	(144)
a__isNeList^#(__(V1,V2))	→	a__U41^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(145)
a__U22^#(tt,V2)	→	a__U23^#(a__isList(V2))	(146)
a____^#(__(X,Y),Z)	→	mark^#(Z)	(147)
mark^#(isPal(X))	→	a__isPal^#(X)	(148)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(149)
mark^#(__(X1,X2))	→	mark^#(X2)	(150)
a__U31^#(tt,V)	→	a__isQid^#(V)	(151)
mark^#(U22(X1,X2))	→	a__U22^#(mark(X1),X2)	(152)
a__isPal^#(V)	→	a__isPalListKind^#(V)	(153)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(154)
a__U21^#(tt,V1,V2)	→	a__U22^#(a__isList(V1),V2)	(155)
a____^#(__(X,Y),Z)	→	mark^#(Y)	(156)
mark^#(U12(X))	→	a__U12^#(mark(X))	(157)
mark^#(U11(X1,X2))	→	mark^#(X1)	(158)
mark^#(U32(X))	→	a__U32^#(mark(X))	(159)
a__U52^#(tt,V2)	→	a__isList^#(V2)	(160)
a__U11^#(tt,V)	→	a__U12^#(a__isNeList(V))	(161)
a__isNePal^#(V)	→	a__U61^#(a__isPalListKind(V),V)	(162)
mark^#(U43(X))	→	a__U43^#(mark(X))	(163)
mark^#(U53(X))	→	mark^#(X)	(164)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(165)
a__U51^#(tt,V1,V2)	→	a__U52^#(a__isNeList(V1),V2)	(166)
a__isNePal^#(V)	→	a__isPalListKind^#(V)	(167)
mark^#(U23(X))	→	mark^#(X)	(168)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(169)
mark^#(U43(X))	→	mark^#(X)	(170)
a____^#(nil,X)	→	mark^#(X)	(171)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(172)
mark^#(U23(X))	→	a__U23^#(mark(X))	(173)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(174)
mark^#(U61(X1,X2))	→	mark^#(X1)	(175)
a__U41^#(tt,V1,V2)	→	a__isList^#(V1)	(176)
a__isPalListKind^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(177)
mark^#(isNePal(X))	→	a__isNePal^#(X)	(178)
mark^#(isPalListKind(X))	→	a__isPalListKind^#(X)	(179)
a____^#(__(X,Y),Z)	→	a____^#(mark(X),a____(mark(Y),mark(Z)))	(180)
a__isNeList^#(__(V1,V2))	→	a__U51^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(181)
a__isList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(182)
a__U21^#(tt,V1,V2)	→	a__isList^#(V1)	(183)
mark^#(U61(X1,X2))	→	a__U61^#(mark(X1),X2)	(184)
a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__isQid(I),isPalListKind(I))	(185)
mark^#(U71(X1,X2))	→	a__U71^#(mark(X1),X2)	(186)
a____^#(X,nil)	→	mark^#(X)	(187)
a__isNeList^#(V)	→	a__U31^#(a__isPalListKind(V),V)	(188)
mark^#(U12(X))	→	mark^#(X)	(189)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(190)
a__isNePal^#(__(I,__(P,I)))	→	a__isQid^#(I)	(191)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(142)
mark^#(U31(X1,X2))	→	a__U31^#(mark(X1),X2)	(192)
a__isPalListKind^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(193)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__isPalListKind^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(193)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(142)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(154)
mark^#(U22(X1,X2))	→	a__U22^#(mark(X1),X2)	(152)
a__isPal^#(V)	→	a__isPalListKind^#(V)	(153)
mark^#(__(X1,X2))	→	mark^#(X2)	(150)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(149)
mark^#(isPal(X))	→	a__isPal^#(X)	(148)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(190)
a____^#(__(X,Y),Z)	→	mark^#(Z)	(147)
a__isNeList^#(__(V1,V2))	→	a__U41^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(145)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isList(V1),V2)	(144)
mark^#(U21(X1,X2,X3))	→	a__U21^#(mark(X1),X2,X3)	(143)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(142)
mark^#(U12(X))	→	mark^#(X)	(189)
a__U51^#(tt,V1,V2)	→	a__isNeList^#(V1)	(141)
mark^#(U71(X1,X2))	→	mark^#(X1)	(140)
a__isNeList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(138)
a____^#(X,nil)	→	mark^#(X)	(187)
mark^#(U52(X1,X2))	→	mark^#(X1)	(139)
mark^#(U71(X1,X2))	→	a__U71^#(mark(X1),X2)	(186)
a__isNeList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(138)
a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__isQid(I),isPalListKind(I))	(185)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(137)
a__U11^#(tt,V)	→	a__isNeList^#(V)	(136)
a__U21^#(tt,V1,V2)	→	a__isList^#(V1)	(183)
a__U71^#(tt,V)	→	a__isNePal^#(V)	(135)
a__isList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(182)
a__U22^#(tt,V2)	→	a__isList^#(V2)	(134)
a__isNeList^#(__(V1,V2))	→	a__U51^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(181)
a____^#(__(X,Y),Z)	→	a____^#(mark(X),a____(mark(Y),mark(Z)))	(180)
mark^#(isPalListKind(X))	→	a__isPalListKind^#(X)	(179)
mark^#(U32(X))	→	mark^#(X)	(133)
mark^#(isNeList(X))	→	a__isNeList^#(X)	(132)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(131)
mark^#(isNePal(X))	→	a__isNePal^#(X)	(178)
mark^#(U31(X1,X2))	→	mark^#(X1)	(130)
a__U41^#(tt,V1,V2)	→	a__isList^#(V1)	(176)
a__isPalListKind^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(177)
mark^#(U61(X1,X2))	→	mark^#(X1)	(175)
a__isList^#(V)	→	a__isPalListKind^#(V)	(127)
a__isNeList^#(V)	→	a__isPalListKind^#(V)	(126)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(174)
mark^#(U72(X))	→	mark^#(X)	(125)
mark^#(and(X1,X2))	→	mark^#(X1)	(124)
mark^#(__(X1,X2))	→	mark^#(X1)	(122)
mark^#(U11(X1,X2))	→	a__U11^#(mark(X1),X2)	(123)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(172)
a____^#(nil,X)	→	mark^#(X)	(171)
mark^#(U43(X))	→	mark^#(X)	(170)
a__isPal^#(V)	→	a__U71^#(a__isPalListKind(V),V)	(118)
mark^#(U52(X1,X2))	→	a__U52^#(mark(X1),X2)	(169)
mark^#(U22(X1,X2))	→	mark^#(X1)	(116)
mark^#(U23(X))	→	mark^#(X)	(168)
a__isNePal^#(V)	→	a__isPalListKind^#(V)	(167)
mark^#(U62(X))	→	mark^#(X)	(115)
a__U51^#(tt,V1,V2)	→	a__U52^#(a__isNeList(V1),V2)	(166)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(165)
mark^#(U53(X))	→	mark^#(X)	(164)
a__isList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(112)
a__U42^#(tt,V2)	→	a__isNeList^#(V2)	(111)
mark^#(isList(X))	→	a__isList^#(X)	(110)
a__U52^#(tt,V2)	→	a__isList^#(V2)	(160)
mark^#(U42(X1,X2))	→	a__U42^#(mark(X1),X2)	(109)
a__and^#(tt,X)	→	mark^#(X)	(106)
a__isList^#(V)	→	a__U11^#(a__isPalListKind(V),V)	(107)
mark^#(U11(X1,X2))	→	mark^#(X1)	(158)
a____^#(__(X,Y),Z)	→	mark^#(Y)	(156)
a__isList^#(__(V1,V2))	→	a__U21^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(105)
a____^#(__(X,Y),Z)	→	mark^#(X)	(102)
mark^#(U42(X1,X2))	→	mark^#(X1)	(103)
a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(101)
a__U21^#(tt,V1,V2)	→	a__U22^#(a__isList(V1),V2)	(155)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	0
[a__isNePal^#(x₁)]	=	x₁ + 2
[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 4
[a__U72^#(x₁)]	=	0
[a__U71^#(x₁, x₂)]	=	x₂ + 2
[U11(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U31^#(x₁, x₂)]	=	0
[a__isNeList^#(x₁)]	=	x₁ + 4
[isNeList(x₁)]	=	x₁ + 2
[a__U23^#(x₁)]	=	0
[isPal(x₁)]	=	x₁ + 0
[U42(x₁, x₂)]	=	x₁ + x₂ + 2
[u]	=	26170
[U71(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U62(x₁)]	=	x₁ + 0
[and(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U43^#(x₁)]	=	0
[a__isPal^#(x₁)]	=	x₁ + 2
[U43(x₁)]	=	x₁ + 0
[a__U51^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 4
[U23(x₁)]	=	x₁ + 0
[a__U22(x₁, x₂)]	=	x₁ + x₂ + 2
[isNePal(x₁)]	=	x₁ + 0
[U72(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂)]	=	x₂ + 4
[a__U31(x₁, x₂)]	=	x₁ + 2
[a__U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 4
[a____^#(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U53^#(x₁)]	=	0
[U12(x₁)]	=	x₁ + 0
[a__U43(x₁)]	=	x₁ + 0
[isQid(x₁)]	=	0
[a__U62^#(x₁)]	=	0
[a____(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U42^#(x₁, x₂)]	=	x₂ + 4
[a__U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 4
[a__isList(x₁)]	=	x₁ + 2
[a__isNeList(x₁)]	=	x₁ + 2
[a__U12^#(x₁)]	=	0
[o]	=	0
[a__U21^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 4
[a__U61^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 2
[isList(x₁)]	=	x₁ + 2
[a__and^#(x₁, x₂)]	=	x₂ + 2
[a__U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 4
[a__U32(x₁)]	=	x₁ + 2
[nil]	=	2
[U62(x₁)]	=	x₁ + 0
[a__isQid^#(x₁)]	=	0
[a__U52^#(x₁, x₂)]	=	x₂ + 4
[mark(x₁)]	=	x₁ + 0
[a__U72(x₁)]	=	x₁ + 0
[a__isNePal(x₁)]	=	x₁ + 0
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 2
[a__isPalListKind(x₁)]	=	0
[U32(x₁)]	=	x₁ + 2
[a__U53(x₁)]	=	x₁ + 0
[a__U42(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U52(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U12(x₁)]	=	x₁ + 0
[i]	=	0
[U52(x₁, x₂)]	=	x₁ + x₂ + 2
[U61(x₁, x₂)]	=	x₁ + 0
[e]	=	0
[a__U22^#(x₁, x₂)]	=	x₂ + 4
[a__isPalListKind^#(x₁)]	=	2
[U31(x₁, x₂)]	=	x₁ + 2
[a__U71(x₁, x₂)]	=	x₁ + x₂ + 0
[a__isPal(x₁)]	=	x₁ + 0
[a__U61(x₁, x₂)]	=	x₁ + 0
[a__U41^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 5
[tt]	=	0
[a__isQid(x₁)]	=	0
[a__U23(x₁)]	=	x₁ + 0
[a__isList^#(x₁)]	=	x₁ + 4
[U22(x₁, x₂)]	=	x₁ + x₂ + 2
[U51(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 4
[a__and(x₁, x₂)]	=	x₁ + x₂ + 0
[isPalListKind(x₁)]	=	0
[U53(x₁)]	=	x₁ + 0
[U41(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 4
[a__U32^#(x₁)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 2

together with the usable rules

a__U62(tt)	→	tt	(18)
mark(isList(X))	→	a__isList(X)	(50)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(80)
a__U11(tt,V)	→	a__U12(a__isNeList(V))	(4)
a__U52(tt,V2)	→	a__U53(a__isList(V2))	(15)
a__U23(tt)	→	tt	(8)
mark(isQid(X))	→	a__isQid(X)	(54)
a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(X1,X2)	→	U11(X1,X2)	(77)
a____(nil,X)	→	mark(X)	(3)
a__U53(tt)	→	tt	(16)
a__and(tt,X)	→	mark(X)	(21)
a__isPalListKind(o)	→	tt	(36)
mark(isPal(X))	→	a__isPal(X)	(68)
a__U32(X)	→	U32(X)	(85)
a__isPal(X)	→	isPal(X)	(100)
a__isNeList(__(V1,V2))	→	a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(26)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(63)
a__U71(tt,V)	→	a__U72(a__isNePal(V))	(19)
a__isPalListKind(a)	→	tt	(32)
a__U61(tt,V)	→	a__U62(a__isQid(V))	(17)
mark(U53(X))	→	a__U53(mark(X))	(60)
a__isNeList(__(V1,V2))	→	a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(27)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(87)
a__U31(X1,X2)	→	U31(X1,X2)	(84)
a__isPalListKind(i)	→	tt	(34)
a__isList(V)	→	a__U11(a__isPalListKind(V),V)	(22)
a__isNePal(V)	→	a__U61(a__isPalListKind(V),V)	(28)
mark(isNePal(X))	→	a__isNePal(X)	(65)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(44)
a__U12(tt)	→	tt	(5)
mark(e)	→	e	(72)
a__isPalListKind(e)	→	tt	(33)
mark(U72(X))	→	a__U72(mark(X))	(64)
a__U61(X1,X2)	→	U61(X1,X2)	(93)
a__U53(X)	→	U53(X)	(92)
a__U32(tt)	→	tt	(10)
a__isQid(a)	→	tt	(39)
a__U22(tt,V2)	→	a__U23(a__isList(V2))	(7)
a__U42(X1,X2)	→	U42(X1,X2)	(88)
a__U72(tt)	→	tt	(20)
a__isNeList(V)	→	a__U31(a__isPalListKind(V),V)	(25)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(49)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(52)
a__isPal(V)	→	a__U71(a__isPalListKind(V),V)	(30)
mark(U62(X))	→	a__U62(mark(X))	(62)
a__U51(tt,V1,V2)	→	a__U52(a__isNeList(V1),V2)	(14)
a__isList(X)	→	isList(X)	(82)
a__U43(X)	→	U43(X)	(89)
mark(U42(X1,X2))	→	a__U42(mark(X1),X2)	(56)
a__isNeList(X)	→	isNeList(X)	(79)
a__isPal(nil)	→	tt	(31)
a__U42(tt,V2)	→	a__U43(a__isNeList(V2))	(12)
mark(nil)	→	nil	(69)
a__U72(X)	→	U72(X)	(96)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(45)
a__U12(X)	→	U12(X)	(78)
a__U22(X1,X2)	→	U22(X1,X2)	(81)
a__isList(nil)	→	tt	(23)
mark(tt)	→	tt	(70)
a__isList(__(V1,V2))	→	a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(24)
a__U62(X)	→	U62(X)	(94)
a____(X1,X2)	→	__(X1,X2)	(76)
mark(U43(X))	→	a__U43(mark(X))	(57)
a__and(X1,X2)	→	and(X1,X2)	(98)
a__U41(tt,V1,V2)	→	a__U42(a__isList(V1),V2)	(11)
a__U31(tt,V)	→	a__U32(a__isQid(V))	(9)
a__U43(tt)	→	tt	(13)
mark(U23(X))	→	a__U23(mark(X))	(51)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(90)
a__isQid(e)	→	tt	(40)
mark(isPalListKind(X))	→	a__isPalListKind(X)	(67)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(55)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(59)
a__U21(tt,V1,V2)	→	a__U22(a__isList(V1),V2)	(6)
a__isPalListKind(__(V1,V2))	→	a__and(a__isPalListKind(V1),isPalListKind(V2))	(38)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(61)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(58)
mark(o)	→	o	(74)
mark(u)	→	u	(75)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(48)
mark(a)	→	a	(71)
mark(U32(X))	→	a__U32(mark(X))	(53)
mark(isNeList(X))	→	a__isNeList(X)	(47)
mark(i)	→	i	(73)
a__U52(X1,X2)	→	U52(X1,X2)	(91)
a__isNePal(X)	→	isNePal(X)	(97)
a__isPalListKind(X)	→	isPalListKind(X)	(99)
a__isPalListKind(u)	→	tt	(37)
a__isQid(i)	→	tt	(41)
a__U71(X1,X2)	→	U71(X1,X2)	(95)
a__isQid(o)	→	tt	(42)
mark(U12(X))	→	a__U12(mark(X))	(46)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(66)
a__U23(X)	→	U23(X)	(83)
a__isPalListKind(nil)	→	tt	(35)
a__isNePal(__(I,__(P,I)))	→	a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(29)
a__isQid(u)	→	tt	(43)
a__isQid(X)	→	isQid(X)	(86)
a____(X,nil)	→	mark(X)	(2)

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

a__isNeList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(142)
mark^#(U41(X1,X2,X3))	→	mark^#(X1)	(154)
mark^#(__(X1,X2))	→	mark^#(X2)	(150)
mark^#(U51(X1,X2,X3))	→	a__U51^#(mark(X1),X2,X3)	(149)
mark^#(U51(X1,X2,X3))	→	mark^#(X1)	(190)
a__isNeList^#(__(V1,V2))	→	a__U41^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(145)
a__U41^#(tt,V1,V2)	→	a__U42^#(a__isList(V1),V2)	(144)
mark^#(U21(X1,X2,X3))	→	a__U21^#(mark(X1),X2,X3)	(143)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(142)
a__isNeList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(138)
mark^#(U52(X1,X2))	→	mark^#(X1)	(139)
a__isNeList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(138)
a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__isQid(I),isPalListKind(I))	(185)
mark^#(U41(X1,X2,X3))	→	a__U41^#(mark(X1),X2,X3)	(137)
a__isList^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(182)
a__isNeList^#(__(V1,V2))	→	a__U51^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(181)
mark^#(U32(X))	→	mark^#(X)	(133)
mark^#(U21(X1,X2,X3))	→	mark^#(X1)	(131)
mark^#(U31(X1,X2))	→	mark^#(X1)	(130)
a__U41^#(tt,V1,V2)	→	a__isList^#(V1)	(176)
a__isList^#(V)	→	a__isPalListKind^#(V)	(127)
a__isNeList^#(V)	→	a__isPalListKind^#(V)	(126)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(174)
mark^#(__(X1,X2))	→	mark^#(X1)	(122)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(172)
mark^#(U22(X1,X2))	→	mark^#(X1)	(116)
a__isList^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(112)
mark^#(U11(X1,X2))	→	mark^#(X1)	(158)
a__isList^#(__(V1,V2))	→	a__U21^#(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(105)
mark^#(U42(X1,X2))	→	mark^#(X1)	(103)
a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(101)

could be deleted.

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)))

(180)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	1
[a__isNePal^#(x₁)]	=	2
[U21(x₁, x₂, x₃)]	=	x₁ + 2
[a__U72^#(x₁)]	=	0
[a__U71^#(x₁, x₂)]	=	2
[U11(x₁, x₂)]	=	x₁ + 2
[a__U31^#(x₁, x₂)]	=	0
[a__isNeList^#(x₁)]	=	4
[isNeList(x₁)]	=	2
[a__U23^#(x₁)]	=	0
[isPal(x₁)]	=	x₁ + 1
[U42(x₁, x₂)]	=	2
[u]	=	21822
[U71(x₁, x₂)]	=	x₁ + 1
[a__U62(x₁)]	=	x₁ + 1
[and(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U43^#(x₁)]	=	0
[a__isPal^#(x₁)]	=	2
[U43(x₁)]	=	1
[a__U51^#(x₁, x₂, x₃)]	=	4
[U23(x₁)]	=	0
[a__U22(x₁, x₂)]	=	x₁ + 0
[isNePal(x₁)]	=	x₁ + 2
[U72(x₁)]	=	1
[a__U11^#(x₁, x₂)]	=	4
[a__U31(x₁, x₂)]	=	x₁ + 2
[a__U51(x₁, x₂, x₃)]	=	x₁ + 2
[a____^#(x₁, x₂)]	=	x₁ + 0
[a__U53^#(x₁)]	=	0
[U12(x₁)]	=	x₁ + 0
[a__U43(x₁)]	=	1
[isQid(x₁)]	=	1
[a__U62^#(x₁)]	=	0
[a____(x₁, x₂)]	=	x₁ + x₂ + 38593
[a__U42^#(x₁, x₂)]	=	4
[a__U41(x₁, x₂, x₃)]	=	x₁ + 2
[a__isList(x₁)]	=	2
[a__isNeList(x₁)]	=	2
[a__U12^#(x₁)]	=	0
[o]	=	0
[a__U21^#(x₁, x₂, x₃)]	=	4
[a__U61^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	2
[isList(x₁)]	=	2
[a__and^#(x₁, x₂)]	=	2
[a__U21(x₁, x₂, x₃)]	=	x₁ + 2
[a__U32(x₁)]	=	x₁ + 1
[nil]	=	11453
[U62(x₁)]	=	x₁ + 1
[a__isQid^#(x₁)]	=	0
[a__U52^#(x₁, x₂)]	=	4
[mark(x₁)]	=	x₁ + 0
[a__U72(x₁)]	=	1
[a__isNePal(x₁)]	=	x₁ + 2
[a__U11(x₁, x₂)]	=	x₁ + 2
[a__isPalListKind(x₁)]	=	0
[U32(x₁)]	=	x₁ + 1
[a__U53(x₁)]	=	x₁ + 0
[a__U42(x₁, x₂)]	=	2
[a__U52(x₁, x₂)]	=	2
[a__U12(x₁)]	=	x₁ + 0
[i]	=	43724
[U52(x₁, x₂)]	=	2
[U61(x₁, x₂)]	=	x₁ + x₂ + 2
[e]	=	0
[a__U22^#(x₁, x₂)]	=	4
[a__isPalListKind^#(x₁)]	=	2
[U31(x₁, x₂)]	=	x₁ + 2
[a__U71(x₁, x₂)]	=	x₁ + 1
[a__isPal(x₁)]	=	x₁ + 1
[a__U61(x₁, x₂)]	=	x₁ + x₂ + 2
[a__U41^#(x₁, x₂, x₃)]	=	5
[tt]	=	0
[a__isQid(x₁)]	=	1
[a__U23(x₁)]	=	0
[a__isList^#(x₁)]	=	4
[U22(x₁, x₂)]	=	x₁ + 0
[U51(x₁, x₂, x₃)]	=	x₁ + 2
[a__and(x₁, x₂)]	=	x₁ + x₂ + 0
[isPalListKind(x₁)]	=	0
[U53(x₁)]	=	x₁ + 0
[U41(x₁, x₂, x₃)]	=	x₁ + 2
[a__U32^#(x₁)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 38593

together with the usable rules

a__U62(tt)	→	tt	(18)
mark(isList(X))	→	a__isList(X)	(50)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(80)
a__U11(tt,V)	→	a__U12(a__isNeList(V))	(4)
a__U52(tt,V2)	→	a__U53(a__isList(V2))	(15)
a__U23(tt)	→	tt	(8)
mark(isQid(X))	→	a__isQid(X)	(54)
a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(X1,X2)	→	U11(X1,X2)	(77)
a____(nil,X)	→	mark(X)	(3)
a__U53(tt)	→	tt	(16)
a__and(tt,X)	→	mark(X)	(21)
a__isPalListKind(o)	→	tt	(36)
mark(isPal(X))	→	a__isPal(X)	(68)
a__U32(X)	→	U32(X)	(85)
a__isPal(X)	→	isPal(X)	(100)
a__isNeList(__(V1,V2))	→	a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(26)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(63)
a__U71(tt,V)	→	a__U72(a__isNePal(V))	(19)
a__isPalListKind(a)	→	tt	(32)
a__U61(tt,V)	→	a__U62(a__isQid(V))	(17)
mark(U53(X))	→	a__U53(mark(X))	(60)
a__isNeList(__(V1,V2))	→	a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(27)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(87)
a__U31(X1,X2)	→	U31(X1,X2)	(84)
a__isPalListKind(i)	→	tt	(34)
a__isList(V)	→	a__U11(a__isPalListKind(V),V)	(22)
a__isNePal(V)	→	a__U61(a__isPalListKind(V),V)	(28)
mark(isNePal(X))	→	a__isNePal(X)	(65)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(44)
a__U12(tt)	→	tt	(5)
mark(e)	→	e	(72)
a__isPalListKind(e)	→	tt	(33)
mark(U72(X))	→	a__U72(mark(X))	(64)
a__U61(X1,X2)	→	U61(X1,X2)	(93)
a__U53(X)	→	U53(X)	(92)
a__U32(tt)	→	tt	(10)
a__isQid(a)	→	tt	(39)
a__U22(tt,V2)	→	a__U23(a__isList(V2))	(7)
a__U42(X1,X2)	→	U42(X1,X2)	(88)
a__U72(tt)	→	tt	(20)
a__isNeList(V)	→	a__U31(a__isPalListKind(V),V)	(25)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(49)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(52)
a__isPal(V)	→	a__U71(a__isPalListKind(V),V)	(30)
mark(U62(X))	→	a__U62(mark(X))	(62)
a__U51(tt,V1,V2)	→	a__U52(a__isNeList(V1),V2)	(14)
a__isList(X)	→	isList(X)	(82)
a__U43(X)	→	U43(X)	(89)
mark(U42(X1,X2))	→	a__U42(mark(X1),X2)	(56)
a__isNeList(X)	→	isNeList(X)	(79)
a__isPal(nil)	→	tt	(31)
a__U42(tt,V2)	→	a__U43(a__isNeList(V2))	(12)
mark(nil)	→	nil	(69)
a__U72(X)	→	U72(X)	(96)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(45)
a__U12(X)	→	U12(X)	(78)
a__U22(X1,X2)	→	U22(X1,X2)	(81)
a__isList(nil)	→	tt	(23)
mark(tt)	→	tt	(70)
a__isList(__(V1,V2))	→	a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(24)
a__U62(X)	→	U62(X)	(94)
a____(X1,X2)	→	__(X1,X2)	(76)
mark(U43(X))	→	a__U43(mark(X))	(57)
a__and(X1,X2)	→	and(X1,X2)	(98)
a__U41(tt,V1,V2)	→	a__U42(a__isList(V1),V2)	(11)
a__U31(tt,V)	→	a__U32(a__isQid(V))	(9)
a__U43(tt)	→	tt	(13)
mark(U23(X))	→	a__U23(mark(X))	(51)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(90)
a__isQid(e)	→	tt	(40)
mark(isPalListKind(X))	→	a__isPalListKind(X)	(67)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(55)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(59)
a__U21(tt,V1,V2)	→	a__U22(a__isList(V1),V2)	(6)
a__isPalListKind(__(V1,V2))	→	a__and(a__isPalListKind(V1),isPalListKind(V2))	(38)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(61)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(58)
mark(o)	→	o	(74)
mark(u)	→	u	(75)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(48)
mark(a)	→	a	(71)
mark(U32(X))	→	a__U32(mark(X))	(53)
mark(isNeList(X))	→	a__isNeList(X)	(47)
mark(i)	→	i	(73)
a__U52(X1,X2)	→	U52(X1,X2)	(91)
a__isNePal(X)	→	isNePal(X)	(97)
a__isPalListKind(X)	→	isPalListKind(X)	(99)
a__isPalListKind(u)	→	tt	(37)
a__isQid(i)	→	tt	(41)
a__U71(X1,X2)	→	U71(X1,X2)	(95)
a__isQid(o)	→	tt	(42)
mark(U12(X))	→	a__U12(mark(X))	(46)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(66)
a__U23(X)	→	U23(X)	(83)
a__isPalListKind(nil)	→	tt	(35)
a__isNePal(__(I,__(P,I)))	→	a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(29)
a__isQid(u)	→	tt	(43)
a__isQid(X)	→	isQid(X)	(86)
a____(X,nil)	→	mark(X)	(2)

(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)))

(180)

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

a__and^#(tt,X)	→	mark^#(X)	(106)
mark^#(isPal(X))	→	a__isPal^#(X)	(148)
mark^#(U71(X1,X2))	→	mark^#(X1)	(140)
mark^#(U71(X1,X2))	→	a__U71^#(mark(X1),X2)	(186)
a__U71^#(tt,V)	→	a__isNePal^#(V)	(135)
mark^#(U53(X))	→	mark^#(X)	(164)
a__isNePal^#(V)	→	a__isPalListKind^#(V)	(167)
mark^#(isNePal(X))	→	a__isNePal^#(X)	(178)
mark^#(U72(X))	→	mark^#(X)	(125)
a__isPal^#(V)	→	a__isPalListKind^#(V)	(153)
a__isPal^#(V)	→	a__U71^#(a__isPalListKind(V),V)	(118)
mark^#(U62(X))	→	mark^#(X)	(115)
mark^#(U43(X))	→	mark^#(X)	(170)
mark^#(U23(X))	→	mark^#(X)	(168)
mark^#(isPalListKind(X))	→	a__isPalListKind^#(X)	(179)
a__isPalListKind^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(177)
a__isPalListKind^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(193)
mark^#(U61(X1,X2))	→	mark^#(X1)	(175)
mark^#(U12(X))	→	mark^#(X)	(189)
mark^#(and(X1,X2))	→	mark^#(X1)	(124)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(165)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	1
[a__isNePal^#(x₁)]	=	3
[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[a__U72^#(x₁)]	=	0
[a__U71^#(x₁, x₂)]	=	4
[U11(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U31^#(x₁, x₂)]	=	0
[a__isNeList^#(x₁)]	=	4
[isNeList(x₁)]	=	x₁ + 0
[a__U23^#(x₁)]	=	0
[isPal(x₁)]	=	4
[U42(x₁, x₂)]	=	x₂ + 1
[u]	=	10883
[U71(x₁, x₂)]	=	x₁ + 4
[a__U62(x₁)]	=	x₁ + 1
[and(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U43^#(x₁)]	=	0
[a__isPal^#(x₁)]	=	5
[U43(x₁)]	=	x₁ + 1
[a__U51^#(x₁, x₂, x₃)]	=	4
[U23(x₁)]	=	x₁ + 0
[a__U22(x₁, x₂)]	=	x₁ + x₂ + 0
[isNePal(x₁)]	=	4
[U72(x₁)]	=	x₁ + 0
[a__U11^#(x₁, x₂)]	=	4
[a__U31(x₁, x₂)]	=	x₁ + 0
[a__U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 1
[a____^#(x₁, x₂)]	=	x₁ + 0
[a__U53^#(x₁)]	=	0
[U12(x₁)]	=	x₁ + 0
[a__U43(x₁)]	=	x₁ + 1
[isQid(x₁)]	=	0
[a__U62^#(x₁)]	=	0
[a____(x₁, x₂)]	=	x₁ + x₂ + 1
[a__U42^#(x₁, x₂)]	=	4
[a__U41(x₁, x₂, x₃)]	=	x₃ + 1
[a__isList(x₁)]	=	x₁ + 0
[a__isNeList(x₁)]	=	x₁ + 0
[a__U12^#(x₁)]	=	0
[o]	=	22280
[a__U21^#(x₁, x₂, x₃)]	=	4
[a__U61^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 2
[isList(x₁)]	=	x₁ + 0
[a__and^#(x₁, x₂)]	=	x₂ + 2
[a__U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[a__U32(x₁)]	=	x₁ + 0
[nil]	=	11453
[U62(x₁)]	=	x₁ + 1
[a__isQid^#(x₁)]	=	0
[a__U52^#(x₁, x₂)]	=	4
[mark(x₁)]	=	x₁ + 0
[a__U72(x₁)]	=	x₁ + 0
[a__isNePal(x₁)]	=	4
[a__U11(x₁, x₂)]	=	x₁ + x₂ + 0
[a__isPalListKind(x₁)]	=	0
[U32(x₁)]	=	x₁ + 0
[a__U53(x₁)]	=	x₁ + 0
[a__U42(x₁, x₂)]	=	x₂ + 1
[a__U52(x₁, x₂)]	=	x₂ + 1
[a__U12(x₁)]	=	x₁ + 0
[i]	=	58340
[U52(x₁, x₂)]	=	x₂ + 1
[U61(x₁, x₂)]	=	x₁ + 4
[e]	=	41861
[a__U22^#(x₁, x₂)]	=	4
[a__isPalListKind^#(x₁)]	=	2
[U31(x₁, x₂)]	=	x₁ + 0
[a__U71(x₁, x₂)]	=	x₁ + 4
[a__isPal(x₁)]	=	4
[a__U61(x₁, x₂)]	=	x₁ + 4
[a__U41^#(x₁, x₂, x₃)]	=	5
[tt]	=	0
[a__isQid(x₁)]	=	0
[a__U23(x₁)]	=	x₁ + 0
[a__isList^#(x₁)]	=	4
[U22(x₁, x₂)]	=	x₁ + x₂ + 0
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 1
[a__and(x₁, x₂)]	=	x₁ + x₂ + 0
[isPalListKind(x₁)]	=	0
[U53(x₁)]	=	x₁ + 0
[U41(x₁, x₂, x₃)]	=	x₃ + 1
[a__U32^#(x₁)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

a__U62(tt)	→	tt	(18)
mark(isList(X))	→	a__isList(X)	(50)
a__U21(X1,X2,X3)	→	U21(X1,X2,X3)	(80)
a__U11(tt,V)	→	a__U12(a__isNeList(V))	(4)
a__U52(tt,V2)	→	a__U53(a__isList(V2))	(15)
a__U23(tt)	→	tt	(8)
mark(isQid(X))	→	a__isQid(X)	(54)
a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a__U11(X1,X2)	→	U11(X1,X2)	(77)
a____(nil,X)	→	mark(X)	(3)
a__U53(tt)	→	tt	(16)
a__and(tt,X)	→	mark(X)	(21)
a__isPalListKind(o)	→	tt	(36)
mark(isPal(X))	→	a__isPal(X)	(68)
a__U32(X)	→	U32(X)	(85)
a__isPal(X)	→	isPal(X)	(100)
a__isNeList(__(V1,V2))	→	a__U41(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(26)
mark(U71(X1,X2))	→	a__U71(mark(X1),X2)	(63)
a__U71(tt,V)	→	a__U72(a__isNePal(V))	(19)
a__isPalListKind(a)	→	tt	(32)
a__U61(tt,V)	→	a__U62(a__isQid(V))	(17)
mark(U53(X))	→	a__U53(mark(X))	(60)
a__isNeList(__(V1,V2))	→	a__U51(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(27)
a__U41(X1,X2,X3)	→	U41(X1,X2,X3)	(87)
a__U31(X1,X2)	→	U31(X1,X2)	(84)
a__isPalListKind(i)	→	tt	(34)
a__isList(V)	→	a__U11(a__isPalListKind(V),V)	(22)
a__isNePal(V)	→	a__U61(a__isPalListKind(V),V)	(28)
mark(isNePal(X))	→	a__isNePal(X)	(65)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(44)
a__U12(tt)	→	tt	(5)
mark(e)	→	e	(72)
a__isPalListKind(e)	→	tt	(33)
mark(U72(X))	→	a__U72(mark(X))	(64)
a__U61(X1,X2)	→	U61(X1,X2)	(93)
a__U53(X)	→	U53(X)	(92)
a__U32(tt)	→	tt	(10)
a__isQid(a)	→	tt	(39)
a__U22(tt,V2)	→	a__U23(a__isList(V2))	(7)
a__U42(X1,X2)	→	U42(X1,X2)	(88)
a__U72(tt)	→	tt	(20)
a__isNeList(V)	→	a__U31(a__isPalListKind(V),V)	(25)
mark(U22(X1,X2))	→	a__U22(mark(X1),X2)	(49)
mark(U31(X1,X2))	→	a__U31(mark(X1),X2)	(52)
a__isPal(V)	→	a__U71(a__isPalListKind(V),V)	(30)
mark(U62(X))	→	a__U62(mark(X))	(62)
a__U51(tt,V1,V2)	→	a__U52(a__isNeList(V1),V2)	(14)
a__isList(X)	→	isList(X)	(82)
a__U43(X)	→	U43(X)	(89)
mark(U42(X1,X2))	→	a__U42(mark(X1),X2)	(56)
a__isNeList(X)	→	isNeList(X)	(79)
a__isPal(nil)	→	tt	(31)
a__U42(tt,V2)	→	a__U43(a__isNeList(V2))	(12)
mark(nil)	→	nil	(69)
a__U72(X)	→	U72(X)	(96)
mark(U11(X1,X2))	→	a__U11(mark(X1),X2)	(45)
a__U12(X)	→	U12(X)	(78)
a__U22(X1,X2)	→	U22(X1,X2)	(81)
a__isList(nil)	→	tt	(23)
mark(tt)	→	tt	(70)
a__isList(__(V1,V2))	→	a__U21(a__and(a__isPalListKind(V1),isPalListKind(V2)),V1,V2)	(24)
a__U62(X)	→	U62(X)	(94)
a____(X1,X2)	→	__(X1,X2)	(76)
mark(U43(X))	→	a__U43(mark(X))	(57)
a__and(X1,X2)	→	and(X1,X2)	(98)
a__U41(tt,V1,V2)	→	a__U42(a__isList(V1),V2)	(11)
a__U31(tt,V)	→	a__U32(a__isQid(V))	(9)
a__U43(tt)	→	tt	(13)
mark(U23(X))	→	a__U23(mark(X))	(51)
a__U51(X1,X2,X3)	→	U51(X1,X2,X3)	(90)
a__isQid(e)	→	tt	(40)
mark(isPalListKind(X))	→	a__isPalListKind(X)	(67)
mark(U41(X1,X2,X3))	→	a__U41(mark(X1),X2,X3)	(55)
mark(U52(X1,X2))	→	a__U52(mark(X1),X2)	(59)
a__U21(tt,V1,V2)	→	a__U22(a__isList(V1),V2)	(6)
a__isPalListKind(__(V1,V2))	→	a__and(a__isPalListKind(V1),isPalListKind(V2))	(38)
mark(U61(X1,X2))	→	a__U61(mark(X1),X2)	(61)
mark(U51(X1,X2,X3))	→	a__U51(mark(X1),X2,X3)	(58)
mark(o)	→	o	(74)
mark(u)	→	u	(75)
mark(U21(X1,X2,X3))	→	a__U21(mark(X1),X2,X3)	(48)
mark(a)	→	a	(71)
mark(U32(X))	→	a__U32(mark(X))	(53)
mark(isNeList(X))	→	a__isNeList(X)	(47)
mark(i)	→	i	(73)
a__U52(X1,X2)	→	U52(X1,X2)	(91)
a__isNePal(X)	→	isNePal(X)	(97)
a__isPalListKind(X)	→	isPalListKind(X)	(99)
a__isPalListKind(u)	→	tt	(37)
a__isQid(i)	→	tt	(41)
a__U71(X1,X2)	→	U71(X1,X2)	(95)
a__isQid(o)	→	tt	(42)
mark(U12(X))	→	a__U12(mark(X))	(46)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(66)
a__U23(X)	→	U23(X)	(83)
a__isPalListKind(nil)	→	tt	(35)
a__isNePal(__(I,__(P,I)))	→	a__and(a__and(a__isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P)))	(29)
a__isQid(u)	→	tt	(43)
a__isQid(X)	→	isQid(X)	(86)
a____(X,nil)	→	mark(X)	(2)

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

mark^#(isPal(X))	→	a__isPal^#(X)	(148)
mark^#(U71(X1,X2))	→	mark^#(X1)	(140)
mark^#(U71(X1,X2))	→	a__U71^#(mark(X1),X2)	(186)
a__U71^#(tt,V)	→	a__isNePal^#(V)	(135)
a__isNePal^#(V)	→	a__isPalListKind^#(V)	(167)
mark^#(isNePal(X))	→	a__isNePal^#(X)	(178)
a__isPal^#(V)	→	a__isPalListKind^#(V)	(153)
a__isPal^#(V)	→	a__U71^#(a__isPalListKind(V),V)	(118)
mark^#(U62(X))	→	mark^#(X)	(115)
mark^#(U43(X))	→	mark^#(X)	(170)
mark^#(U61(X1,X2))	→	mark^#(X1)	(175)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__and^#(tt,X)	→	mark^#(X)	(106)
mark^#(U53(X))	→	mark^#(X)	(164)
mark^#(U72(X))	→	mark^#(X)	(125)
mark^#(U23(X))	→	mark^#(X)	(168)
mark^#(isPalListKind(X))	→	a__isPalListKind^#(X)	(179)
a__isPalListKind^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(177)
a__isPalListKind^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(193)
mark^#(U12(X))	→	mark^#(X)	(189)
mark^#(and(X1,X2))	→	mark^#(X1)	(124)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(165)

1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	2657
[a__isNePal^#(x₁)]	=	3
[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[a__U72^#(x₁)]	=	0
[a__U71^#(x₁, x₂)]	=	4
[U11(x₁, x₂)]	=	35886
[a__U31^#(x₁, x₂)]	=	0
[a__isNeList^#(x₁)]	=	4
[isNeList(x₁)]	=	x₁ + 74345
[a__U23^#(x₁)]	=	0
[isPal(x₁)]	=	33230
[U42(x₁, x₂)]	=	x₁ + x₂ + 74348
[u]	=	2656
[U71(x₁, x₂)]	=	24066
[a__U62(x₁)]	=	35891
[and(x₁, x₂)]	=	x₁ + x₂ + 35890
[a__U43^#(x₁)]	=	0
[a__isPal^#(x₁)]	=	5
[U43(x₁)]	=	1
[a__U51^#(x₁, x₂, x₃)]	=	4
[U23(x₁)]	=	x₁ + 1
[a__U22(x₁, x₂)]	=	x₁ + 1
[isNePal(x₁)]	=	35888
[U72(x₁)]	=	x₁ + 1
[a__U11^#(x₁, x₂)]	=	4
[a__U31(x₁, x₂)]	=	x₂ + 1
[a__U51(x₁, x₂, x₃)]	=	x₁ + x₂ + 38461
[a____^#(x₁, x₂)]	=	0
[a__U53^#(x₁)]	=	0
[U12(x₁)]	=	x₁ + 0
[a__U43(x₁)]	=	x₁ + 2
[isQid(x₁)]	=	x₁ + 33227
[a__U62^#(x₁)]	=	0
[a____(x₁, x₂)]	=	6
[a__U42^#(x₁, x₂)]	=	4
[a__U41(x₁, x₂, x₃)]	=	x₂ + 74350
[a__isList(x₁)]	=	x₁ + 35886
[a__isNeList(x₁)]	=	x₁ + 74345
[a__U12^#(x₁)]	=	0
[o]	=	2656
[a__U21^#(x₁, x₂, x₃)]	=	4
[a__U61^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 2
[isList(x₁)]	=	35886
[a__and^#(x₁, x₂)]	=	x₂ + 5
[a__U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 2
[a__U32(x₁)]	=	1
[nil]	=	2656
[U62(x₁)]	=	35892
[a__isQid^#(x₁)]	=	0
[a__U52^#(x₁, x₂)]	=	4
[mark(x₁)]	=	x₁ + 0
[a__U72(x₁)]	=	35884
[a__isNePal(x₁)]	=	35889
[a__U11(x₁, x₂)]	=	x₂ + 35886
[a__isPalListKind(x₁)]	=	x₁ + 33229
[U32(x₁)]	=	x₁ + 0
[a__U53(x₁)]	=	2
[a__U42(x₁, x₂)]	=	74347
[a__U52(x₁, x₂)]	=	x₁ + x₂ + 1
[a__U12(x₁)]	=	1
[i]	=	2656
[U52(x₁, x₂)]	=	2
[U61(x₁, x₂)]	=	x₂ + 35891
[e]	=	0
[a__U22^#(x₁, x₂)]	=	4
[a__isPalListKind^#(x₁)]	=	x₁ + 18407
[U31(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U71(x₁, x₂)]	=	x₁ + 0
[a__isPal(x₁)]	=	x₁ + 33229
[a__U61(x₁, x₂)]	=	35890
[a__U41^#(x₁, x₂, x₃)]	=	5
[tt]	=	35885
[a__isQid(x₁)]	=	x₁ + 33228
[a__U23(x₁)]	=	35885
[a__isList^#(x₁)]	=	4
[U22(x₁, x₂)]	=	x₁ + x₂ + 1
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 38460
[a__and(x₁, x₂)]	=	35889
[isPalListKind(x₁)]	=	x₁ + 18406
[U53(x₁)]	=	x₁ + 1
[U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 74351
[a__U32^#(x₁)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 5

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

a__and^#(tt,X)	→	mark^#(X)	(106)
mark^#(U53(X))	→	mark^#(X)	(164)
mark^#(U72(X))	→	mark^#(X)	(125)
mark^#(U23(X))	→	mark^#(X)	(168)
mark^#(isPalListKind(X))	→	a__isPalListKind^#(X)	(179)
a__isPalListKind^#(__(V1,V2))	→	a__isPalListKind^#(V1)	(177)
a__isPalListKind^#(__(V1,V2))	→	a__and^#(a__isPalListKind(V1),isPalListKind(V2))	(193)
mark^#(and(X1,X2))	→	mark^#(X1)	(124)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(165)

could be deleted.

1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(U12(X))

→

mark^#(X)

(189)

1.1.1.1.2.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	2657
[a__isNePal^#(x₁)]	=	3
[U21(x₁, x₂, x₃)]	=	x₁ + x₂ + 1
[a__U72^#(x₁)]	=	0
[a__U71^#(x₁, x₂)]	=	4
[U11(x₁, x₂)]	=	16964
[a__U31^#(x₁, x₂)]	=	0
[a__isNeList^#(x₁)]	=	4
[isNeList(x₁)]	=	x₁ + 43836
[a__U23^#(x₁)]	=	0
[isPal(x₁)]	=	4
[U42(x₁, x₂)]	=	x₁ + x₂ + 96461
[u]	=	2
[U71(x₁, x₂)]	=	24066
[a__U62(x₁)]	=	52630
[and(x₁, x₂)]	=	x₁ + x₂ + 52629
[a__U43^#(x₁)]	=	0
[a__isPal^#(x₁)]	=	5
[U43(x₁)]	=	52623
[a__U51^#(x₁, x₂, x₃)]	=	4
[U23(x₁)]	=	x₁ + 1
[a__U22(x₁, x₂)]	=	x₁ + 1
[isNePal(x₁)]	=	13704
[U72(x₁)]	=	x₁ + 2
[a__U11^#(x₁, x₂)]	=	4
[a__U31(x₁, x₂)]	=	x₂ + 1
[a__U51(x₁, x₂, x₃)]	=	x₁ + x₂ + 43832
[a____^#(x₁, x₂)]	=	0
[a__U53^#(x₁)]	=	0
[U12(x₁)]	=	x₁ + 1
[a__U43(x₁)]	=	x₁ + 52624
[isQid(x₁)]	=	x₁ + 1
[a__U62^#(x₁)]	=	0
[a____(x₁, x₂)]	=	52625
[a__U42^#(x₁, x₂)]	=	4
[a__U41(x₁, x₂, x₃)]	=	x₂ + 96460
[a__isList(x₁)]	=	x₁ + 16964
[a__isNeList(x₁)]	=	x₁ + 43836
[a__U12^#(x₁)]	=	0
[o]	=	2
[a__U21^#(x₁, x₂, x₃)]	=	4
[a__U61^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 2
[isList(x₁)]	=	16964
[a__and^#(x₁, x₂)]	=	5
[a__U21(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 16960
[a__U32(x₁)]	=	1
[nil]	=	2656
[U62(x₁)]	=	52631
[a__isQid^#(x₁)]	=	0
[a__U52^#(x₁, x₂)]	=	4
[mark(x₁)]	=	x₁ + 0
[a__U72(x₁)]	=	4
[a__isNePal(x₁)]	=	52628
[a__U11(x₁, x₂)]	=	x₂ + 16964
[a__isPalListKind(x₁)]	=	x₁ + 3
[U32(x₁)]	=	x₁ + 0
[a__U53(x₁)]	=	2
[a__U42(x₁, x₂)]	=	96460
[a__U52(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U12(x₁)]	=	2
[i]	=	2
[U52(x₁, x₂)]	=	21423
[U61(x₁, x₂)]	=	x₂ + 52630
[e]	=	0
[a__U22^#(x₁, x₂)]	=	4
[a__isPalListKind^#(x₁)]	=	18407
[U31(x₁, x₂)]	=	x₁ + x₂ + 0
[a__U71(x₁, x₂)]	=	x₁ + 0
[a__isPal(x₁)]	=	x₁ + 3
[a__U61(x₁, x₂)]	=	52629
[a__U41^#(x₁, x₂, x₃)]	=	5
[tt]	=	5
[a__isQid(x₁)]	=	x₁ + 2
[a__U23(x₁)]	=	5
[a__isList^#(x₁)]	=	4
[U22(x₁, x₂)]	=	x₁ + x₂ + 1
[U51(x₁, x₂, x₃)]	=	x₁ + x₃ + 15520
[a__and(x₁, x₂)]	=	52628
[isPalListKind(x₁)]	=	x₁ + 1
[U53(x₁)]	=	x₁ + 1
[U41(x₁, x₂, x₃)]	=	x₂ + x₃ + 96461
[a__U32^#(x₁)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 52624

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

mark^#(U12(X))

→

mark^#(X)

(189)

could be deleted.

1.1.1.1.2.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.