Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_DLMMU04_iGM)

The rewrite relation of the following TRS is considered.

active(pairNs)	→	mark(cons(0,incr(oddNs)))	(1)
active(oddNs)	→	mark(incr(pairNs))	(2)
active(incr(cons(X,XS)))	→	mark(cons(s(X),incr(XS)))	(3)
active(take(0,XS))	→	mark(nil)	(4)
active(take(s(N),cons(X,XS)))	→	mark(cons(X,take(N,XS)))	(5)
active(zip(nil,XS))	→	mark(nil)	(6)
active(zip(X,nil))	→	mark(nil)	(7)
active(zip(cons(X,XS),cons(Y,YS)))	→	mark(cons(pair(X,Y),zip(XS,YS)))	(8)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
active(repItems(nil))	→	mark(nil)	(10)
active(repItems(cons(X,XS)))	→	mark(cons(X,cons(X,repItems(XS))))	(11)
mark(pairNs)	→	active(pairNs)	(12)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(13)
mark(0)	→	active(0)	(14)
mark(incr(X))	→	active(incr(mark(X)))	(15)
mark(oddNs)	→	active(oddNs)	(16)
mark(s(X))	→	active(s(mark(X)))	(17)
mark(take(X1,X2))	→	active(take(mark(X1),mark(X2)))	(18)
mark(nil)	→	active(nil)	(19)
mark(zip(X1,X2))	→	active(zip(mark(X1),mark(X2)))	(20)
mark(pair(X1,X2))	→	active(pair(mark(X1),mark(X2)))	(21)
mark(tail(X))	→	active(tail(mark(X)))	(22)
mark(repItems(X))	→	active(repItems(mark(X)))	(23)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
incr(mark(X))	→	incr(X)	(28)
incr(active(X))	→	incr(X)	(29)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
take(mark(X1),X2)	→	take(X1,X2)	(32)
take(X1,mark(X2))	→	take(X1,X2)	(33)
take(active(X1),X2)	→	take(X1,X2)	(34)
take(X1,active(X2))	→	take(X1,X2)	(35)
zip(mark(X1),X2)	→	zip(X1,X2)	(36)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
pair(X1,active(X2))	→	pair(X1,X2)	(43)
tail(mark(X))	→	tail(X)	(44)
tail(active(X))	→	tail(X)	(45)
repItems(mark(X))	→	repItems(X)	(46)
repItems(active(X))	→	repItems(X)	(47)

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.

