Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex7_BLR02_C)

The rewrite relation of the following TRS is considered.

active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(head(cons(X,XS)))	→	mark(X)	(2)
active(2nd(cons(X,XS)))	→	mark(head(XS))	(3)
active(take(0,XS))	→	mark(nil)	(4)
active(take(s(N),cons(X,XS)))	→	mark(cons(X,take(N,XS)))	(5)
active(sel(0,cons(X,XS)))	→	mark(X)	(6)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(7)
active(from(X))	→	from(active(X))	(8)
active(cons(X1,X2))	→	cons(active(X1),X2)	(9)
active(s(X))	→	s(active(X))	(10)
active(head(X))	→	head(active(X))	(11)
active(2nd(X))	→	2nd(active(X))	(12)
active(take(X1,X2))	→	take(active(X1),X2)	(13)
active(take(X1,X2))	→	take(X1,active(X2))	(14)
active(sel(X1,X2))	→	sel(active(X1),X2)	(15)
active(sel(X1,X2))	→	sel(X1,active(X2))	(16)
from(mark(X))	→	mark(from(X))	(17)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(18)
s(mark(X))	→	mark(s(X))	(19)
head(mark(X))	→	mark(head(X))	(20)
2nd(mark(X))	→	mark(2nd(X))	(21)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(24)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(25)
proper(from(X))	→	from(proper(X))	(26)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(27)
proper(s(X))	→	s(proper(X))	(28)
proper(head(X))	→	head(proper(X))	(29)
proper(2nd(X))	→	2nd(proper(X))	(30)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(31)
proper(0)	→	ok(0)	(32)
proper(nil)	→	ok(nil)	(33)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(34)
from(ok(X))	→	ok(from(X))	(35)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
s(ok(X))	→	ok(s(X))	(37)
head(ok(X))	→	ok(head(X))	(38)
2nd(ok(X))	→	ok(2nd(X))	(39)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(41)
top(mark(X))	→	top(proper(X))	(42)
top(ok(X))	→	top(active(X))	(43)

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.

top^#(ok(X))	→	active^#(X)	(44)
proper^#(cons(X1,X2))	→	cons^#(proper(X1),proper(X2))	(45)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(46)
active^#(take(s(N),cons(X,XS)))	→	cons^#(X,take(N,XS))	(47)
from^#(mark(X))	→	from^#(X)	(48)
proper^#(sel(X1,X2))	→	proper^#(X2)	(49)
proper^#(sel(X1,X2))	→	proper^#(X1)	(50)
proper^#(s(X))	→	s^#(proper(X))	(51)
s^#(mark(X))	→	s^#(X)	(52)
active^#(sel(X1,X2))	→	active^#(X2)	(53)
proper^#(from(X))	→	from^#(proper(X))	(54)
active^#(from(X))	→	from^#(active(X))	(55)
active^#(sel(X1,X2))	→	active^#(X1)	(56)
proper^#(s(X))	→	proper^#(X)	(57)
top^#(mark(X))	→	top^#(proper(X))	(58)
active^#(from(X))	→	active^#(X)	(59)
active^#(from(X))	→	cons^#(X,from(s(X)))	(60)
proper^#(sel(X1,X2))	→	sel^#(proper(X1),proper(X2))	(61)
2nd^#(mark(X))	→	2nd^#(X)	(62)
active^#(take(X1,X2))	→	active^#(X1)	(63)
s^#(ok(X))	→	s^#(X)	(64)
take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(65)
active^#(from(X))	→	s^#(X)	(66)
proper^#(take(X1,X2))	→	proper^#(X2)	(67)
proper^#(take(X1,X2))	→	proper^#(X1)	(68)
proper^#(cons(X1,X2))	→	proper^#(X2)	(69)
active^#(take(X1,X2))	→	take^#(active(X1),X2)	(70)
active^#(sel(s(N),cons(X,XS)))	→	sel^#(N,XS)	(71)
active^#(from(X))	→	from^#(s(X))	(72)
active^#(cons(X1,X2))	→	cons^#(active(X1),X2)	(73)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(74)
head^#(mark(X))	→	head^#(X)	(75)
active^#(sel(X1,X2))	→	sel^#(X1,active(X2))	(76)
proper^#(from(X))	→	proper^#(X)	(77)
active^#(take(X1,X2))	→	take^#(X1,active(X2))	(78)
active^#(2nd(X))	→	2nd^#(active(X))	(79)
top^#(mark(X))	→	proper^#(X)	(80)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(81)
head^#(ok(X))	→	head^#(X)	(82)
active^#(s(X))	→	s^#(active(X))	(83)
from^#(ok(X))	→	from^#(X)	(84)
proper^#(cons(X1,X2))	→	proper^#(X1)	(85)
proper^#(2nd(X))	→	proper^#(X)	(86)
proper^#(take(X1,X2))	→	take^#(proper(X1),proper(X2))	(87)
active^#(s(X))	→	active^#(X)	(88)
proper^#(2nd(X))	→	2nd^#(proper(X))	(89)
active^#(sel(X1,X2))	→	sel^#(active(X1),X2)	(90)
active^#(head(X))	→	active^#(X)	(91)
2nd^#(ok(X))	→	2nd^#(X)	(92)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(93)
active^#(take(X1,X2))	→	active^#(X2)	(94)
active^#(take(s(N),cons(X,XS)))	→	take^#(N,XS)	(95)
active^#(2nd(X))	→	active^#(X)	(96)
active^#(head(X))	→	head^#(active(X))	(97)
proper^#(head(X))	→	head^#(proper(X))	(98)
top^#(ok(X))	→	top^#(active(X))	(99)
active^#(2nd(cons(X,XS)))	→	head^#(XS)	(100)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(101)
active^#(cons(X1,X2))	→	active^#(X1)	(102)
proper^#(head(X))	→	proper^#(X)	(103)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(104)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(105)

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(99)
top^#(mark(X))	→	top^#(proper(X))	(58)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(top^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(s^#)	=	1
π(active)	=	1

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

