Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_DLMMU04_C)

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)
active(cons(X1,X2))	→	cons(active(X1),X2)	(12)
active(incr(X))	→	incr(active(X))	(13)
active(s(X))	→	s(active(X))	(14)
active(take(X1,X2))	→	take(active(X1),X2)	(15)
active(take(X1,X2))	→	take(X1,active(X2))	(16)
active(zip(X1,X2))	→	zip(active(X1),X2)	(17)
active(zip(X1,X2))	→	zip(X1,active(X2))	(18)
active(pair(X1,X2))	→	pair(active(X1),X2)	(19)
active(pair(X1,X2))	→	pair(X1,active(X2))	(20)
active(tail(X))	→	tail(active(X))	(21)
active(repItems(X))	→	repItems(active(X))	(22)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
s(mark(X))	→	mark(s(X))	(25)
take(mark(X1),X2)	→	mark(take(X1,X2))	(26)
take(X1,mark(X2))	→	mark(take(X1,X2))	(27)
zip(mark(X1),X2)	→	mark(zip(X1,X2))	(28)
zip(X1,mark(X2))	→	mark(zip(X1,X2))	(29)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
tail(mark(X))	→	mark(tail(X))	(32)
repItems(mark(X))	→	mark(repItems(X))	(33)
proper(pairNs)	→	ok(pairNs)	(34)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(35)
proper(0)	→	ok(0)	(36)
proper(incr(X))	→	incr(proper(X))	(37)
proper(oddNs)	→	ok(oddNs)	(38)
proper(s(X))	→	s(proper(X))	(39)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(40)
proper(nil)	→	ok(nil)	(41)
proper(zip(X1,X2))	→	zip(proper(X1),proper(X2))	(42)
proper(pair(X1,X2))	→	pair(proper(X1),proper(X2))	(43)
proper(tail(X))	→	tail(proper(X))	(44)
proper(repItems(X))	→	repItems(proper(X))	(45)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
incr(ok(X))	→	ok(incr(X))	(47)
s(ok(X))	→	ok(s(X))	(48)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(49)
zip(ok(X1),ok(X2))	→	ok(zip(X1,X2))	(50)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
tail(ok(X))	→	ok(tail(X))	(52)
repItems(ok(X))	→	ok(repItems(X))	(53)
top(mark(X))	→	top(proper(X))	(54)
top(ok(X))	→	top(active(X))	(55)

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.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 11 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(134)
top^#(mark(X))	→	top^#(proper(X))	(87)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

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