active^#(oddNs)	→	incr^#(pairNs)	(48)
tail^#(mark(X))	→	tail^#(X)	(49)
mark^#(0)	→	active^#(0)	(50)
mark^#(zip(X1,X2))	→	mark^#(X2)	(51)
active^#(pairNs)	→	mark^#(cons(0,incr(oddNs)))	(52)
mark^#(tail(X))	→	tail^#(mark(X))	(53)
active^#(take(s(N),cons(X,XS)))	→	take^#(N,XS)	(54)
active^#(take(s(N),cons(X,XS)))	→	cons^#(X,take(N,XS))	(55)
zip^#(X1,active(X2))	→	zip^#(X1,X2)	(56)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(57)
mark^#(tail(X))	→	mark^#(X)	(58)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(59)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	pair^#(X,Y)	(60)
take^#(active(X1),X2)	→	take^#(X1,X2)	(61)
mark^#(incr(X))	→	mark^#(X)	(62)
mark^#(incr(X))	→	incr^#(mark(X))	(63)
mark^#(pair(X1,X2))	→	pair^#(mark(X1),mark(X2))	(64)
mark^#(oddNs)	→	active^#(oddNs)	(65)
active^#(repItems(nil))	→	mark^#(nil)	(66)
repItems^#(mark(X))	→	repItems^#(X)	(67)
mark^#(pair(X1,X2))	→	mark^#(X1)	(68)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(69)
active^#(pairNs)	→	cons^#(0,incr(oddNs))	(70)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(71)
mark^#(s(X))	→	s^#(mark(X))	(72)
pair^#(mark(X1),X2)	→	pair^#(X1,X2)	(73)
zip^#(X1,mark(X2))	→	zip^#(X1,X2)	(74)
zip^#(active(X1),X2)	→	zip^#(X1,X2)	(75)
mark^#(pair(X1,X2))	→	active^#(pair(mark(X1),mark(X2)))	(76)
active^#(take(0,XS))	→	mark^#(nil)	(77)
mark^#(repItems(X))	→	repItems^#(mark(X))	(78)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	cons^#(pair(X,Y),zip(XS,YS))	(79)
mark^#(repItems(X))	→	active^#(repItems(mark(X)))	(80)
mark^#(take(X1,X2))	→	take^#(mark(X1),mark(X2))	(81)
mark^#(tail(X))	→	active^#(tail(mark(X)))	(82)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(pair(X,Y),zip(XS,YS)))	(83)
active^#(zip(nil,XS))	→	mark^#(nil)	(84)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(85)
mark^#(take(X1,X2))	→	mark^#(X1)	(86)
zip^#(mark(X1),X2)	→	zip^#(X1,X2)	(87)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(88)
active^#(incr(cons(X,XS)))	→	mark^#(cons(s(X),incr(XS)))	(89)
s^#(mark(X))	→	s^#(X)	(90)
mark^#(s(X))	→	mark^#(X)	(91)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(92)
mark^#(repItems(X))	→	mark^#(X)	(93)
active^#(repItems(cons(X,XS)))	→	cons^#(X,repItems(XS))	(94)
pair^#(active(X1),X2)	→	pair^#(X1,X2)	(95)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(96)
repItems^#(active(X))	→	repItems^#(X)	(97)
active^#(incr(cons(X,XS)))	→	s^#(X)	(98)
mark^#(zip(X1,X2))	→	zip^#(mark(X1),mark(X2))	(99)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	zip^#(XS,YS)	(100)
take^#(X1,active(X2))	→	take^#(X1,X2)	(101)
incr^#(mark(X))	→	incr^#(X)	(102)
active^#(incr(cons(X,XS)))	→	incr^#(XS)	(103)
s^#(active(X))	→	s^#(X)	(104)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(105)
mark^#(zip(X1,X2))	→	mark^#(X1)	(106)
mark^#(pairNs)	→	active^#(pairNs)	(107)
mark^#(pair(X1,X2))	→	mark^#(X2)	(108)
active^#(tail(cons(X,XS)))	→	mark^#(XS)	(109)
mark^#(zip(X1,X2))	→	active^#(zip(mark(X1),mark(X2)))	(110)
active^#(repItems(cons(X,XS)))	→	cons^#(X,cons(X,repItems(XS)))	(111)
active^#(incr(cons(X,XS)))	→	cons^#(s(X),incr(XS))	(112)
tail^#(active(X))	→	tail^#(X)	(113)
active^#(pairNs)	→	incr^#(oddNs)	(114)
active^#(zip(X,nil))	→	mark^#(nil)	(115)
active^#(repItems(cons(X,XS)))	→	repItems^#(XS)	(116)
mark^#(cons(X1,X2))	→	mark^#(X1)	(117)
pair^#(X1,active(X2))	→	pair^#(X1,X2)	(118)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(119)
active^#(oddNs)	→	mark^#(incr(pairNs))	(120)
mark^#(nil)	→	active^#(nil)	(121)
pair^#(X1,mark(X2))	→	pair^#(X1,X2)	(122)
mark^#(cons(X1,X2))	→	cons^#(mark(X1),X2)	(123)
incr^#(active(X))	→	incr^#(X)	(124)
mark^#(take(X1,X2))	→	mark^#(X2)	(125)
mark^#(s(X))	→	active^#(s(mark(X)))	(126)
active^#(repItems(cons(X,XS)))	→	mark^#(cons(X,cons(X,repItems(XS))))	(127)

1.1 Dependency Graph Processor

The dependency pairs are split into 9 components.

The 1^st component contains the pair

