Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex3_2_Luc97_iGM)

The rewrite relation of the following TRS is considered.

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

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^#(dbl(s(X)))	→	s^#(s(dbl(X)))	(39)
indx^#(X1,active(X2))	→	indx^#(X1,X2)	(40)
mark^#(dbl(X))	→	dbl^#(mark(X))	(41)
indx^#(X1,mark(X2))	→	indx^#(X1,X2)	(42)
mark^#(sel(X1,X2))	→	sel^#(mark(X1),mark(X2))	(43)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(44)
dbl^#(mark(X))	→	dbl^#(X)	(45)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(46)
mark^#(sel(X1,X2))	→	mark^#(X1)	(47)
active^#(indx(cons(X,Y),Z))	→	sel^#(X,Z)	(48)
mark^#(sel(X1,X2))	→	mark^#(X2)	(49)
active^#(dbls(cons(X,Y)))	→	dbl^#(X)	(50)
mark^#(indx(X1,X2))	→	indx^#(mark(X1),X2)	(51)
indx^#(active(X1),X2)	→	indx^#(X1,X2)	(52)
active^#(dbls(cons(X,Y)))	→	dbls^#(Y)	(53)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(54)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(55)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(56)
mark^#(dbls(X))	→	mark^#(X)	(57)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(58)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(59)
active^#(dbls(cons(X,Y)))	→	cons^#(dbl(X),dbls(Y))	(60)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(61)
mark^#(nil)	→	active^#(nil)	(62)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(63)
mark^#(dbls(X))	→	dbls^#(mark(X))	(64)
indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(65)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(66)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(67)
mark^#(dbl(X))	→	mark^#(X)	(68)
active^#(indx(cons(X,Y),Z))	→	cons^#(sel(X,Z),indx(Y,Z))	(69)
active^#(dbls(nil))	→	mark^#(nil)	(70)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(71)
dbls^#(mark(X))	→	dbls^#(X)	(72)
from^#(mark(X))	→	from^#(X)	(73)
mark^#(indx(X1,X2))	→	mark^#(X1)	(74)
active^#(sel(s(X),cons(Y,Z)))	→	sel^#(X,Z)	(75)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(76)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(77)
s^#(mark(X))	→	s^#(X)	(78)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(79)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(80)
s^#(active(X))	→	s^#(X)	(81)
active^#(indx(nil,X))	→	mark^#(nil)	(82)
mark^#(from(X))	→	active^#(from(X))	(83)
active^#(from(X))	→	s^#(X)	(84)
active^#(sel(0,cons(X,Y)))	→	mark^#(X)	(85)
dbls^#(active(X))	→	dbls^#(X)	(86)
dbl^#(active(X))	→	dbl^#(X)	(87)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(88)
mark^#(s(X))	→	active^#(s(X))	(89)
active^#(from(X))	→	from^#(s(X))	(90)
active^#(dbl(s(X)))	→	s^#(dbl(X))	(91)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(92)
active^#(indx(cons(X,Y),Z))	→	indx^#(Y,Z)	(93)
from^#(active(X))	→	from^#(X)	(94)
active^#(from(X))	→	cons^#(X,from(s(X)))	(95)
active^#(dbl(s(X)))	→	dbl^#(X)	(96)
active^#(dbl(0))	→	mark^#(0)	(97)
mark^#(0)	→	active^#(0)	(98)

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

The 1^st component contains the pair

