Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex7_BLR02_iGM)

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)
mark(from(X))	→	active(from(mark(X)))	(8)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(9)
mark(s(X))	→	active(s(mark(X)))	(10)
mark(head(X))	→	active(head(mark(X)))	(11)
mark(2nd(X))	→	active(2nd(mark(X)))	(12)
mark(take(X1,X2))	→	active(take(mark(X1),mark(X2)))	(13)
mark(0)	→	active(0)	(14)
mark(nil)	→	active(nil)	(15)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(16)
from(mark(X))	→	from(X)	(17)
from(active(X))	→	from(X)	(18)
cons(mark(X1),X2)	→	cons(X1,X2)	(19)
cons(X1,mark(X2))	→	cons(X1,X2)	(20)
cons(active(X1),X2)	→	cons(X1,X2)	(21)
cons(X1,active(X2))	→	cons(X1,X2)	(22)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
head(mark(X))	→	head(X)	(25)
head(active(X))	→	head(X)	(26)
2nd(mark(X))	→	2nd(X)	(27)
2nd(active(X))	→	2nd(X)	(28)
take(mark(X1),X2)	→	take(X1,X2)	(29)
take(X1,mark(X2))	→	take(X1,X2)	(30)
take(active(X1),X2)	→	take(X1,X2)	(31)
take(X1,active(X2))	→	take(X1,X2)	(32)
sel(mark(X1),X2)	→	sel(X1,X2)	(33)
sel(X1,mark(X2))	→	sel(X1,X2)	(34)
sel(active(X1),X2)	→	sel(X1,X2)	(35)
sel(X1,active(X2))	→	sel(X1,X2)	(36)

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.

take^#(mark(X1),X2)	→	take^#(X1,X2)	(37)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(38)
mark^#(s(X))	→	mark^#(X)	(39)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(40)
mark^#(sel(X1,X2))	→	mark^#(X1)	(41)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(42)
head^#(active(X))	→	head^#(X)	(43)
2nd^#(mark(X))	→	2nd^#(X)	(44)
mark^#(sel(X1,X2))	→	mark^#(X2)	(45)
active^#(from(X))	→	s^#(X)	(46)
active^#(2nd(cons(X,XS)))	→	mark^#(head(XS))	(47)
active^#(take(0,XS))	→	mark^#(nil)	(48)
from^#(mark(X))	→	from^#(X)	(49)
mark^#(take(X1,X2))	→	take^#(mark(X1),mark(X2))	(50)
from^#(active(X))	→	from^#(X)	(51)
mark^#(from(X))	→	from^#(mark(X))	(52)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(53)
active^#(from(X))	→	cons^#(X,from(s(X)))	(54)
mark^#(head(X))	→	head^#(mark(X))	(55)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(56)
mark^#(cons(X1,X2))	→	mark^#(X1)	(57)
mark^#(nil)	→	active^#(nil)	(58)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(59)
head^#(mark(X))	→	head^#(X)	(60)
mark^#(sel(X1,X2))	→	sel^#(mark(X1),mark(X2))	(61)
mark^#(head(X))	→	active^#(head(mark(X)))	(62)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(63)
mark^#(from(X))	→	mark^#(X)	(64)
mark^#(head(X))	→	mark^#(X)	(65)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(66)
active^#(from(X))	→	from^#(s(X))	(67)
active^#(2nd(cons(X,XS)))	→	head^#(XS)	(68)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(69)
take^#(active(X1),X2)	→	take^#(X1,X2)	(70)
mark^#(take(X1,X2))	→	mark^#(X1)	(71)
take^#(X1,active(X2))	→	take^#(X1,X2)	(72)
mark^#(cons(X1,X2))	→	cons^#(mark(X1),X2)	(73)
active^#(take(s(N),cons(X,XS)))	→	take^#(N,XS)	(74)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(75)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(76)
mark^#(s(X))	→	s^#(mark(X))	(77)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(78)
2nd^#(active(X))	→	2nd^#(X)	(79)
mark^#(s(X))	→	active^#(s(mark(X)))	(80)
mark^#(2nd(X))	→	active^#(2nd(mark(X)))	(81)
active^#(take(s(N),cons(X,XS)))	→	cons^#(X,take(N,XS))	(82)
mark^#(2nd(X))	→	mark^#(X)	(83)
active^#(sel(s(N),cons(X,XS)))	→	sel^#(N,XS)	(84)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(85)
mark^#(0)	→	active^#(0)	(86)
s^#(mark(X))	→	s^#(X)	(87)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(88)
active^#(head(cons(X,XS)))	→	mark^#(X)	(89)
mark^#(from(X))	→	active^#(from(mark(X)))	(90)
mark^#(take(X1,X2))	→	mark^#(X2)	(91)
s^#(active(X))	→	s^#(X)	(92)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(93)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(94)
mark^#(2nd(X))	→	2nd^#(mark(X))	(95)

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

The 1^st component contains the pair