prec(repItems)	=	5	status(repItems)	=	[1]	list-extension(repItems)	=	Lex
prec(incr)	=	2	status(incr)	=	[1]	list-extension(incr)	=	Lex
prec(s)	=	4	status(s)	=	[1]	list-extension(s)	=	Lex
prec(take^#)	=	0	status(take^#)	=	[2, 1]	list-extension(take^#)	=	Lex
prec(take)	=	2	status(take)	=	[2, 1]	list-extension(take)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(pair)	=	2	status(pair)	=	[1, 2]	list-extension(pair)	=	Lex
prec(tail)	=	1	status(tail)	=	[1]	list-extension(tail)	=	Lex
prec(0)	=	3	status(0)	=	[]	list-extension(0)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(nil)	=	5	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(tail^#)	=	0	status(tail^#)	=	[]	list-extension(tail^#)	=	Lex
prec(mark)	=	0	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(incr^#)	=	0	status(incr^#)	=	[]	list-extension(incr^#)	=	Lex
prec(pairNs)	=	6	status(pairNs)	=	[]	list-extension(pairNs)	=	Lex
prec(oddNs)	=	7	status(oddNs)	=	[]	list-extension(oddNs)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(repItems^#)	=	0	status(repItems^#)	=	[]	list-extension(repItems^#)	=	Lex
prec(cons)	=	2	status(cons)	=	[1]	list-extension(cons)	=	Lex
prec(active^#)	=	0	status(active^#)	=	[]	list-extension(active^#)	=	Lex
prec(pair^#)	=	0	status(pair^#)	=	[]	list-extension(pair^#)	=	Lex
prec(zip)	=	5	status(zip)	=	[1, 2]	list-extension(zip)	=	Lex

and the following Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 1
[incr(x₁)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	x₁ + x₂ + 1
[take(x₁, x₂)]	=	x₁ + x₂ + 2
[top(x₁)]	=	1
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[tail(x₁)]	=	x₁ + 1
[0]	=	31122
[s^#(x₁)]	=	1
[nil]	=	31123
[tail^#(x₁)]	=	1
[mark(x₁)]	=	x₁ + 0
[incr^#(x₁)]	=	1
[pairNs]	=	31126
[oddNs]	=	31126
[proper^#(x₁)]	=	1
[repItems^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 3, x₂ + 0, 0)
[active^#(x₁)]	=	1
[pair^#(x₁, x₂)]	=	x₂ + 1
[zip(x₁, x₂)]	=	x₁ + x₂ + 2

together with the usable rules

active(zip(X1,X2))	→	zip(X1,active(X2))	(18)
zip(ok(X1),ok(X2))	→	ok(zip(X1,X2))	(50)
active(take(0,XS))	→	mark(nil)	(4)
active(take(X1,X2))	→	take(active(X1),X2)	(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)
active(take(X1,X2))	→	take(X1,active(X2))	(16)
active(tail(X))	→	tail(active(X))	(21)
proper(0)	→	ok(0)	(36)
take(mark(X1),X2)	→	mark(take(X1,X2))	(26)
active(pair(X1,X2))	→	pair(active(X1),X2)	(19)
tail(mark(X))	→	mark(tail(X))	(32)
active(zip(X1,X2))	→	zip(active(X1),X2)	(17)
take(X1,mark(X2))	→	mark(take(X1,X2))	(27)
proper(pairNs)	→	ok(pairNs)	(34)
active(repItems(X))	→	repItems(active(X))	(22)
zip(mark(X1),X2)	→	mark(zip(X1,X2))	(28)
proper(tail(X))	→	tail(proper(X))	(44)
active(take(s(N),cons(X,XS)))	→	mark(cons(X,take(N,XS)))	(5)
repItems(mark(X))	→	mark(repItems(X))	(33)
active(repItems(nil))	→	mark(nil)	(10)
proper(s(X))	→	s(proper(X))	(39)
active(zip(X,nil))	→	mark(nil)	(7)
active(pair(X1,X2))	→	pair(X1,active(X2))	(20)
s(mark(X))	→	mark(s(X))	(25)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(49)
tail(ok(X))	→	ok(tail(X))	(52)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
active(s(X))	→	s(active(X))	(14)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
active(cons(X1,X2))	→	cons(active(X1),X2)	(12)
proper(repItems(X))	→	repItems(proper(X))	(45)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(repItems(cons(X,XS)))	→	mark(cons(X,cons(X,repItems(XS))))	(11)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
active(incr(X))	→	incr(active(X))	(13)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(40)
active(zip(nil,XS))	→	mark(nil)	(6)
proper(oddNs)	→	ok(oddNs)	(38)
s(ok(X))	→	ok(s(X))	(48)
repItems(ok(X))	→	ok(repItems(X))	(53)
incr(ok(X))	→	ok(incr(X))	(47)
proper(incr(X))	→	incr(proper(X))	(37)
proper(nil)	→	ok(nil)	(41)
proper(zip(X1,X2))	→	zip(proper(X1),proper(X2))	(42)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(35)
zip(X1,mark(X2))	→	mark(zip(X1,X2))	(29)
proper(pair(X1,X2))	→	pair(proper(X1),proper(X2))	(43)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(87)

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

(134)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 1
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 436
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 1
[top(x₁)]	=	0
[pair(x₁, x₂)]	=	x₂ + 1
[top^#(x₁)]	=	x₁ + 0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	x₁ + 2
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	12644
[tail^#(x₁)]	=	0
[mark(x₁)]	=	0
[incr^#(x₁)]	=	0
[pairNs]	=	38803
[oddNs]	=	59342
[proper^#(x₁)]	=	0
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 0
[active^#(x₁)]	=	0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	x₂ + 1

together with the usable rules

active(zip(X1,X2))	→	zip(X1,active(X2))	(18)
zip(ok(X1),ok(X2))	→	ok(zip(X1,X2))	(50)
active(take(0,XS))	→	mark(nil)	(4)
active(take(X1,X2))	→	take(active(X1),X2)	(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)
active(take(X1,X2))	→	take(X1,active(X2))	(16)
active(tail(X))	→	tail(active(X))	(21)
proper(0)	→	ok(0)	(36)
take(mark(X1),X2)	→	mark(take(X1,X2))	(26)
active(pair(X1,X2))	→	pair(active(X1),X2)	(19)
tail(mark(X))	→	mark(tail(X))	(32)
active(zip(X1,X2))	→	zip(active(X1),X2)	(17)
take(X1,mark(X2))	→	mark(take(X1,X2))	(27)
proper(pairNs)	→	ok(pairNs)	(34)
active(repItems(X))	→	repItems(active(X))	(22)
zip(mark(X1),X2)	→	mark(zip(X1,X2))	(28)
proper(tail(X))	→	tail(proper(X))	(44)
active(take(s(N),cons(X,XS)))	→	mark(cons(X,take(N,XS)))	(5)
repItems(mark(X))	→	mark(repItems(X))	(33)
active(repItems(nil))	→	mark(nil)	(10)
proper(s(X))	→	s(proper(X))	(39)
active(zip(X,nil))	→	mark(nil)	(7)
active(pair(X1,X2))	→	pair(X1,active(X2))	(20)
s(mark(X))	→	mark(s(X))	(25)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(49)
tail(ok(X))	→	ok(tail(X))	(52)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
active(s(X))	→	s(active(X))	(14)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
active(cons(X1,X2))	→	cons(active(X1),X2)	(12)
proper(repItems(X))	→	repItems(proper(X))	(45)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(repItems(cons(X,XS)))	→	mark(cons(X,cons(X,repItems(XS))))	(11)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
active(incr(X))	→	incr(active(X))	(13)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(40)
active(zip(nil,XS))	→	mark(nil)	(6)
proper(oddNs)	→	ok(oddNs)	(38)
s(ok(X))	→	ok(s(X))	(48)
repItems(ok(X))	→	ok(repItems(X))	(53)
incr(ok(X))	→	ok(incr(X))	(47)
proper(incr(X))	→	incr(proper(X))	(37)
proper(nil)	→	ok(nil)	(41)
proper(zip(X1,X2))	→	zip(proper(X1),proper(X2))	(42)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(35)
zip(X1,mark(X2))	→	mark(zip(X1,X2))	(29)
proper(pair(X1,X2))	→	pair(proper(X1),proper(X2))	(43)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

top^#(ok(X))

→

top^#(active(X))

(134)

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

proper^#(tail(X))	→	proper^#(X)	(133)
proper^#(pair(X1,X2))	→	proper^#(X2)	(132)
proper^#(incr(X))	→	proper^#(X)	(96)
proper^#(zip(X1,X2))	→	proper^#(X2)	(92)
proper^#(cons(X1,X2))	→	proper^#(X2)	(130)
proper^#(s(X))	→	proper^#(X)	(90)
proper^#(pair(X1,X2))	→	proper^#(X1)	(126)
proper^#(take(X1,X2))	→	proper^#(X1)	(124)
proper^#(zip(X1,X2))	→	proper^#(X1)	(83)
proper^#(repItems(X))	→	proper^#(X)	(118)
proper^#(take(X1,X2))	→	proper^#(X2)	(113)
proper^#(cons(X1,X2))	→	proper^#(X1)	(103)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 1
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[top^#(x₁)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	x₁ + 57785
[ok(x₁)]	=	x₁ + 57786
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[incr^#(x₁)]	=	0
[pairNs]	=	36828
[oddNs]	=	36827
[proper^#(x₁)]	=	x₁ + 0
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

proper^#(tail(X))	→	proper^#(X)	(133)
proper^#(pair(X1,X2))	→	proper^#(X2)	(132)
proper^#(incr(X))	→	proper^#(X)	(96)
proper^#(zip(X1,X2))	→	proper^#(X2)	(92)
proper^#(cons(X1,X2))	→	proper^#(X2)	(130)
proper^#(s(X))	→	proper^#(X)	(90)
proper^#(pair(X1,X2))	→	proper^#(X1)	(126)
proper^#(take(X1,X2))	→	proper^#(X1)	(124)
proper^#(zip(X1,X2))	→	proper^#(X1)	(83)
proper^#(repItems(X))	→	proper^#(X)	(118)
proper^#(take(X1,X2))	→	proper^#(X2)	(113)
proper^#(cons(X1,X2))	→	proper^#(X1)	(103)

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

active^#(incr(X))	→	active^#(X)	(101)
active^#(tail(X))	→	active^#(X)	(97)
active^#(zip(X1,X2))	→	active^#(X2)	(94)
active^#(zip(X1,X2))	→	active^#(X1)	(95)
active^#(take(X1,X2))	→	active^#(X1)	(85)
active^#(pair(X1,X2))	→	active^#(X1)	(76)
active^#(cons(X1,X2))	→	active^#(X1)	(114)
active^#(repItems(X))	→	active^#(X)	(67)
active^#(s(X))	→	active^#(X)	(64)
active^#(take(X1,X2))	→	active^#(X2)	(106)
active^#(pair(X1,X2))	→	active^#(X2)	(57)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 1
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[top^#(x₁)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 32132
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[incr^#(x₁)]	=	0
[pairNs]	=	32002
[oddNs]	=	51373
[proper^#(x₁)]	=	0
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 19374
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	x₁ + 0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

active^#(incr(X))	→	active^#(X)	(101)
active^#(tail(X))	→	active^#(X)	(97)
active^#(zip(X1,X2))	→	active^#(X2)	(94)
active^#(zip(X1,X2))	→	active^#(X1)	(95)
active^#(take(X1,X2))	→	active^#(X1)	(85)
active^#(pair(X1,X2))	→	active^#(X1)	(76)
active^#(cons(X1,X2))	→	active^#(X1)	(114)
active^#(repItems(X))	→	active^#(X)	(67)
active^#(s(X))	→	active^#(X)	(64)
active^#(take(X1,X2))	→	active^#(X2)	(106)
active^#(pair(X1,X2))	→	active^#(X2)	(57)

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

repItems^#(ok(X))	→	repItems^#(X)	(125)
repItems^#(mark(X))	→	repItems^#(X)	(61)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

repItems^#(ok(X))

→

repItems^#(X)

(125)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

repItems^#(mark(X))

→

repItems^#(X)

(61)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

repItems^#(mark(X))

→

repItems^#(X)

(61)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

tail^#(mark(X))	→	tail^#(X)	(84)
tail^#(ok(X))	→	tail^#(X)	(104)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

tail^#(mark(X))	→	tail^#(X)	(84)
tail^#(ok(X))	→	tail^#(X)	(104)

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

s^#(ok(X))	→	s^#(X)	(117)
s^#(mark(X))	→	s^#(X)	(63)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 2089
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 25118
[top(x₁)]	=	0
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[top^#(x₁)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 57205
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	x₁ + 0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	43648
[oddNs]	=	43647
[proper^#(x₁)]	=	0
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

s^#(ok(X))	→	s^#(X)	(117)
s^#(mark(X))	→	s^#(X)	(63)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

incr^#(ok(X))	→	incr^#(X)	(131)
incr^#(mark(X))	→	incr^#(X)	(58)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

incr^#(ok(X))	→	incr^#(X)	(131)
incr^#(mark(X))	→	incr^#(X)	(58)

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(98)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(82)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(98)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(82)

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

zip^#(ok(X1),ok(X2))	→	zip^#(X1,X2)	(127)
zip^#(mark(X1),X2)	→	zip^#(X1,X2)	(80)
zip^#(X1,mark(X2))	→	zip^#(X1,X2)	(109)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 1
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 2
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 10109
[top(x₁)]	=	0
[pair(x₁, x₂)]	=	x₁ + x₂ + 1
[top^#(x₁)]	=	0
[zip^#(x₁, x₂)]	=	x₂ + 0
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[pairNs]	=	35973
[oddNs]	=	35972
[proper^#(x₁)]	=	0
[repItems^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
pair(mark(X1),X2)	→	mark(pair(X1,X2))	(30)
pair(X1,mark(X2))	→	mark(pair(X1,X2))	(31)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(tail(cons(X,XS)))	→	mark(XS)	(9)
pair(ok(X1),ok(X2))	→	ok(pair(X1,X2))	(51)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

zip^#(ok(X1),ok(X2))	→	zip^#(X1,X2)	(127)
zip^#(X1,mark(X2))	→	zip^#(X1,X2)	(109)

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

zip^#(mark(X1),X2)

→

zip^#(X1,X2)

(80)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

zip^#(mark(X1),X2)

→

zip^#(X1,X2)

(80)

could be deleted.

1.1.9.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

pair^#(ok(X1),ok(X2))	→	pair^#(X1,X2)	(88)
pair^#(mark(X1),X2)	→	pair^#(X1,X2)	(74)
pair^#(X1,mark(X2))	→	pair^#(X1,X2)	(59)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(take(0,XS))	→	mark(nil)	(4)
active(repItems(nil))	→	mark(nil)	(10)
active(zip(X,nil))	→	mark(nil)	(7)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(23)
incr(mark(X))	→	mark(incr(X))	(24)
active(zip(nil,XS))	→	mark(nil)	(6)
incr(ok(X))	→	ok(incr(X))	(47)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(46)
active(oddNs)	→	mark(incr(pairNs))	(2)

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

pair^#(ok(X1),ok(X2))	→	pair^#(X1,X2)	(88)
pair^#(mark(X1),X2)	→	pair^#(X1,X2)	(74)

could be deleted.

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

(59)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	x₁ + 1
[incr(x₁)]	=	x₁ + 12782
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	2
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	2
[top(x₁)]	=	0
[pair(x₁, x₂)]	=	24632
[top^#(x₁)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	x₁ + 18331
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 15149
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	23332
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 2766
[incr^#(x₁)]	=	0
[pairNs]	=	32662
[oddNs]	=	1
[proper^#(x₁)]	=	0
[repItems^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	24292
[active^#(x₁)]	=	0
[pair^#(x₁, x₂)]	=	x₂ + 0
[zip(x₁, x₂)]	=	x₁ + 20541

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

pair^#(X1,mark(X2))

→

pair^#(X1,X2)

(59)

could be deleted.

1.1.10.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 11^th component contains the pair

take^#(X1,mark(X2))	→	take^#(X1,X2)	(129)
take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(79)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(116)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[repItems(x₁)]	=	12893
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	31371
[take^#(x₁, x₂)]	=	x₁ + x₂ + 0
[take(x₁, x₂)]	=	31609
[top(x₁)]	=	0
[pair(x₁, x₂)]	=	19072
[top^#(x₁)]	=	0
[zip^#(x₁, x₂)]	=	0
[tail(x₁)]	=	18331
[proper(x₁)]	=	12892
[ok(x₁)]	=	x₁ + 16209
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	23332
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 2766
[incr^#(x₁)]	=	0
[pairNs]	=	32662
[oddNs]	=	2284
[proper^#(x₁)]	=	0
[repItems^#(x₁)]	=	0
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	x₁ + 46918
[active^#(x₁)]	=	0
[pair^#(x₁, x₂)]	=	0
[zip(x₁, x₂)]	=	21654

together with the usable rules

incr(mark(X))	→	mark(incr(X))	(24)
incr(ok(X))	→	ok(incr(X))	(47)

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

take^#(X1,mark(X2))	→	take^#(X1,X2)	(129)
take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(79)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(116)

could be deleted.

1.1.11.1 Dependency Graph Processor

The dependency pairs are split into 0 components.