mark^#(dbl(X))	→	mark^#(X)	(68)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(67)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(66)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(63)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(92)
mark^#(s(X))	→	active^#(s(X))	(89)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(59)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(58)
mark^#(dbls(X))	→	mark^#(X)	(57)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(56)
active^#(sel(0,cons(X,Y)))	→	mark^#(X)	(85)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(54)
mark^#(from(X))	→	active^#(from(X))	(83)
mark^#(sel(X1,X2))	→	mark^#(X2)	(49)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(79)
mark^#(sel(X1,X2))	→	mark^#(X1)	(47)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(46)
mark^#(indx(X1,X2))	→	mark^#(X1)	(74)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	45687
[dbls(x₁)]	=	45688
[dbl(x₁)]	=	45688
[indx(x₁, x₂)]	=	45688
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	45688
[0]	=	45690
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	45688
[from(x₁)]	=	45688
[s^#(x₁)]	=	0
[nil]	=	45690
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	45690
[cons(x₁, x₂)]	=	19781
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

s(mark(X))	→	s(X)	(21)
indx(X1,active(X2))	→	indx(X1,X2)	(36)
cons(X1,mark(X2))	→	cons(X1,X2)	(26)
dbl(mark(X))	→	dbl(X)	(19)
sel(X1,active(X2))	→	sel(X1,X2)	(32)
cons(active(X1),X2)	→	cons(X1,X2)	(27)
indx(X1,mark(X2))	→	indx(X1,X2)	(34)
s(active(X))	→	s(X)	(22)
cons(X1,active(X2))	→	cons(X1,X2)	(28)
indx(mark(X1),X2)	→	indx(X1,X2)	(33)
dbl(active(X))	→	dbl(X)	(20)
cons(mark(X1),X2)	→	cons(X1,X2)	(25)
sel(X1,mark(X2))	→	sel(X1,X2)	(30)
sel(active(X1),X2)	→	sel(X1,X2)	(31)
dbls(mark(X))	→	dbls(X)	(23)
dbls(active(X))	→	dbls(X)	(24)
from(active(X))	→	from(X)	(38)
from(mark(X))	→	from(X)	(37)
indx(active(X1),X2)	→	indx(X1,X2)	(35)
sel(mark(X1),X2)	→	sel(X1,X2)	(29)

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

mark^#(s(X))	→	active^#(s(X))	(89)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(54)

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))	→	active^#(from(X))	(83)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(66)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(56)
mark^#(sel(X1,X2))	→	mark^#(X2)	(49)
mark^#(sel(X1,X2))	→	mark^#(X1)	(47)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(63)
mark^#(indx(X1,X2))	→	mark^#(X1)	(74)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(46)
active^#(sel(0,cons(X,Y)))	→	mark^#(X)	(85)
mark^#(dbl(X))	→	mark^#(X)	(68)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(79)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(67)
mark^#(dbls(X))	→	mark^#(X)	(57)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(59)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(58)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(92)

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
[dbls(x₁)]	=	x₁ + 52871
[dbl(x₁)]	=	x₁ + 31892
[indx(x₁, x₂)]	=	max(x₁ + 50260, x₂ + 50261, 0)
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	max(0)
[indx^#(x₁, x₂)]	=	max(0)
[sel(x₁, x₂)]	=	max(x₁ + 50260, x₂ + 29283, 0)
[from(x₁)]	=	x₁ + 35659
[s^#(x₁)]	=	0
[nil]	=	50262
[mark(x₁)]	=	x₁ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	max(x₁ + 20978, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

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

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

mark^#(sel(X1,X2))	→	mark^#(X2)	(49)
mark^#(sel(X1,X2))	→	mark^#(X1)	(47)
mark^#(indx(X1,X2))	→	mark^#(X1)	(74)
active^#(sel(0,cons(X,Y)))	→	mark^#(X)	(85)
mark^#(dbl(X))	→	mark^#(X)	(68)
mark^#(dbls(X))	→	mark^#(X)	(57)

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(X))	(83)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(66)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(56)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(63)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(46)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(79)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(67)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(59)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(58)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(92)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	8843
[dbls(x₁)]	=	x₁ + 15107
[dbl(x₁)]	=	15107
[indx(x₁, x₂)]	=	15107
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	15106
[from(x₁)]	=	15107
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	21653
[from^#(x₁)]	=	0
[active(x₁)]	=	21652
[cons(x₁, x₂)]	=	14003
[active^#(x₁)]	=	15106

together with the usable rules

s(mark(X))	→	s(X)	(21)
cons(X1,mark(X2))	→	cons(X1,X2)	(26)
sel(X1,active(X2))	→	sel(X1,X2)	(32)
cons(active(X1),X2)	→	cons(X1,X2)	(27)
s(active(X))	→	s(X)	(22)
cons(X1,active(X2))	→	cons(X1,X2)	(28)
cons(mark(X1),X2)	→	cons(X1,X2)	(25)
sel(X1,mark(X2))	→	sel(X1,X2)	(30)
sel(active(X1),X2)	→	sel(X1,X2)	(31)
from(active(X))	→	from(X)	(38)
from(mark(X))	→	from(X)	(37)
sel(mark(X1),X2)	→	sel(X1,X2)	(29)

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

mark^#(from(X))	→	active^#(from(X))	(83)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(66)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(56)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(46)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(79)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(67)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(59)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(92)

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)))	(63)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(58)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

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

prec(cons^#)	=	0	status(cons^#)	=	[]	list-extension(cons^#)	=	Lex
prec(s)	=	1	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbls)	=	2	status(dbls)	=	[1]	list-extension(dbls)	=	Lex
prec(dbl)	=	2	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	4	status(indx)	=	[]	list-extension(indx)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(dbls^#)	=	0	status(dbls^#)	=	[]	list-extension(dbls^#)	=	Lex
prec(0)	=	3	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[2, 1]	list-extension(sel^#)	=	Lex
prec(indx^#)	=	0	status(indx^#)	=	[]	list-extension(indx^#)	=	Lex
prec(sel)	=	0	status(sel)	=	[1]	list-extension(sel)	=	Lex
prec(from)	=	2	status(from)	=	[]	list-extension(from)	=	Lex
prec(nil)	=	3	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(cons)	=	2	status(cons)	=	[]	list-extension(cons)	=	Lex

and the following Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	max(x₁ + 1, 0)
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 16910
[dbl(x₁)]	=	x₁ + 0
[indx(x₁, x₂)]	=	x₁ + x₂ + 16911
[dbl^#(x₁)]	=	1
[dbls^#(x₁)]	=	1
[0]	=	21238
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[indx^#(x₁, x₂)]	=	1
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 17750
[nil]	=	42199
[from^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 16909, x₂ + 0, 0)

together with the usable rules

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

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

active^#(sel(s(X),cons(Y,Z)))

→

mark^#(sel(X,Z))

(58)

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

sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(61)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(55)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(80)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(77)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 46172
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₂ + 47960
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	15106
[0]	=	4
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 2920
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 12701
[active^#(x₁)]	=	15106

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

sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(61)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(55)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(80)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(77)

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(71)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(88)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(76)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(44)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 25967
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₂ + 43619
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	15106
[0]	=	4
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 40940
[from(x₁)]	=	59112
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 32136
[active^#(x₁)]	=	15106

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(71)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(88)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(44)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(76)

1.1.3.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 12678
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₂ + 24121
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	15106
[0]	=	4
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	29635
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[active^#(x₁)]	=	15106

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

cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(44)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(76)

could be deleted.

1.1.3.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

from^#(active(X))	→	from^#(X)	(94)
from^#(mark(X))	→	from^#(X)	(73)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₂ + 4930
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	15106
[0]	=	4
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 44797
[from(x₁)]	=	41087
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 8823
[active^#(x₁)]	=	15106

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

from^#(active(X))	→	from^#(X)	(94)
from^#(mark(X))	→	from^#(X)	(73)

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

dbl^#(active(X))	→	dbl^#(X)	(87)
dbl^#(mark(X))	→	dbl^#(X)	(45)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 43050
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₂ + 39572
[dbl^#(x₁)]	=	x₁ + 0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	15106
[0]	=	10
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 18009
[from(x₁)]	=	1
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 26206
[active^#(x₁)]	=	15106

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

dbl^#(active(X))	→	dbl^#(X)	(87)
dbl^#(mark(X))	→	dbl^#(X)	(45)

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

indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(65)
indx^#(active(X1),X2)	→	indx^#(X1,X2)	(52)
indx^#(X1,mark(X2))	→	indx^#(X1,X2)	(42)
indx^#(X1,active(X2))	→	indx^#(X1,X2)	(40)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	15106
[0]	=	4
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	1
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[active^#(x₁)]	=	15106

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

indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(65)
indx^#(active(X1),X2)	→	indx^#(X1,X2)	(52)

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

indx^#(X1,active(X2))	→	indx^#(X1,X2)	(40)
indx^#(X1,mark(X2))	→	indx^#(X1,X2)	(42)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	1735
[indx(x₁, x₂)]	=	x₂ + 50609
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	15106
[0]	=	1737
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	x₂ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	25306
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[active^#(x₁)]	=	15106

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

indx^#(X1,active(X2))	→	indx^#(X1,X2)	(40)
indx^#(X1,mark(X2))	→	indx^#(X1,X2)	(42)

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^#(active(X))	→	s^#(X)	(81)
s^#(mark(X))	→	s^#(X)	(78)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 18255
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₂ + 79523
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	15106
[0]	=	4
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 44760
[from(x₁)]	=	1
[s^#(x₁)]	=	x₁ + 0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[active^#(x₁)]	=	15106

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

s^#(active(X))	→	s^#(X)	(81)
s^#(mark(X))	→	s^#(X)	(78)

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

dbls^#(active(X))	→	dbls^#(X)	(86)
dbls^#(mark(X))	→	dbls^#(X)	(72)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₂ + 37978
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	x₁ + 0
[mark^#(x₁)]	=	15106
[0]	=	4
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 41755
[from(x₁)]	=	50110
[s^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[cons(x₁, x₂)]	=	x₁ + x₂ + 8484
[active^#(x₁)]	=	15106

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

dbls^#(active(X))	→	dbls^#(X)	(86)
dbls^#(mark(X))	→	dbls^#(X)	(72)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.