active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(94)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(69)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(93)
mark^#(head(X))	→	mark^#(X)	(65)
mark^#(from(X))	→	mark^#(X)	(64)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(63)
mark^#(head(X))	→	active^#(head(mark(X)))	(62)
mark^#(take(X1,X2))	→	mark^#(X2)	(91)
mark^#(from(X))	→	active^#(from(mark(X)))	(90)
active^#(head(cons(X,XS)))	→	mark^#(X)	(89)
mark^#(cons(X1,X2))	→	mark^#(X1)	(57)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(56)
mark^#(2nd(X))	→	mark^#(X)	(83)
mark^#(2nd(X))	→	active^#(2nd(mark(X)))	(81)
mark^#(s(X))	→	active^#(s(mark(X)))	(80)
active^#(2nd(cons(X,XS)))	→	mark^#(head(XS))	(47)
mark^#(sel(X1,X2))	→	mark^#(X2)	(45)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(76)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(75)
mark^#(sel(X1,X2))	→	mark^#(X1)	(41)
mark^#(take(X1,X2))	→	mark^#(X1)	(71)
mark^#(s(X))	→	mark^#(X)	(39)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

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

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

mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(56)
mark^#(s(X))	→	active^#(s(mark(X)))	(80)

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^#(from(X))	→	mark^#(X)	(64)
mark^#(from(X))	→	active^#(from(mark(X)))	(90)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(94)
active^#(2nd(cons(X,XS)))	→	mark^#(head(XS))	(47)
mark^#(sel(X1,X2))	→	mark^#(X2)	(45)
mark^#(sel(X1,X2))	→	mark^#(X1)	(41)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(76)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(63)
mark^#(s(X))	→	mark^#(X)	(39)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(69)
mark^#(2nd(X))	→	mark^#(X)	(83)
mark^#(2nd(X))	→	active^#(2nd(mark(X)))	(81)
mark^#(head(X))	→	mark^#(X)	(65)
mark^#(head(X))	→	active^#(head(mark(X)))	(62)
mark^#(cons(X1,X2))	→	mark^#(X1)	(57)
mark^#(take(X1,X2))	→	mark^#(X2)	(91)
mark^#(take(X1,X2))	→	mark^#(X1)	(71)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(75)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(93)
active^#(head(cons(X,XS)))	→	mark^#(X)	(89)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	max(0)
[take(x₁, x₂)]	=	max(x₁ + 8947, x₂ + 10090, 0)
[2nd(x₁)]	=	x₁ + 44023
[head^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1144
[sel^#(x₁, x₂)]	=	max(0)
[from(x₁)]	=	x₁ + 9228
[sel(x₁, x₂)]	=	max(x₁ + 26286, x₂ + 46824, 0)
[s^#(x₁)]	=	0
[nil]	=	10091
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[head(x₁)]	=	x₁ + 44022
[cons(x₁, x₂)]	=	max(x₁ + 8946, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

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

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

mark^#(from(X))	→	mark^#(X)	(64)
active^#(2nd(cons(X,XS)))	→	mark^#(head(XS))	(47)
mark^#(sel(X1,X2))	→	mark^#(X2)	(45)
mark^#(sel(X1,X2))	→	mark^#(X1)	(41)
mark^#(2nd(X))	→	mark^#(X)	(83)
mark^#(head(X))	→	mark^#(X)	(65)
mark^#(cons(X1,X2))	→	mark^#(X1)	(57)
mark^#(take(X1,X2))	→	mark^#(X2)	(91)
mark^#(take(X1,X2))	→	mark^#(X1)	(71)
active^#(sel(0,cons(X,XS)))	→	mark^#(X)	(93)
active^#(head(cons(X,XS)))	→	mark^#(X)	(89)

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^#(from(X))	→	active^#(from(mark(X)))	(90)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(94)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(76)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(63)
mark^#(s(X))	→	mark^#(X)	(39)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(69)
mark^#(2nd(X))	→	active^#(2nd(mark(X)))	(81)
mark^#(head(X))	→	active^#(head(mark(X)))	(62)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(75)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 3
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₂ + 3
[2nd(x₁)]	=	14139
[head^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	26931
[sel(x₁, x₂)]	=	2
[s^#(x₁)]	=	0
[nil]	=	1
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	1
[from^#(x₁)]	=	0
[active(x₁)]	=	2
[head(x₁)]	=	1105
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	2

together with the usable rules

cons(active(X1),X2)	→	cons(X1,X2)	(21)
sel(X1,active(X2))	→	sel(X1,X2)	(36)
head(active(X))	→	head(X)	(26)
cons(mark(X1),X2)	→	cons(X1,X2)	(19)
sel(X1,mark(X2))	→	sel(X1,X2)	(34)
cons(X1,active(X2))	→	cons(X1,X2)	(22)
sel(mark(X1),X2)	→	sel(X1,X2)	(33)
cons(X1,mark(X2))	→	cons(X1,X2)	(20)
head(mark(X))	→	head(X)	(25)
sel(active(X1),X2)	→	sel(X1,X2)	(35)

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

mark^#(from(X))	→	active^#(from(mark(X)))	(90)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(94)
active^#(take(s(N),cons(X,XS)))	→	mark^#(cons(X,take(N,XS)))	(63)
mark^#(s(X))	→	mark^#(X)	(39)
mark^#(2nd(X))	→	active^#(2nd(mark(X)))	(81)
mark^#(head(X))	→	active^#(head(mark(X)))	(62)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(75)

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^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(76)
active^#(sel(s(N),cons(X,XS)))	→	mark^#(sel(N,XS))	(69)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(s^#)	=	1
π(mark)	=	1
π(active)	=	1

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

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

and the following Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(x₁ + 1, 0)
[s(x₁)]	=	x₁ + 0
[take^#(x₁, x₂)]	=	1
[take(x₁, x₂)]	=	x₂ + 20978
[2nd(x₁)]	=	x₁ + 2999
[head^#(x₁)]	=	1
[mark^#(x₁)]	=	x₁ + 1
[0]	=	35658
[sel^#(x₁, x₂)]	=	x₁ + 1
[from(x₁)]	=	x₁ + 20981
[sel(x₁, x₂)]	=	x₁ + x₂ + 20980
[nil]	=	20977
[2nd^#(x₁)]	=	1
[from^#(x₁)]	=	1
[head(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	max(x₁ + 20979, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 1

together with the usable rules

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

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

active^#(sel(s(N),cons(X,XS)))

→

mark^#(sel(N,XS))

(69)

could be deleted.

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

2nd^#(active(X))	→	2nd^#(X)	(79)
2nd^#(mark(X))	→	2nd^#(X)	(44)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 21394
[2nd(x₁)]	=	0
[head^#(x₁)]	=	0
[mark^#(x₁)]	=	3
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	1
[sel(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[2nd^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	16022
[cons(x₁, x₂)]	=	x₁ + 3
[active^#(x₁)]	=	2

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

2nd^#(active(X))	→	2nd^#(X)	(79)
2nd^#(mark(X))	→	2nd^#(X)	(44)

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

head^#(mark(X))	→	head^#(X)	(60)
head^#(active(X))	→	head^#(X)	(43)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 7066
[2nd(x₁)]	=	0
[head^#(x₁)]	=	x₁ + 0
[mark^#(x₁)]	=	3
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	40400
[sel(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	16022
[cons(x₁, x₂)]	=	x₁ + 40402
[active^#(x₁)]	=	2

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

head^#(mark(X))	→	head^#(X)	(60)
head^#(active(X))	→	head^#(X)	(43)

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

sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(66)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(88)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(85)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(42)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

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

sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(66)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(88)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(85)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(42)

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

s^#(active(X))	→	s^#(X)	(92)
s^#(mark(X))	→	s^#(X)	(87)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	25192
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 15628
[2nd(x₁)]	=	0
[head^#(x₁)]	=	0
[mark^#(x₁)]	=	3
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	1
[sel(x₁, x₂)]	=	0
[s^#(x₁)]	=	x₁ + 0
[nil]	=	0
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	16022
[cons(x₁, x₂)]	=	x₁ + 3
[active^#(x₁)]	=	2

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

s^#(active(X))	→	s^#(X)	(92)
s^#(mark(X))	→	s^#(X)	(87)

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

from^#(active(X))	→	from^#(X)	(51)
from^#(mark(X))	→	from^#(X)	(49)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	25192
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[2nd(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[mark^#(x₁)]	=	3
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	1
[sel(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	14463
[cons(x₁, x₂)]	=	x₁ + 3
[active^#(x₁)]	=	2

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

from^#(active(X))	→	from^#(X)	(51)
from^#(mark(X))	→	from^#(X)	(49)

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

cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(59)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(53)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(40)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(38)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[2nd(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[mark^#(x₁)]	=	3
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	1
[sel(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 53622
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 53623
[head(x₁)]	=	3828
[cons(x₁, x₂)]	=	x₁ + 3
[active^#(x₁)]	=	2

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(53)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(38)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(40)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(59)

1.1.7.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[2nd(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[mark^#(x₁)]	=	3
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	26727
[sel(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	26731
[cons(x₁, x₂)]	=	x₁ + 26729
[active^#(x₁)]	=	2

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

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(40)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(59)

could be deleted.

1.1.7.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

take^#(X1,mark(X2))	→	take^#(X1,X2)	(78)
take^#(X1,active(X2))	→	take^#(X1,X2)	(72)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(37)
take^#(active(X1),X2)	→	take^#(X1,X2)	(70)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1184
[take^#(x₁, x₂)]	=	x₁ + x₂ + 0
[take(x₁, x₂)]	=	x₁ + x₂ + 1
[2nd(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[mark^#(x₁)]	=	3
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	25442
[sel(x₁, x₂)]	=	0
[s^#(x₁)]	=	0
[nil]	=	0
[2nd^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	25446
[cons(x₁, x₂)]	=	x₁ + 25444
[active^#(x₁)]	=	2

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

take^#(X1,mark(X2))	→	take^#(X1,X2)	(78)
take^#(X1,active(X2))	→	take^#(X1,X2)	(72)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(37)
take^#(active(X1),X2)	→	take^#(X1,X2)	(70)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.