active^#(repItems(cons(X,XS)))	→	mark^#(cons(X,cons(X,repItems(XS))))	(127)
mark^#(take(X1,X2))	→	mark^#(X2)	(125)
mark^#(s(X))	→	active^#(s(mark(X)))	(126)
mark^#(repItems(X))	→	mark^#(X)	(93)
mark^#(s(X))	→	mark^#(X)	(91)
active^#(incr(cons(X,XS)))	→	mark^#(cons(s(X),incr(XS)))	(89)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(88)
mark^#(take(X1,X2))	→	mark^#(X1)	(86)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(pair(X,Y),zip(XS,YS)))	(83)
mark^#(tail(X))	→	active^#(tail(mark(X)))	(82)
active^#(oddNs)	→	mark^#(incr(pairNs))	(120)
mark^#(repItems(X))	→	active^#(repItems(mark(X)))	(80)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(119)
mark^#(cons(X1,X2))	→	mark^#(X1)	(117)
mark^#(pair(X1,X2))	→	active^#(pair(mark(X1),mark(X2)))	(76)
mark^#(zip(X1,X2))	→	active^#(zip(mark(X1),mark(X2)))	(110)
active^#(tail(cons(X,XS)))	→	mark^#(XS)	(109)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(71)
mark^#(pair(X1,X2))	→	mark^#(X2)	(108)
mark^#(pair(X1,X2))	→	mark^#(X1)	(68)
mark^#(pairNs)	→	active^#(pairNs)	(107)
mark^#(oddNs)	→	active^#(oddNs)	(65)
mark^#(zip(X1,X2))	→	mark^#(X1)	(106)
mark^#(incr(X))	→	mark^#(X)	(62)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(57)
mark^#(tail(X))	→	mark^#(X)	(58)
active^#(pairNs)	→	mark^#(cons(0,incr(oddNs)))	(52)
mark^#(zip(X1,X2))	→	mark^#(X2)	(51)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	2
[incr(x₁)]	=	2
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	2
[pair(x₁, x₂)]	=	1
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	2
[mark^#(x₁)]	=	2
[0]	=	2
[s^#(x₁)]	=	0
[nil]	=	4
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	2
[oddNs]	=	2
[repItems^#(x₁)]	=	0
[active(x₁)]	=	4
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	2

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

mark^#(s(X))	→	active^#(s(mark(X)))	(126)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(88)
mark^#(pair(X1,X2))	→	active^#(pair(mark(X1),mark(X2)))	(76)

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

mark^#(take(X1,X2))	→	mark^#(X2)	(125)
mark^#(take(X1,X2))	→	mark^#(X1)	(86)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(119)
mark^#(incr(X))	→	mark^#(X)	(62)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(57)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(pair(X,Y),zip(XS,YS)))	(83)
active^#(pairNs)	→	mark^#(cons(0,incr(oddNs)))	(52)
active^#(incr(cons(X,XS)))	→	mark^#(cons(s(X),incr(XS)))	(89)
mark^#(oddNs)	→	active^#(oddNs)	(65)
mark^#(pair(X1,X2))	→	mark^#(X2)	(108)
mark^#(pair(X1,X2))	→	mark^#(X1)	(68)
mark^#(s(X))	→	mark^#(X)	(91)
mark^#(tail(X))	→	mark^#(X)	(58)
mark^#(tail(X))	→	active^#(tail(mark(X)))	(82)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(71)
mark^#(zip(X1,X2))	→	mark^#(X2)	(51)
mark^#(zip(X1,X2))	→	mark^#(X1)	(106)
mark^#(zip(X1,X2))	→	active^#(zip(mark(X1),mark(X2)))	(110)
mark^#(pairNs)	→	active^#(pairNs)	(107)
mark^#(repItems(X))	→	mark^#(X)	(93)
mark^#(repItems(X))	→	active^#(repItems(mark(X)))	(80)
active^#(repItems(cons(X,XS)))	→	mark^#(cons(X,cons(X,repItems(XS))))	(127)
active^#(tail(cons(X,XS)))	→	mark^#(XS)	(109)
mark^#(cons(X1,X2))	→	mark^#(X1)	(117)
active^#(oddNs)	→	mark^#(incr(pairNs))	(120)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 8949
[incr(x₁)]	=	x₁ + 0
[cons^#(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	max(0)
[take(x₁, x₂)]	=	max(x₁ + 9232, x₂ + 250, 0)
[pair(x₁, x₂)]	=	max(x₁ + 284, x₂ + 282, 0)
[zip^#(x₁, x₂)]	=	max(0)
[tail(x₁)]	=	x₁ + 20538
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[s^#(x₁)]	=	0
[nil]	=	9232
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[incr^#(x₁)]	=	0
[pairNs]	=	24870
[oddNs]	=	24870
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 8948, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	max(0)
[zip(x₁, x₂)]	=	max(x₁ + 284, x₂ + 9231, 0)

together with the usable rules

mark(take(X1,X2))	→	active(take(mark(X1),mark(X2)))	(18)
active(take(0,XS))	→	mark(nil)	(4)
mark(incr(X))	→	active(incr(mark(X)))	(15)
active(zip(cons(X,XS),cons(Y,YS)))	→	mark(cons(pair(X,Y),zip(XS,YS)))	(8)
active(pairNs)	→	mark(cons(0,incr(oddNs)))	(1)
active(incr(cons(X,XS)))	→	mark(cons(s(X),incr(XS)))	(3)
mark(oddNs)	→	active(oddNs)	(16)
mark(pair(X1,X2))	→	active(pair(mark(X1),mark(X2)))	(21)
zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
mark(nil)	→	active(nil)	(19)
take(mark(X1),X2)	→	take(X1,X2)	(32)
mark(s(X))	→	active(s(mark(X)))	(17)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
mark(tail(X))	→	active(tail(mark(X)))	(22)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
active(take(s(N),cons(X,XS)))	→	mark(cons(X,take(N,XS)))	(5)
take(X1,mark(X2))	→	take(X1,X2)	(33)
active(repItems(nil))	→	mark(nil)	(10)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
active(zip(X,nil))	→	mark(nil)	(7)
mark(zip(X1,X2))	→	active(zip(mark(X1),mark(X2)))	(20)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
mark(0)	→	active(0)	(14)
s(active(X))	→	s(X)	(31)
mark(pairNs)	→	active(pairNs)	(12)
tail(active(X))	→	tail(X)	(45)
mark(repItems(X))	→	active(repItems(mark(X)))	(23)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
active(repItems(cons(X,XS)))	→	mark(cons(X,cons(X,repItems(XS))))	(11)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(13)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
active(zip(nil,XS))	→	mark(nil)	(6)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

mark^#(take(X1,X2))	→	mark^#(X2)	(125)
mark^#(take(X1,X2))	→	mark^#(X1)	(86)
mark^#(pair(X1,X2))	→	mark^#(X2)	(108)
mark^#(pair(X1,X2))	→	mark^#(X1)	(68)
mark^#(tail(X))	→	mark^#(X)	(58)
mark^#(zip(X1,X2))	→	mark^#(X2)	(51)
mark^#(zip(X1,X2))	→	mark^#(X1)	(106)
mark^#(repItems(X))	→	mark^#(X)	(93)
active^#(tail(cons(X,XS)))	→	mark^#(XS)	(109)
mark^#(cons(X1,X2))	→	mark^#(X1)	(117)

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

mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(119)
mark^#(incr(X))	→	mark^#(X)	(62)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(57)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(pair(X,Y),zip(XS,YS)))	(83)
active^#(incr(cons(X,XS)))	→	mark^#(cons(s(X),incr(XS)))	(89)
mark^#(oddNs)	→	active^#(oddNs)	(65)
mark^#(s(X))	→	mark^#(X)	(91)
mark^#(tail(X))	→	active^#(tail(mark(X)))	(82)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(71)
mark^#(zip(X1,X2))	→	active^#(zip(mark(X1),mark(X2)))	(110)
mark^#(repItems(X))	→	active^#(repItems(mark(X)))	(80)
active^#(repItems(cons(X,XS)))	→	mark^#(cons(X,cons(X,repItems(XS))))	(127)
active^#(oddNs)	→	mark^#(incr(pairNs))	(120)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	11651
[incr(x₁)]	=	11651
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	11651
[pair(x₁, x₂)]	=	1
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	11650
[mark^#(x₁)]	=	11653
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	1
[incr^#(x₁)]	=	0
[pairNs]	=	2
[oddNs]	=	11651
[repItems^#(x₁)]	=	0
[active(x₁)]	=	2
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	x₁ + 2
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	11651

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

mark^#(tail(X))

→

active^#(tail(mark(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

mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(119)
mark^#(incr(X))	→	mark^#(X)	(62)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(57)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(pair(X,Y),zip(XS,YS)))	(83)
active^#(incr(cons(X,XS)))	→	mark^#(cons(s(X),incr(XS)))	(89)
mark^#(oddNs)	→	active^#(oddNs)	(65)
mark^#(s(X))	→	mark^#(X)	(91)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(71)
mark^#(zip(X1,X2))	→	active^#(zip(mark(X1),mark(X2)))	(110)
mark^#(repItems(X))	→	active^#(repItems(mark(X)))	(80)
active^#(repItems(cons(X,XS)))	→	mark^#(cons(X,cons(X,repItems(XS))))	(127)
active^#(oddNs)	→	mark^#(incr(pairNs))	(120)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	3
[incr(x₁)]	=	x₁ + 2
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + 3
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	1
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	23557
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 5
[incr^#(x₁)]	=	0
[pairNs]	=	0
[oddNs]	=	6
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	2
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	x₁ + x₂ + 3

together with the usable rules

cons(active(X1),X2)	→	cons(X1,X2)	(26)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
incr(mark(X))	→	incr(X)	(28)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(119)
mark^#(incr(X))	→	mark^#(X)	(62)
active^#(zip(cons(X,XS),cons(Y,YS)))	→	mark^#(cons(pair(X,Y),zip(XS,YS)))	(83)
active^#(incr(cons(X,XS)))	→	mark^#(cons(s(X),incr(XS)))	(89)
mark^#(oddNs)	→	active^#(oddNs)	(65)
mark^#(s(X))	→	mark^#(X)	(91)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(71)
mark^#(zip(X1,X2))	→	active^#(zip(mark(X1),mark(X2)))	(110)
mark^#(repItems(X))	→	active^#(repItems(mark(X)))	(80)
active^#(repItems(cons(X,XS)))	→	mark^#(cons(X,cons(X,repItems(XS))))	(127)

could be deleted.

1.1.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

mark^#(incr(X))	→	active^#(incr(mark(X)))	(57)
active^#(oddNs)	→	mark^#(incr(pairNs))	(120)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	1
[incr(x₁)]	=	3580
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	147
[pair(x₁, x₂)]	=	1
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	3578
[mark^#(x₁)]	=	3581
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	23557
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	649
[oddNs]	=	3582
[repItems^#(x₁)]	=	0
[active(x₁)]	=	3580
[cons(x₁, x₂)]	=	3580
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	486

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

mark^#(incr(X))	→	active^#(incr(mark(X)))	(57)
active^#(oddNs)	→	mark^#(incr(pairNs))	(120)

could be deleted.

1.1.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

repItems^#(mark(X))	→	repItems^#(X)	(67)
repItems^#(active(X))	→	repItems^#(X)	(97)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	16892
[incr(x₁)]	=	26875
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	27824
[s^#(x₁)]	=	0
[nil]	=	16894
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	1184
[oddNs]	=	26873
[repItems^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	26877
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

repItems^#(mark(X))	→	repItems^#(X)	(67)
repItems^#(active(X))	→	repItems^#(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

s^#(mark(X))	→	s^#(X)	(90)
s^#(active(X))	→	s^#(X)	(104)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	23975
[incr(x₁)]	=	56727
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	27824
[s^#(x₁)]	=	x₁ + 0
[nil]	=	32549
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	56726
[oddNs]	=	56725
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	56729
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

s^#(mark(X))	→	s^#(X)	(90)
s^#(active(X))	→	s^#(X)	(104)

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

incr^#(active(X))	→	incr^#(X)	(124)
incr^#(mark(X))	→	incr^#(X)	(102)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	1549
[incr(x₁)]	=	1913
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	28733
[s^#(x₁)]	=	0
[nil]	=	32549
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	x₁ + 0
[pairNs]	=	1888
[oddNs]	=	1911
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	1915
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

incr^#(active(X))	→	incr^#(X)	(124)
incr^#(mark(X))	→	incr^#(X)	(102)

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

pair^#(X1,mark(X2))	→	pair^#(X1,X2)	(122)
pair^#(X1,active(X2))	→	pair^#(X1,X2)	(118)
pair^#(mark(X1),X2)	→	pair^#(X1,X2)	(73)
pair^#(active(X1),X2)	→	pair^#(X1,X2)	(95)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	1
[incr(x₁)]	=	11844
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	16496
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	2
[oddNs]	=	11842
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	11846
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	x₁ + 0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

pair^#(mark(X1),X2)	→	pair^#(X1,X2)	(73)
pair^#(active(X1),X2)	→	pair^#(X1,X2)	(95)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

pair^#(X1,mark(X2))	→	pair^#(X1,X2)	(122)
pair^#(X1,active(X2))	→	pair^#(X1,X2)	(118)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	15538
[incr(x₁)]	=	18816
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	40386
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	1
[oddNs]	=	18814
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	18818
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	x₂ + 0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

pair^#(X1,mark(X2))	→	pair^#(X1,X2)	(122)
pair^#(X1,active(X2))	→	pair^#(X1,X2)	(118)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

zip^#(mark(X1),X2)	→	zip^#(X1,X2)	(87)
zip^#(active(X1),X2)	→	zip^#(X1,X2)	(75)
zip^#(X1,mark(X2))	→	zip^#(X1,X2)	(74)
zip^#(X1,active(X2))	→	zip^#(X1,X2)	(56)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	1
[incr(x₁)]	=	30089
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	x₂ + 0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	21726
[s^#(x₁)]	=	0
[nil]	=	20363
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	1
[oddNs]	=	30087
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	30091
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

zip^#(X1,mark(X2))	→	zip^#(X1,X2)	(74)
zip^#(X1,active(X2))	→	zip^#(X1,X2)	(56)

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

zip^#(mark(X1),X2)	→	zip^#(X1,X2)	(87)
zip^#(active(X1),X2)	→	zip^#(X1,X2)	(75)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	2
[incr(x₁)]	=	3
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	x₁ + 0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	21280
[s^#(x₁)]	=	0
[nil]	=	20364
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	1
[oddNs]	=	1
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	5
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

zip^#(mark(X1),X2)	→	zip^#(X1,X2)	(87)
zip^#(active(X1),X2)	→	zip^#(X1,X2)	(75)

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

take^#(active(X1),X2)	→	take^#(X1,X2)	(61)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(59)
take^#(X1,active(X2))	→	take^#(X1,X2)	(101)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(96)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	1
[incr(x₁)]	=	11178
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	x₁ + x₂ + 0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	20364
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	40484
[oddNs]	=	1
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	40486
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

take^#(active(X1),X2)	→	take^#(X1,X2)	(61)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(59)
take^#(X1,active(X2))	→	take^#(X1,X2)	(101)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(96)

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

tail^#(active(X))	→	tail^#(X)	(113)
tail^#(mark(X))	→	tail^#(X)	(49)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	1
[incr(x₁)]	=	32538
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	55042
[s^#(x₁)]	=	0
[nil]	=	11030
[tail^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	20948
[oddNs]	=	32536
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	32540
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

tail^#(active(X))	→	tail^#(X)	(113)
tail^#(mark(X))	→	tail^#(X)	(49)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(92)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(85)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(69)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(105)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	1
[incr(x₁)]	=	4594
[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	13459
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	4592
[oddNs]	=	4592
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	4596
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(92)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(85)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

cons^#(active(X1),X2)	→	cons^#(X1,X2)	(69)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(105)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	1
[incr(x₁)]	=	39814
[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	0
[pair(x₁, x₂)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	0
[mark^#(x₁)]	=	3581
[0]	=	36526
[s^#(x₁)]	=	0
[nil]	=	3
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	39812
[oddNs]	=	39812
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	39816
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	0

together with the usable rules

zip(mark(X1),X2)	→	zip(X1,X2)	(36)
cons(active(X1),X2)	→	cons(X1,X2)	(26)
take(mark(X1),X2)	→	take(X1,X2)	(32)
cons(X1,active(X2))	→	cons(X1,X2)	(27)
take(active(X1),X2)	→	take(X1,X2)	(34)
incr(mark(X))	→	incr(X)	(28)
tail(mark(X))	→	tail(X)	(44)
take(X1,mark(X2))	→	take(X1,X2)	(33)
zip(X1,active(X2))	→	zip(X1,X2)	(39)
cons(X1,mark(X2))	→	cons(X1,X2)	(25)
s(mark(X))	→	s(X)	(30)
s(active(X))	→	s(X)	(31)
tail(active(X))	→	tail(X)	(45)
cons(mark(X1),X2)	→	cons(X1,X2)	(24)
pair(mark(X1),X2)	→	pair(X1,X2)	(40)
zip(active(X1),X2)	→	zip(X1,X2)	(38)
repItems(active(X))	→	repItems(X)	(47)
zip(X1,mark(X2))	→	zip(X1,X2)	(37)
pair(X1,mark(X2))	→	pair(X1,X2)	(41)
pair(active(X1),X2)	→	pair(X1,X2)	(42)
repItems(mark(X))	→	repItems(X)	(46)
take(X1,active(X2))	→	take(X1,X2)	(35)
incr(active(X))	→	incr(X)	(29)
pair(X1,active(X2))	→	pair(X1,X2)	(43)

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

cons^#(active(X1),X2)	→	cons^#(X1,X2)	(69)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(105)

could be deleted.

1.1.9.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.