prec(cons^#)	=	0	status(cons^#)	=	[2, 1]	list-extension(cons^#)	=	Lex
prec(s)	=	6	status(s)	=	[1]	list-extension(s)	=	Lex
prec(take^#)	=	0	status(take^#)	=	[1]	list-extension(take^#)	=	Lex
prec(take)	=	7	status(take)	=	[2, 1]	list-extension(take)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(2nd)	=	3	status(2nd)	=	[1]	list-extension(2nd)	=	Lex
prec(head^#)	=	0	status(head^#)	=	[]	list-extension(head^#)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(from)	=	3	status(from)	=	[1]	list-extension(from)	=	Lex
prec(sel)	=	4	status(sel)	=	[1, 2]	list-extension(sel)	=	Lex
prec(nil)	=	8	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(2nd^#)	=	0	status(2nd^#)	=	[]	list-extension(2nd^#)	=	Lex
prec(mark)	=	1	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(head)	=	6	status(head)	=	[1]	list-extension(head)	=	Lex
prec(cons)	=	2	status(cons)	=	[1]	list-extension(cons)	=	Lex
prec(active^#)	=	0	status(active^#)	=	[]	list-extension(active^#)	=	Lex

and the following Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	x₁ + 1
[take(x₁, x₂)]	=	x₁ + x₂ + 17069
[top(x₁)]	=	1
[2nd(x₁)]	=	x₁ + 2
[head^#(x₁)]	=	1
[0]	=	7630
[sel^#(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 48180
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[nil]	=	7632
[2nd^#(x₁)]	=	1
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	1
[from^#(x₁)]	=	1
[head(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	max(x₁ + 17068, x₂ + 0, 0)
[active^#(x₁)]	=	1

together with the usable rules

cons(mark(X1),X2)	→	mark(cons(X1,X2))	(18)
active(take(0,XS))	→	mark(nil)	(4)
active(sel(X1,X2))	→	sel(active(X1),X2)	(15)
active(from(X))	→	from(active(X))	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(2nd(cons(X,XS)))	→	mark(head(XS))	(3)
active(sel(X1,X2))	→	sel(X1,active(X2))	(16)
2nd(mark(X))	→	mark(2nd(X))	(21)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
proper(from(X))	→	from(proper(X))	(26)
s(mark(X))	→	mark(s(X))	(19)
proper(0)	→	ok(0)	(32)
from(mark(X))	→	mark(from(X))	(17)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(27)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(34)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
proper(s(X))	→	s(proper(X))	(28)
active(take(s(N),cons(X,XS)))	→	mark(cons(X,take(N,XS)))	(5)
proper(nil)	→	ok(nil)	(33)
active(s(X))	→	s(active(X))	(10)
2nd(ok(X))	→	ok(2nd(X))	(39)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(7)
head(mark(X))	→	mark(head(X))	(20)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(25)
proper(2nd(X))	→	2nd(proper(X))	(30)
active(take(X1,X2))	→	take(X1,active(X2))	(14)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(31)
active(2nd(X))	→	2nd(active(X))	(12)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(24)
active(head(X))	→	head(active(X))	(11)
active(cons(X1,X2))	→	cons(active(X1),X2)	(9)
active(take(X1,X2))	→	take(active(X1),X2)	(13)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
active(sel(0,cons(X,XS)))	→	mark(X)	(6)
head(ok(X))	→	ok(head(X))	(38)
s(ok(X))	→	ok(s(X))	(37)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(41)
from(ok(X))	→	ok(from(X))	(35)
proper(head(X))	→	head(proper(X))	(29)
active(head(cons(X,XS)))	→	mark(X)	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(58)

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

(99)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 0
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[proper(x₁)]	=	12703
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₂ + 0
[s^#(x₁)]	=	0
[nil]	=	12701
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + 0
[active^#(x₁)]	=	0

together with the usable rules

cons(mark(X1),X2)	→	mark(cons(X1,X2))	(18)
active(take(0,XS))	→	mark(nil)	(4)
active(sel(X1,X2))	→	sel(active(X1),X2)	(15)
active(from(X))	→	from(active(X))	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(2nd(cons(X,XS)))	→	mark(head(XS))	(3)
active(sel(X1,X2))	→	sel(X1,active(X2))	(16)
2nd(mark(X))	→	mark(2nd(X))	(21)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(36)
proper(from(X))	→	from(proper(X))	(26)
s(mark(X))	→	mark(s(X))	(19)
proper(0)	→	ok(0)	(32)
from(mark(X))	→	mark(from(X))	(17)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(27)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(34)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
proper(s(X))	→	s(proper(X))	(28)
active(take(s(N),cons(X,XS)))	→	mark(cons(X,take(N,XS)))	(5)
proper(nil)	→	ok(nil)	(33)
active(s(X))	→	s(active(X))	(10)
2nd(ok(X))	→	ok(2nd(X))	(39)
active(sel(s(N),cons(X,XS)))	→	mark(sel(N,XS))	(7)
head(mark(X))	→	mark(head(X))	(20)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(25)
proper(2nd(X))	→	2nd(proper(X))	(30)
active(take(X1,X2))	→	take(X1,active(X2))	(14)
proper(take(X1,X2))	→	take(proper(X1),proper(X2))	(31)
active(2nd(X))	→	2nd(active(X))	(12)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(24)
active(head(X))	→	head(active(X))	(11)
active(cons(X1,X2))	→	cons(active(X1),X2)	(9)
active(take(X1,X2))	→	take(active(X1),X2)	(13)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
active(sel(0,cons(X,XS)))	→	mark(X)	(6)
head(ok(X))	→	ok(head(X))	(38)
s(ok(X))	→	ok(s(X))	(37)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(41)
from(ok(X))	→	ok(from(X))	(35)
proper(head(X))	→	head(proper(X))	(29)
active(head(cons(X,XS)))	→	mark(X)	(2)

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

top^#(ok(X))

→

top^#(active(X))

(99)

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^#(from(X))	→	proper^#(X)	(77)
proper^#(head(X))	→	proper^#(X)	(103)
proper^#(cons(X1,X2))	→	proper^#(X2)	(69)
proper^#(take(X1,X2))	→	proper^#(X1)	(68)
proper^#(take(X1,X2))	→	proper^#(X2)	(67)
proper^#(s(X))	→	proper^#(X)	(57)
proper^#(2nd(X))	→	proper^#(X)	(86)
proper^#(cons(X1,X2))	→	proper^#(X1)	(85)
proper^#(sel(X1,X2))	→	proper^#(X1)	(50)
proper^#(sel(X1,X2))	→	proper^#(X2)	(49)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 1
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	14462
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 1
[sel(x₁, x₂)]	=	x₁ + x₂ + 2
[s^#(x₁)]	=	0
[nil]	=	14460
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	x₁ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 29274
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

proper^#(from(X))	→	proper^#(X)	(77)
proper^#(head(X))	→	proper^#(X)	(103)
proper^#(cons(X1,X2))	→	proper^#(X2)	(69)
proper^#(take(X1,X2))	→	proper^#(X1)	(68)
proper^#(take(X1,X2))	→	proper^#(X2)	(67)
proper^#(s(X))	→	proper^#(X)	(57)
proper^#(2nd(X))	→	proper^#(X)	(86)
proper^#(cons(X1,X2))	→	proper^#(X1)	(85)
proper^#(sel(X1,X2))	→	proper^#(X1)	(50)
proper^#(sel(X1,X2))	→	proper^#(X2)	(49)

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^#(cons(X1,X2))	→	active^#(X1)	(102)
active^#(2nd(X))	→	active^#(X)	(96)
active^#(take(X1,X2))	→	active^#(X2)	(94)
active^#(take(X1,X2))	→	active^#(X1)	(63)
active^#(head(X))	→	active^#(X)	(91)
active^#(from(X))	→	active^#(X)	(59)
active^#(sel(X1,X2))	→	active^#(X1)	(56)
active^#(s(X))	→	active^#(X)	(88)
active^#(sel(X1,X2))	→	active^#(X2)	(53)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 32135
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 1
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	4
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 1
[sel(x₁, x₂)]	=	x₁ + x₂ + 2
[s^#(x₁)]	=	0
[nil]	=	2
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 29274
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

active^#(cons(X1,X2))	→	active^#(X1)	(102)
active^#(2nd(X))	→	active^#(X)	(96)
active^#(take(X1,X2))	→	active^#(X2)	(94)
active^#(take(X1,X2))	→	active^#(X1)	(63)
active^#(head(X))	→	active^#(X)	(91)
active^#(from(X))	→	active^#(X)	(59)
active^#(sel(X1,X2))	→	active^#(X1)	(56)
active^#(s(X))	→	active^#(X)	(88)
active^#(sel(X1,X2))	→	active^#(X2)	(53)

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

take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(65)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(93)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(81)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	x₁ + x₂ + 0
[take(x₁, x₂)]	=	x₁ + x₂ + 8822
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	30250
[ok(x₁)]	=	x₁ + 1
[0]	=	51072
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1911
[s^#(x₁)]	=	0
[nil]	=	41702
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	30250
[cons(x₁, x₂)]	=	x₂ + 32158
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

take^#(ok(X1),ok(X2))	→	take^#(X1,X2)	(65)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(93)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(81)

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

head^#(mark(X))	→	head^#(X)	(75)
head^#(ok(X))	→	head^#(X)	(82)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	51072
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 21256
[s^#(x₁)]	=	0
[nil]	=	3449
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[cons(x₁, x₂)]	=	x₂ + 32158
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

head^#(mark(X))	→	head^#(X)	(75)
head^#(ok(X))	→	head^#(X)	(82)

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

cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(104)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(74)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	2
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[nil]	=	2
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[cons(x₁, x₂)]	=	x₂ + 32158
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

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

→

cons^#(X1,X2)

(104)

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

cons^#(mark(X1),X2)

→

cons^#(X1,X2)

(74)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 24847
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 17015
[s^#(x₁)]	=	0
[nil]	=	2
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[cons(x₁, x₂)]	=	x₂ + 2
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

cons^#(mark(X1),X2)

→

cons^#(X1,X2)

(74)

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

s^#(ok(X))	→	s^#(X)	(64)
s^#(mark(X))	→	s^#(X)	(52)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 5851
[s^#(x₁)]	=	x₁ + 0
[nil]	=	2
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	2
[cons(x₁, x₂)]	=	x₂ + 2
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

s^#(ok(X))	→	s^#(X)	(64)
s^#(mark(X))	→	s^#(X)	(52)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

from^#(ok(X))	→	from^#(X)	(84)
from^#(mark(X))	→	from^#(X)	(48)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	2
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[s^#(x₁)]	=	0
[nil]	=	20259
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	1
[head(x₁)]	=	2
[cons(x₁, x₂)]	=	x₂ + 2
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

from^#(ok(X))	→	from^#(X)	(84)
from^#(mark(X))	→	from^#(X)	(48)

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

sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(105)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(101)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(46)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	15740
[ok(x₁)]	=	x₁ + 1
[0]	=	15740
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₂ + 2
[s^#(x₁)]	=	0
[nil]	=	15740
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	9124
[cons(x₁, x₂)]	=	x₂ + 2
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
take(mark(X1),X2)	→	mark(take(X1,X2))	(22)
take(X1,mark(X2))	→	mark(take(X1,X2))	(23)
take(ok(X1),ok(X2))	→	ok(take(X1,X2))	(40)
s(ok(X))	→	ok(s(X))	(37)

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

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

→

sel^#(X1,X2)

(101)

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

sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(46)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(105)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	11314
[sel^#(x₁, x₂)]	=	x₂ + 0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₂ + 15796
[s^#(x₁)]	=	0
[nil]	=	26720
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
s(ok(X))	→	ok(s(X))	(37)

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

sel^#(X1,mark(X2))

→

sel^#(X1,X2)

(46)

could be deleted.

1.1.9.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

sel^#(mark(X1),X2)

→

sel^#(X1,X2)

(105)

1.1.9.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	14735
[sel^#(x₁, x₂)]	=	x₁ + 0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₂ + 11968
[s^#(x₁)]	=	0
[nil]	=	31921
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 58268
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
s(ok(X))	→	ok(s(X))	(37)

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

sel^#(mark(X1),X2)

→

sel^#(X1,X2)

(105)

could be deleted.

1.1.9.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

2nd^#(mark(X))	→	2nd^#(X)	(62)
2nd^#(ok(X))	→	2nd^#(X)	(92)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 2
[top(x₁)]	=	0
[2nd(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 20695
[0]	=	11890
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₂ + 24417
[s^#(x₁)]	=	0
[nil]	=	64750
[2nd^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(19)
from(mark(X))	→	mark(from(X))	(17)
s(ok(X))	→	ok(s(X))	(37)
from(ok(X))	→	ok(from(X))	(35)

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

2nd^#(mark(X))	→	2nd^#(X)	(62)
2nd^#(ok(X))	→	2nd^#(X)	(92)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 0 components.