Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_7_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)
active(dbl1(0))	→	mark(01)	(10)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
active(sel1(s(X),cons(Y,Z)))	→	mark(sel1(X,Z))	(13)
active(quote(0))	→	mark(01)	(14)
active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
active(quote(sel(X,Y)))	→	mark(sel1(X,Y))	(17)
mark(dbl(X))	→	active(dbl(mark(X)))	(18)
mark(0)	→	active(0)	(19)
mark(s(X))	→	active(s(X))	(20)
mark(dbls(X))	→	active(dbls(mark(X)))	(21)
mark(nil)	→	active(nil)	(22)
mark(cons(X1,X2))	→	active(cons(X1,X2))	(23)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(24)
mark(indx(X1,X2))	→	active(indx(mark(X1),X2))	(25)
mark(from(X))	→	active(from(X))	(26)
mark(dbl1(X))	→	active(dbl1(mark(X)))	(27)
mark(01)	→	active(01)	(28)
mark(s1(X))	→	active(s1(mark(X)))	(29)
mark(sel1(X1,X2))	→	active(sel1(mark(X1),mark(X2)))	(30)
mark(quote(X))	→	active(quote(mark(X)))	(31)
dbl(mark(X))	→	dbl(X)	(32)
dbl(active(X))	→	dbl(X)	(33)
s(mark(X))	→	s(X)	(34)
s(active(X))	→	s(X)	(35)
dbls(mark(X))	→	dbls(X)	(36)
dbls(active(X))	→	dbls(X)	(37)
cons(mark(X1),X2)	→	cons(X1,X2)	(38)
cons(X1,mark(X2))	→	cons(X1,X2)	(39)
cons(active(X1),X2)	→	cons(X1,X2)	(40)
cons(X1,active(X2))	→	cons(X1,X2)	(41)
sel(mark(X1),X2)	→	sel(X1,X2)	(42)
sel(X1,mark(X2))	→	sel(X1,X2)	(43)
sel(active(X1),X2)	→	sel(X1,X2)	(44)
sel(X1,active(X2))	→	sel(X1,X2)	(45)
indx(mark(X1),X2)	→	indx(X1,X2)	(46)
indx(X1,mark(X2))	→	indx(X1,X2)	(47)
indx(active(X1),X2)	→	indx(X1,X2)	(48)
indx(X1,active(X2))	→	indx(X1,X2)	(49)
from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)
dbl1(mark(X))	→	dbl1(X)	(52)
dbl1(active(X))	→	dbl1(X)	(53)
s1(mark(X))	→	s1(X)	(54)
s1(active(X))	→	s1(X)	(55)
sel1(mark(X1),X2)	→	sel1(X1,X2)	(56)
sel1(X1,mark(X2))	→	sel1(X1,X2)	(57)
sel1(active(X1),X2)	→	sel1(X1,X2)	(58)
sel1(X1,active(X2))	→	sel1(X1,X2)	(59)
quote(mark(X))	→	quote(X)	(60)
quote(active(X))	→	quote(X)	(61)

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)))	(62)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(63)
active^#(sel1(0,cons(X,Y)))	→	mark^#(X)	(64)
active^#(from(X))	→	cons^#(X,from(s(X)))	(65)
active^#(dbl1(s(X)))	→	dbl1^#(X)	(66)
active^#(dbls(nil))	→	mark^#(nil)	(67)
mark^#(nil)	→	active^#(nil)	(68)
mark^#(quote(X))	→	mark^#(X)	(69)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(70)
active^#(dbls(cons(X,Y)))	→	dbl^#(X)	(71)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(72)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(73)
mark^#(dbl(X))	→	dbl^#(mark(X))	(74)
from^#(mark(X))	→	from^#(X)	(75)
active^#(quote(s(X)))	→	s1^#(quote(X))	(76)
active^#(quote(sel(X,Y)))	→	sel1^#(X,Y)	(77)
sel1^#(mark(X1),X2)	→	sel1^#(X1,X2)	(78)
dbl1^#(mark(X))	→	dbl1^#(X)	(79)
quote^#(mark(X))	→	quote^#(X)	(80)
active^#(quote(0))	→	mark^#(01)	(81)
mark^#(0)	→	active^#(0)	(82)
dbl^#(mark(X))	→	dbl^#(X)	(83)
mark^#(s(X))	→	active^#(s(X))	(84)
active^#(dbl1(0))	→	mark^#(01)	(85)
mark^#(sel(X1,X2))	→	sel^#(mark(X1),mark(X2))	(86)
mark^#(s1(X))	→	active^#(s1(mark(X)))	(87)
active^#(indx(nil,X))	→	mark^#(nil)	(88)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(89)
s^#(mark(X))	→	s^#(X)	(90)
mark^#(sel(X1,X2))	→	mark^#(X2)	(91)
active^#(quote(s(X)))	→	mark^#(s1(quote(X)))	(92)
mark^#(sel1(X1,X2))	→	mark^#(X1)	(93)
dbls^#(active(X))	→	dbls^#(X)	(94)
s^#(active(X))	→	s^#(X)	(95)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(96)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(97)
mark^#(indx(X1,X2))	→	mark^#(X1)	(98)
mark^#(from(X))	→	active^#(from(X))	(99)
active^#(dbls(cons(X,Y)))	→	cons^#(dbl(X),dbls(Y))	(100)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(101)
mark^#(dbl1(X))	→	mark^#(X)	(102)
s1^#(active(X))	→	s1^#(X)	(103)
active^#(quote(dbl(X)))	→	mark^#(dbl1(X))	(104)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(105)
mark^#(quote(X))	→	quote^#(mark(X))	(106)
active^#(dbls(cons(X,Y)))	→	dbls^#(Y)	(107)
mark^#(dbl1(X))	→	dbl1^#(mark(X))	(108)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(109)
active^#(from(X))	→	s^#(X)	(110)
mark^#(dbls(X))	→	dbls^#(mark(X))	(111)
mark^#(indx(X1,X2))	→	indx^#(mark(X1),X2)	(112)
active^#(indx(cons(X,Y),Z))	→	indx^#(Y,Z)	(113)
active^#(quote(dbl(X)))	→	dbl1^#(X)	(114)
indx^#(X1,mark(X2))	→	indx^#(X1,X2)	(115)
dbl^#(active(X))	→	dbl^#(X)	(116)
active^#(from(X))	→	from^#(s(X))	(117)
mark^#(sel1(X1,X2))	→	mark^#(X2)	(118)
mark^#(sel1(X1,X2))	→	active^#(sel1(mark(X1),mark(X2)))	(119)
from^#(active(X))	→	from^#(X)	(120)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(121)
active^#(indx(cons(X,Y),Z))	→	sel^#(X,Z)	(122)
mark^#(s1(X))	→	s1^#(mark(X))	(123)
mark^#(sel(X1,X2))	→	mark^#(X1)	(124)
indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(125)
active^#(quote(s(X)))	→	quote^#(X)	(126)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(127)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(128)
active^#(dbl1(s(X)))	→	s1^#(s1(dbl1(X)))	(129)
active^#(quote(sel(X,Y)))	→	mark^#(sel1(X,Y))	(130)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(131)
mark^#(quote(X))	→	active^#(quote(mark(X)))	(132)
mark^#(01)	→	active^#(01)	(133)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(134)
sel1^#(X1,active(X2))	→	sel1^#(X1,X2)	(135)
active^#(dbl1(s(X)))	→	s1^#(dbl1(X))	(136)
active^#(dbl(0))	→	mark^#(0)	(137)
active^#(indx(cons(X,Y),Z))	→	cons^#(sel(X,Z),indx(Y,Z))	(138)
active^#(sel1(s(X),cons(Y,Z)))	→	sel1^#(X,Z)	(139)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(140)
sel1^#(active(X1),X2)	→	sel1^#(X1,X2)	(141)
active^#(dbl1(s(X)))	→	mark^#(s1(s1(dbl1(X))))	(142)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(143)
active^#(sel(0,cons(X,Y)))	→	mark^#(X)	(144)
active^#(sel1(s(X),cons(Y,Z)))	→	mark^#(sel1(X,Z))	(145)
mark^#(dbl(X))	→	mark^#(X)	(146)
s1^#(mark(X))	→	s1^#(X)	(147)
mark^#(dbl1(X))	→	active^#(dbl1(mark(X)))	(148)
sel1^#(X1,mark(X2))	→	sel1^#(X1,X2)	(149)
active^#(sel(s(X),cons(Y,Z)))	→	sel^#(X,Z)	(150)
indx^#(active(X1),X2)	→	indx^#(X1,X2)	(151)
active^#(dbl(s(X)))	→	s^#(dbl(X))	(152)
dbls^#(mark(X))	→	dbls^#(X)	(153)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(154)
indx^#(X1,active(X2))	→	indx^#(X1,X2)	(155)
mark^#(s1(X))	→	mark^#(X)	(156)
dbl1^#(active(X))	→	dbl1^#(X)	(157)
active^#(dbl(s(X)))	→	dbl^#(X)	(158)
mark^#(dbls(X))	→	mark^#(X)	(159)
mark^#(sel1(X1,X2))	→	sel1^#(mark(X1),mark(X2))	(160)
quote^#(active(X))	→	quote^#(X)	(161)

1.1 Dependency Graph Processor

The dependency pairs are split into 12 components.

The 1^st component contains the pair

mark^#(dbls(X))	→	mark^#(X)	(159)
mark^#(sel1(X1,X2))	→	mark^#(X2)	(118)
mark^#(sel1(X1,X2))	→	active^#(sel1(mark(X1),mark(X2)))	(119)
mark^#(s1(X))	→	mark^#(X)	(156)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(105)
active^#(quote(dbl(X)))	→	mark^#(dbl1(X))	(104)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(154)
mark^#(dbl1(X))	→	mark^#(X)	(102)
mark^#(from(X))	→	active^#(from(X))	(99)
mark^#(indx(X1,X2))	→	mark^#(X1)	(98)
mark^#(dbl1(X))	→	active^#(dbl1(mark(X)))	(148)
mark^#(dbl(X))	→	mark^#(X)	(146)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(97)
active^#(sel1(s(X),cons(Y,Z)))	→	mark^#(sel1(X,Z))	(145)
active^#(sel(0,cons(X,Y)))	→	mark^#(X)	(144)
mark^#(sel1(X1,X2))	→	mark^#(X1)	(93)
active^#(dbl1(s(X)))	→	mark^#(s1(s1(dbl1(X))))	(142)
active^#(quote(s(X)))	→	mark^#(s1(quote(X)))	(92)
mark^#(sel(X1,X2))	→	mark^#(X2)	(91)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(89)
mark^#(s1(X))	→	active^#(s1(mark(X)))	(87)
mark^#(s(X))	→	active^#(s(X))	(84)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(134)
mark^#(quote(X))	→	active^#(quote(mark(X)))	(132)
active^#(quote(sel(X,Y)))	→	mark^#(sel1(X,Y))	(130)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(73)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(127)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(72)
mark^#(quote(X))	→	mark^#(X)	(69)
mark^#(sel(X1,X2))	→	mark^#(X1)	(124)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(63)
active^#(sel1(0,cons(X,Y)))	→	mark^#(X)	(64)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(121)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[dbls(x₁)]	=	50052
[dbl(x₁)]	=	50052
[indx(x₁, x₂)]	=	50052
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	50052
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	50052
[from(x₁)]	=	50052
[s^#(x₁)]	=	0
[nil]	=	1
[dbl1(x₁)]	=	50052
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	1
[from^#(x₁)]	=	0
[active(x₁)]	=	2
[quote(x₁)]	=	50052
[cons(x₁, x₂)]	=	50051
[active^#(x₁)]	=	x₁ + 0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	50052
[s1(x₁)]	=	14923

together with the usable rules

from(mark(X))	→	from(X)	(50)
s1(mark(X))	→	s1(X)	(54)
dbls(mark(X))	→	dbls(X)	(36)
dbl(mark(X))	→	dbl(X)	(32)
quote(mark(X))	→	quote(X)	(60)
s(mark(X))	→	s(X)	(34)
sel(active(X1),X2)	→	sel(X1,X2)	(44)
dbl(active(X))	→	dbl(X)	(33)
cons(X1,mark(X2))	→	cons(X1,X2)	(39)
indx(X1,active(X2))	→	indx(X1,X2)	(49)
dbl1(mark(X))	→	dbl1(X)	(52)
sel1(mark(X1),X2)	→	sel1(X1,X2)	(56)
sel(X1,active(X2))	→	sel(X1,X2)	(45)
sel1(X1,mark(X2))	→	sel1(X1,X2)	(57)
from(active(X))	→	from(X)	(51)
cons(active(X1),X2)	→	cons(X1,X2)	(40)
s1(active(X))	→	s1(X)	(55)
sel1(X1,active(X2))	→	sel1(X1,X2)	(59)
cons(mark(X1),X2)	→	cons(X1,X2)	(38)
quote(active(X))	→	quote(X)	(61)
sel1(active(X1),X2)	→	sel1(X1,X2)	(58)
indx(active(X1),X2)	→	indx(X1,X2)	(48)
dbl1(active(X))	→	dbl1(X)	(53)
indx(X1,mark(X2))	→	indx(X1,X2)	(47)
dbls(active(X))	→	dbls(X)	(37)
cons(X1,active(X2))	→	cons(X1,X2)	(41)
sel(mark(X1),X2)	→	sel(X1,X2)	(42)
indx(mark(X1),X2)	→	indx(X1,X2)	(46)
s(active(X))	→	s(X)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(43)

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

mark^#(s1(X))	→	active^#(s1(mark(X)))	(87)
mark^#(s(X))	→	active^#(s(X))	(84)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(72)

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^#(dbl(X))	→	mark^#(X)	(146)
mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(97)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(127)
active^#(quote(s(X)))	→	mark^#(s1(quote(X)))	(92)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(63)
active^#(quote(dbl(X)))	→	mark^#(dbl1(X))	(104)
mark^#(dbls(X))	→	mark^#(X)	(159)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(105)
mark^#(from(X))	→	active^#(from(X))	(99)
active^#(quote(sel(X,Y)))	→	mark^#(sel1(X,Y))	(130)
mark^#(dbl1(X))	→	mark^#(X)	(102)
mark^#(dbl1(X))	→	active^#(dbl1(mark(X)))	(148)
active^#(sel(0,cons(X,Y)))	→	mark^#(X)	(144)
mark^#(indx(X1,X2))	→	mark^#(X1)	(98)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(89)
mark^#(sel1(X1,X2))	→	mark^#(X2)	(118)
mark^#(sel1(X1,X2))	→	mark^#(X1)	(93)
mark^#(sel1(X1,X2))	→	active^#(sel1(mark(X1),mark(X2)))	(119)
mark^#(quote(X))	→	mark^#(X)	(69)
mark^#(quote(X))	→	active^#(quote(mark(X)))	(132)
active^#(sel1(0,cons(X,Y)))	→	mark^#(X)	(64)
mark^#(sel(X1,X2))	→	mark^#(X2)	(91)
mark^#(sel(X1,X2))	→	mark^#(X1)	(124)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(73)
active^#(dbl1(s(X)))	→	mark^#(s1(s1(dbl1(X))))	(142)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(134)
active^#(sel1(s(X),cons(Y,Z)))	→	mark^#(sel1(X,Z))	(145)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(121)
mark^#(s1(X))	→	mark^#(X)	(156)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(154)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 1
[indx(x₁, x₂)]	=	max(x₁ + 2, x₂ + 6, 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₁ + 1, x₂ + 3, 0)
[from(x₁)]	=	x₁ + 3
[s^#(x₁)]	=	0
[nil]	=	7
[dbl1(x₁)]	=	x₁ + 1
[sel1^#(x₁, x₂)]	=	max(0)
[mark(x₁)]	=	x₁ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[quote(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	max(x₁ + 1, x₂ + 3, 0)
[s1(x₁)]	=	x₁ + 0

together with the usable rules

mark(dbl(X))	→	active(dbl(mark(X)))	(18)
from(mark(X))	→	from(X)	(50)
active(dbls(cons(X,Y)))	→	mark(cons(dbl(X),dbls(Y)))	(4)
active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(indx(cons(X,Y),Z))	→	mark(cons(sel(X,Z),indx(Y,Z)))	(8)
s1(mark(X))	→	s1(X)	(54)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
mark(dbls(X))	→	active(dbls(mark(X)))	(21)
dbls(mark(X))	→	dbls(X)	(36)
mark(from(X))	→	active(from(X))	(26)
mark(0)	→	active(0)	(19)
dbl(mark(X))	→	dbl(X)	(32)
active(quote(sel(X,Y)))	→	mark(sel1(X,Y))	(17)
quote(mark(X))	→	quote(X)	(60)
mark(dbl1(X))	→	active(dbl1(mark(X)))	(27)
s(mark(X))	→	s(X)	(34)
mark(nil)	→	active(nil)	(22)
mark(01)	→	active(01)	(28)
sel(active(X1),X2)	→	sel(X1,X2)	(44)
active(sel(0,cons(X,Y)))	→	mark(X)	(5)
dbl(active(X))	→	dbl(X)	(33)
active(dbl1(0))	→	mark(01)	(10)
cons(X1,mark(X2))	→	cons(X1,X2)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
mark(s(X))	→	active(s(X))	(20)
mark(indx(X1,X2))	→	active(indx(mark(X1),X2))	(25)
indx(X1,active(X2))	→	indx(X1,X2)	(49)
dbl1(mark(X))	→	dbl1(X)	(52)
mark(sel1(X1,X2))	→	active(sel1(mark(X1),mark(X2)))	(30)
active(quote(0))	→	mark(01)	(14)
sel1(mark(X1),X2)	→	sel1(X1,X2)	(56)
mark(quote(X))	→	active(quote(mark(X)))	(31)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
sel(X1,active(X2))	→	sel(X1,X2)	(45)
mark(cons(X1,X2))	→	active(cons(X1,X2))	(23)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(24)
sel1(X1,mark(X2))	→	sel1(X1,X2)	(57)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
active(from(X))	→	mark(cons(X,from(s(X))))	(9)
active(sel1(s(X),cons(Y,Z)))	→	mark(sel1(X,Z))	(13)
from(active(X))	→	from(X)	(51)
cons(active(X1),X2)	→	cons(X1,X2)	(40)
s1(active(X))	→	s1(X)	(55)
sel1(X1,active(X2))	→	sel1(X1,X2)	(59)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(6)
cons(mark(X1),X2)	→	cons(X1,X2)	(38)
quote(active(X))	→	quote(X)	(61)
sel1(active(X1),X2)	→	sel1(X1,X2)	(58)
indx(active(X1),X2)	→	indx(X1,X2)	(48)
dbl1(active(X))	→	dbl1(X)	(53)
indx(X1,mark(X2))	→	indx(X1,X2)	(47)
dbls(active(X))	→	dbls(X)	(37)
cons(X1,active(X2))	→	cons(X1,X2)	(41)
sel(mark(X1),X2)	→	sel(X1,X2)	(42)
indx(mark(X1),X2)	→	indx(X1,X2)	(46)
s(active(X))	→	s(X)	(35)
mark(s1(X))	→	active(s1(mark(X)))	(29)
sel(X1,mark(X2))	→	sel(X1,X2)	(43)
active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(2)

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

mark^#(dbl(X))	→	mark^#(X)	(146)
active^#(quote(dbl(X)))	→	mark^#(dbl1(X))	(104)
mark^#(dbls(X))	→	mark^#(X)	(159)
active^#(quote(sel(X,Y)))	→	mark^#(sel1(X,Y))	(130)
mark^#(dbl1(X))	→	mark^#(X)	(102)
active^#(sel(0,cons(X,Y)))	→	mark^#(X)	(144)
mark^#(indx(X1,X2))	→	mark^#(X1)	(98)
mark^#(sel1(X1,X2))	→	mark^#(X2)	(118)
mark^#(sel1(X1,X2))	→	mark^#(X1)	(93)
mark^#(quote(X))	→	mark^#(X)	(69)
active^#(sel1(0,cons(X,Y)))	→	mark^#(X)	(64)
mark^#(sel(X1,X2))	→	mark^#(X2)	(91)
mark^#(sel(X1,X2))	→	mark^#(X1)	(124)

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^#(dbl(X))	→	active^#(dbl(mark(X)))	(97)
active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(127)
active^#(quote(s(X)))	→	mark^#(s1(quote(X)))	(92)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(63)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(105)
mark^#(from(X))	→	active^#(from(X))	(99)
mark^#(dbl1(X))	→	active^#(dbl1(mark(X)))	(148)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(89)
mark^#(sel1(X1,X2))	→	active^#(sel1(mark(X1),mark(X2)))	(119)
mark^#(quote(X))	→	active^#(quote(mark(X)))	(132)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(73)
active^#(dbl1(s(X)))	→	mark^#(s1(s1(dbl1(X))))	(142)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(134)
active^#(sel1(s(X),cons(Y,Z)))	→	mark^#(sel1(X,Z))	(145)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(121)
mark^#(s1(X))	→	mark^#(X)	(156)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(154)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 3
[dbl(x₁)]	=	2
[indx(x₁, x₂)]	=	x₁ + x₂ + 3
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	2
[from(x₁)]	=	x₁ + 3
[s^#(x₁)]	=	0
[nil]	=	0
[dbl1(x₁)]	=	2
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 30219
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[quote(x₁)]	=	2
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	2
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	2
[s1(x₁)]	=	x₁ + 0

together with the usable rules

s1(mark(X))	→	s1(X)	(54)
dbl(mark(X))	→	dbl(X)	(32)
quote(mark(X))	→	quote(X)	(60)
s(mark(X))	→	s(X)	(34)
sel(active(X1),X2)	→	sel(X1,X2)	(44)
dbl(active(X))	→	dbl(X)	(33)
cons(X1,mark(X2))	→	cons(X1,X2)	(39)
dbl1(mark(X))	→	dbl1(X)	(52)
sel1(mark(X1),X2)	→	sel1(X1,X2)	(56)
sel(X1,active(X2))	→	sel(X1,X2)	(45)
sel1(X1,mark(X2))	→	sel1(X1,X2)	(57)
cons(active(X1),X2)	→	cons(X1,X2)	(40)
s1(active(X))	→	s1(X)	(55)
sel1(X1,active(X2))	→	sel1(X1,X2)	(59)
cons(mark(X1),X2)	→	cons(X1,X2)	(38)
quote(active(X))	→	quote(X)	(61)
sel1(active(X1),X2)	→	sel1(X1,X2)	(58)
dbl1(active(X))	→	dbl1(X)	(53)
cons(X1,active(X2))	→	cons(X1,X2)	(41)
sel(mark(X1),X2)	→	sel(X1,X2)	(42)
s(active(X))	→	s(X)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(43)

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

active^#(dbls(cons(X,Y)))	→	mark^#(cons(dbl(X),dbls(Y)))	(127)
active^#(indx(cons(X,Y),Z))	→	mark^#(cons(sel(X,Z),indx(Y,Z)))	(63)
mark^#(dbls(X))	→	active^#(dbls(mark(X)))	(105)
mark^#(from(X))	→	active^#(from(X))	(99)
mark^#(indx(X1,X2))	→	active^#(indx(mark(X1),X2))	(89)
active^#(from(X))	→	mark^#(cons(X,from(s(X))))	(134)

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^#(dbl(X))	→	active^#(dbl(mark(X)))	(97)
active^#(quote(s(X)))	→	mark^#(s1(quote(X)))	(92)
mark^#(dbl1(X))	→	active^#(dbl1(mark(X)))	(148)
mark^#(sel1(X1,X2))	→	active^#(sel1(mark(X1),mark(X2)))	(119)
mark^#(quote(X))	→	active^#(quote(mark(X)))	(132)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(73)
active^#(dbl1(s(X)))	→	mark^#(s1(s1(dbl1(X))))	(142)
active^#(sel1(s(X),cons(Y,Z)))	→	mark^#(sel1(X,Z))	(145)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(121)
mark^#(s1(X))	→	mark^#(X)	(156)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(154)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 10284
[indx(x₁, x₂)]	=	x₁ + x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	28776
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	2
[from(x₁)]	=	x₁ + 2
[s^#(x₁)]	=	0
[nil]	=	0
[dbl1(x₁)]	=	2
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 16028
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[quote(x₁)]	=	2
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	2
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	2
[s1(x₁)]	=	x₁ + 0

together with the usable rules

s1(mark(X))	→	s1(X)	(54)
quote(mark(X))	→	quote(X)	(60)
s(mark(X))	→	s(X)	(34)
sel(active(X1),X2)	→	sel(X1,X2)	(44)
cons(X1,mark(X2))	→	cons(X1,X2)	(39)
dbl1(mark(X))	→	dbl1(X)	(52)
sel1(mark(X1),X2)	→	sel1(X1,X2)	(56)
sel(X1,active(X2))	→	sel(X1,X2)	(45)
sel1(X1,mark(X2))	→	sel1(X1,X2)	(57)
cons(active(X1),X2)	→	cons(X1,X2)	(40)
s1(active(X))	→	s1(X)	(55)
sel1(X1,active(X2))	→	sel1(X1,X2)	(59)
cons(mark(X1),X2)	→	cons(X1,X2)	(38)
quote(active(X))	→	quote(X)	(61)
sel1(active(X1),X2)	→	sel1(X1,X2)	(58)
dbl1(active(X))	→	dbl1(X)	(53)
cons(X1,active(X2))	→	cons(X1,X2)	(41)
sel(mark(X1),X2)	→	sel(X1,X2)	(42)
s(active(X))	→	s(X)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(43)

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

mark^#(dbl(X))	→	active^#(dbl(mark(X)))	(97)
active^#(dbl(s(X)))	→	mark^#(s(s(dbl(X))))	(154)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(quote(s(X)))	→	mark^#(s1(quote(X)))	(92)
mark^#(dbl1(X))	→	active^#(dbl1(mark(X)))	(148)
mark^#(sel1(X1,X2))	→	active^#(sel1(mark(X1),mark(X2)))	(119)
mark^#(quote(X))	→	active^#(quote(mark(X)))	(132)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(73)
active^#(dbl1(s(X)))	→	mark^#(s1(s1(dbl1(X))))	(142)
active^#(sel1(s(X),cons(Y,Z)))	→	mark^#(sel1(X,Z))	(145)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(121)
mark^#(s1(X))	→	mark^#(X)	(156)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(dbl^#)	=	1
π(dbls^#)	=	1
π(mark^#)	=	1
π(s^#)	=	1
π(dbl1)	=	1
π(mark)	=	1
π(active)	=	1
π(quote)	=	1
π(active^#)	=	1
π(quote^#)	=	1

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

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

and the following Max-polynomial interpretation

[dbl1^#(x₁)]	=	1
[01]	=	10282
[cons^#(x₁, x₂)]	=	max(x₁ + 1, 0)
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 66293
[dbl(x₁)]	=	x₁ + 66293
[indx(x₁, x₂)]	=	x₁ + x₂ + 41956
[0]	=	10282
[sel^#(x₁, x₂)]	=	1
[indx^#(x₁, x₂)]	=	x₂ + 1
[sel(x₁, x₂)]	=	x₁ + x₂ + 41956
[from(x₁)]	=	x₁ + 41956
[nil]	=	37986
[sel1^#(x₁, x₂)]	=	x₁ + x₂ + 1
[from^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 41955, x₂ + 0, 0)
[s1^#(x₁)]	=	1
[sel1(x₁, x₂)]	=	x₁ + x₂ + 41954
[s1(x₁)]	=	x₁ + 0

together with the usable rules

mark(dbl(X))	→	active(dbl(mark(X)))	(18)
from(mark(X))	→	from(X)	(50)
active(dbls(cons(X,Y)))	→	mark(cons(dbl(X),dbls(Y)))	(4)
active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(indx(cons(X,Y),Z))	→	mark(cons(sel(X,Z),indx(Y,Z)))	(8)
s1(mark(X))	→	s1(X)	(54)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
mark(dbls(X))	→	active(dbls(mark(X)))	(21)
dbls(mark(X))	→	dbls(X)	(36)
mark(from(X))	→	active(from(X))	(26)
mark(0)	→	active(0)	(19)
dbl(mark(X))	→	dbl(X)	(32)
active(quote(sel(X,Y)))	→	mark(sel1(X,Y))	(17)
quote(mark(X))	→	quote(X)	(60)
mark(dbl1(X))	→	active(dbl1(mark(X)))	(27)
s(mark(X))	→	s(X)	(34)
mark(nil)	→	active(nil)	(22)
mark(01)	→	active(01)	(28)
sel(active(X1),X2)	→	sel(X1,X2)	(44)
active(sel(0,cons(X,Y)))	→	mark(X)	(5)
dbl(active(X))	→	dbl(X)	(33)
active(dbl1(0))	→	mark(01)	(10)
cons(X1,mark(X2))	→	cons(X1,X2)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
mark(s(X))	→	active(s(X))	(20)
mark(indx(X1,X2))	→	active(indx(mark(X1),X2))	(25)
indx(X1,active(X2))	→	indx(X1,X2)	(49)
dbl1(mark(X))	→	dbl1(X)	(52)
mark(sel1(X1,X2))	→	active(sel1(mark(X1),mark(X2)))	(30)
active(quote(0))	→	mark(01)	(14)
sel1(mark(X1),X2)	→	sel1(X1,X2)	(56)
mark(quote(X))	→	active(quote(mark(X)))	(31)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
sel(X1,active(X2))	→	sel(X1,X2)	(45)
mark(cons(X1,X2))	→	active(cons(X1,X2))	(23)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(24)
sel1(X1,mark(X2))	→	sel1(X1,X2)	(57)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
active(from(X))	→	mark(cons(X,from(s(X))))	(9)
active(sel1(s(X),cons(Y,Z)))	→	mark(sel1(X,Z))	(13)
from(active(X))	→	from(X)	(51)
cons(active(X1),X2)	→	cons(X1,X2)	(40)
s1(active(X))	→	s1(X)	(55)
sel1(X1,active(X2))	→	sel1(X1,X2)	(59)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(6)
cons(mark(X1),X2)	→	cons(X1,X2)	(38)
quote(active(X))	→	quote(X)	(61)
sel1(active(X1),X2)	→	sel1(X1,X2)	(58)
indx(active(X1),X2)	→	indx(X1,X2)	(48)
dbl1(active(X))	→	dbl1(X)	(53)
indx(X1,mark(X2))	→	indx(X1,X2)	(47)
dbls(active(X))	→	dbls(X)	(37)
cons(X1,active(X2))	→	cons(X1,X2)	(41)
sel(mark(X1),X2)	→	sel(X1,X2)	(42)
indx(mark(X1),X2)	→	indx(X1,X2)	(46)
s(active(X))	→	s(X)	(35)
mark(s1(X))	→	active(s1(mark(X)))	(29)
sel(X1,mark(X2))	→	sel(X1,X2)	(43)
active(dbl(s(X)))	→	mark(s(s(dbl(X))))	(2)

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

active^#(quote(s(X)))	→	mark^#(s1(quote(X)))	(92)
active^#(dbl1(s(X)))	→	mark^#(s1(s1(dbl1(X))))	(142)
active^#(sel1(s(X),cons(Y,Z)))	→	mark^#(sel1(X,Z))	(145)
mark^#(s1(X))	→	mark^#(X)	(156)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(dbl1(X))	→	active^#(dbl1(mark(X)))	(148)
mark^#(sel1(X1,X2))	→	active^#(sel1(mark(X1),mark(X2)))	(119)
mark^#(quote(X))	→	active^#(quote(mark(X)))	(132)
mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(73)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(121)

1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	3
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	26357
[dbls(x₁)]	=	3701
[dbl(x₁)]	=	1
[indx(x₁, x₂)]	=	1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	4
[0]	=	0
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	4
[from(x₁)]	=	3
[s^#(x₁)]	=	0
[nil]	=	16961
[dbl1(x₁)]	=	3
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	2
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[quote(x₁)]	=	3
[cons(x₁, x₂)]	=	0
[active^#(x₁)]	=	x₁ + 0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	1
[s1(x₁)]	=	3139

together with the usable rules

from(mark(X))	→	from(X)	(50)
s1(mark(X))	→	s1(X)	(54)
dbls(mark(X))	→	dbls(X)	(36)
dbl(mark(X))	→	dbl(X)	(32)
quote(mark(X))	→	quote(X)	(60)
s(mark(X))	→	s(X)	(34)
sel(active(X1),X2)	→	sel(X1,X2)	(44)
dbl(active(X))	→	dbl(X)	(33)
cons(X1,mark(X2))	→	cons(X1,X2)	(39)
indx(X1,active(X2))	→	indx(X1,X2)	(49)
dbl1(mark(X))	→	dbl1(X)	(52)
sel1(mark(X1),X2)	→	sel1(X1,X2)	(56)
sel(X1,active(X2))	→	sel(X1,X2)	(45)
sel1(X1,mark(X2))	→	sel1(X1,X2)	(57)
from(active(X))	→	from(X)	(51)
cons(active(X1),X2)	→	cons(X1,X2)	(40)
s1(active(X))	→	s1(X)	(55)
sel1(X1,active(X2))	→	sel1(X1,X2)	(59)
cons(mark(X1),X2)	→	cons(X1,X2)	(38)
quote(active(X))	→	quote(X)	(61)
sel1(active(X1),X2)	→	sel1(X1,X2)	(58)
indx(active(X1),X2)	→	indx(X1,X2)	(48)
dbl1(active(X))	→	dbl1(X)	(53)
indx(X1,mark(X2))	→	indx(X1,X2)	(47)
dbls(active(X))	→	dbls(X)	(37)
cons(X1,active(X2))	→	cons(X1,X2)	(41)
sel(mark(X1),X2)	→	sel(X1,X2)	(42)
indx(mark(X1),X2)	→	indx(X1,X2)	(46)
s(active(X))	→	s(X)	(35)
sel(X1,mark(X2))	→	sel(X1,X2)	(43)

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

mark^#(dbl1(X))	→	active^#(dbl1(mark(X)))	(148)
mark^#(sel1(X1,X2))	→	active^#(sel1(mark(X1),mark(X2)))	(119)
mark^#(quote(X))	→	active^#(quote(mark(X)))	(132)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

mark^#(sel(X1,X2))	→	active^#(sel(mark(X1),mark(X2)))	(73)
active^#(sel(s(X),cons(Y,Z)))	→	mark^#(sel(X,Z))	(121)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(dbl^#)	=	1
π(dbls^#)	=	1
π(mark^#)	=	1
π(s^#)	=	1
π(dbl1)	=	1
π(mark)	=	1
π(active)	=	1
π(active^#)	=	1
π(quote^#)	=	1

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

prec(dbl1^#)	=	0	status(dbl1^#)	=	[]	list-extension(dbl1^#)	=	Lex
prec(01)	=	5	status(01)	=	[]	list-extension(01)	=	Lex
prec(cons^#)	=	0	status(cons^#)	=	[]	list-extension(cons^#)	=	Lex
prec(s)	=	4	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbls)	=	3	status(dbls)	=	[]	list-extension(dbls)	=	Lex
prec(dbl)	=	5	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	3	status(indx)	=	[2, 1]	list-extension(indx)	=	Lex
prec(0)	=	5	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(indx^#)	=	0	status(indx^#)	=	[]	list-extension(indx^#)	=	Lex
prec(sel)	=	1	status(sel)	=	[1, 2]	list-extension(sel)	=	Lex
prec(from)	=	1	status(from)	=	[1]	list-extension(from)	=	Lex
prec(nil)	=	3	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(sel1^#)	=	0	status(sel1^#)	=	[1, 2]	list-extension(sel1^#)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(quote)	=	6	status(quote)	=	[1]	list-extension(quote)	=	Lex
prec(cons)	=	1	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(s1^#)	=	0	status(s1^#)	=	[]	list-extension(s1^#)	=	Lex
prec(sel1)	=	5	status(sel1)	=	[]	list-extension(sel1)	=	Lex
prec(s1)	=	1	status(s1)	=	[]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

[dbl1^#(x₁)]	=	1
[01]	=	1
[cons^#(x₁, x₂)]	=	max(x₁ + 1, 0)
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 3
[dbl(x₁)]	=	x₁ + 3
[indx(x₁, x₂)]	=	x₁ + x₂ + 3
[0]	=	1
[sel^#(x₁, x₂)]	=	1
[indx^#(x₁, x₂)]	=	x₂ + 1
[sel(x₁, x₂)]	=	x₁ + x₂ + 3
[from(x₁)]	=	x₁ + 14925
[nil]	=	26340
[sel1^#(x₁, x₂)]	=	x₁ + x₂ + 1
[from^#(x₁)]	=	1
[quote(x₁)]	=	x₁ + 18874
[cons(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[s1^#(x₁)]	=	1
[sel1(x₁, x₂)]	=	x₂ + 1
[s1(x₁)]	=	x₁ + 0

together with the usable rules

mark(dbl(X))	→	active(dbl(mark(X)))	(18)
from(mark(X))	→	from(X)	(50)
active(dbls(cons(X,Y)))	→	mark(cons(dbl(X),dbls(Y)))	(4)
active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(indx(cons(X,Y),Z))	→	mark(cons(sel(X,Z),indx(Y,Z)))	(8)
s1(mark(X))	→	s1(X)	(54)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
mark(dbls(X))	→	active(dbls(mark(X)))	(21)
dbls(mark(X))	→	dbls(X)	(36)
mark(from(X))	→	active(from(X))	(26)
mark(0)	→	active(0)	(19)
dbl(mark(X))	→	dbl(X)	(32)
active(quote(sel(X,Y)))	→	mark(sel1(X,Y))	(17)
quote(mark(X))	→	quote(X)	(60)
mark(dbl1(X))	→	active(dbl1(mark(X)))	(27)
s(mark(X))	→	s(X)	(34)
mark(nil)	→	active(nil)	(22)
mark(01)	→	active(01)	(28)
sel(active(X1),X2)	→	sel(X1,X2)	(44)
active(sel(0,cons(X,Y)))	→	mark(X)	(5)
dbl(active(X))	→	dbl(X)	(33)
active(dbl1(0))	→	mark(01)	(10)
cons(X1,mark(X2))	→	cons(X1,X2)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
mark(s(X))	→	active(s(X))	(20)
mark(indx(X1,X2))	→	active(indx(mark(X1),X2))	(25)
indx(X1,active(X2))	→	indx(X1,X2)	(49)
dbl1(mark(X))	→	dbl1(X)	(52)
mark(sel1(X1,X2))	→	active(sel1(mark(X1),mark(X2)))	(30)
active(quote(0))	→	mark(01)	(14)
sel1(mark(X1),X2)	→	sel1(X1,X2)	(56)
mark(quote(X))	→	active(quote(mark(X)))	(31)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
sel(X1,active(X2))	→	sel(X1,X2)	(45)
mark(cons(X1,X2))	→	active(cons(X1,X2))	(23)
mark(sel(X1,X2))	→	active(sel(mark(X1),mark(X2)))	(24)
sel1(X1,mark(X2))	→	sel1(X1,X2)	(57)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
active(from(X))	→	mark(cons(X,from(s(X))))	(9)
active(sel1(s(X),cons(Y,Z)))	→	mark(sel1(X,Z))	(13)
from(active(X))	→	from(X)	(51)
cons(active(X1),X2)	→	cons(X1,X2)	(40)
s1(active(X))	→	s1(X)	(55)
sel1(X1,active(X2))	→	sel1(X1,X2)	(59)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(6)
cons(mark(X1),X2)	→	cons(X1,X2)	(38)
quote(active(X))	→	quote(X)	(61)
sel1(active(X1),X2)	→	sel1(X1,X2)	(58)
indx(active(X1),X2)	→	indx(X1,X2)	(48)
dbl1(active(X))	→	dbl1(X)	(53)
indx(X1,mark(X2))	→	indx(X1,X2)	(47)
dbls(active(X))	→	dbls(X)	(37)
cons(X1,active(X2))	→	cons(X1,X2)	(41)
sel(mark(X1),X2)	→	sel(X1,X2)	(42)
indx(mark(X1),X2)	→	indx(X1,X2)	(46)
s(active(X))	→	s(X)	(35)
mark(s1(X))	→	active(s1(mark(X)))	(29)
sel(X1,mark(X2))	→	sel(X1,X2)	(43)
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))

(121)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

from^#(active(X))	→	from^#(X)	(120)
from^#(mark(X))	→	from^#(X)	(75)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	32953
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	3
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	1
[indx(x₁, x₂)]	=	x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	1
[from(x₁)]	=	11204
[s^#(x₁)]	=	0
[nil]	=	3
[dbl1(x₁)]	=	32951
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 2
[quote(x₁)]	=	x₁ + 32948
[cons(x₁, x₂)]	=	14624
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + 32951
[s1(x₁)]	=	32953

together with the usable rules

from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)

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

from^#(active(X))	→	from^#(X)	(120)
from^#(mark(X))	→	from^#(X)	(75)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

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

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	15717
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	3
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	1
[indx(x₁, x₂)]	=	x₂ + 50143
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	7024
[from(x₁)]	=	5680
[s^#(x₁)]	=	x₁ + 0
[nil]	=	50145
[dbl1(x₁)]	=	15715
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[quote(x₁)]	=	x₁ + 15712
[cons(x₁, x₂)]	=	50145
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + 22738
[s1(x₁)]	=	15717

together with the usable rules

from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)

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

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

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

sel1^#(X1,mark(X2))	→	sel1^#(X1,X2)	(149)
sel1^#(active(X1),X2)	→	sel1^#(X1,X2)	(141)
sel1^#(X1,active(X2))	→	sel1^#(X1,X2)	(135)
sel1^#(mark(X1),X2)	→	sel1^#(X1,X2)	(78)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	6
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1317
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	1
[indx(x₁, x₂)]	=	x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	1
[from(x₁)]	=	1
[s^#(x₁)]	=	0
[nil]	=	3
[dbl1(x₁)]	=	4
[sel1^#(x₁, x₂)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[quote(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	3
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + 4
[s1(x₁)]	=	21297

together with the usable rules

from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)

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

sel1^#(active(X1),X2)	→	sel1^#(X1,X2)	(141)
sel1^#(mark(X1),X2)	→	sel1^#(X1,X2)	(78)

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

sel1^#(X1,mark(X2))	→	sel1^#(X1,X2)	(149)
sel1^#(X1,active(X2))	→	sel1^#(X1,X2)	(135)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	84814
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	30106
[dbls(x₁)]	=	x₁ + 21195
[dbl(x₁)]	=	30104
[indx(x₁, x₂)]	=	x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	30106
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	1
[from(x₁)]	=	1
[s^#(x₁)]	=	0
[nil]	=	3
[dbl1(x₁)]	=	84812
[sel1^#(x₁, x₂)]	=	x₂ + 0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[quote(x₁)]	=	x₁ + 54706
[cons(x₁, x₂)]	=	3
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + 54709
[s1(x₁)]	=	84814

together with the usable rules

from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)

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

sel1^#(X1,mark(X2))	→	sel1^#(X1,X2)	(149)
sel1^#(X1,active(X2))	→	sel1^#(X1,X2)	(135)

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

dbl1^#(active(X))	→	dbl1^#(X)	(157)
dbl1^#(mark(X))	→	dbl1^#(X)	(79)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	x₁ + 0
[01]	=	36343
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	3
[dbls(x₁)]	=	x₁ + 592
[dbl(x₁)]	=	1
[indx(x₁, x₂)]	=	x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	31861
[from(x₁)]	=	1
[s^#(x₁)]	=	0
[nil]	=	29599
[dbl1(x₁)]	=	36341
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[quote(x₁)]	=	x₁ + 36338
[cons(x₁, x₂)]	=	3
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + 68201
[s1(x₁)]	=	36343

together with the usable rules

from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)

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

dbl1^#(active(X))	→	dbl1^#(X)	(157)
dbl1^#(mark(X))	→	dbl1^#(X)	(79)

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

sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(96)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(131)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(128)
sel^#(X1,active(X2))	→	sel^#(X1,X2)	(70)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	6951
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	3
[dbls(x₁)]	=	x₁ + 31103
[dbl(x₁)]	=	1
[indx(x₁, x₂)]	=	x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[sel^#(x₁, x₂)]	=	x₁ + 0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	16780
[from(x₁)]	=	1
[s^#(x₁)]	=	0
[nil]	=	29599
[dbl1(x₁)]	=	6949
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[quote(x₁)]	=	x₁ + 6946
[cons(x₁, x₂)]	=	3
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + 23728
[s1(x₁)]	=	6951

together with the usable rules

from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)

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

sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(96)
sel^#(active(X1),X2)	→	sel^#(X1,X2)	(128)

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

sel^#(X1,active(X2))	→	sel^#(X1,X2)	(70)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(131)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	40457
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	3
[dbls(x₁)]	=	x₁ + 13963
[dbl(x₁)]	=	1
[indx(x₁, x₂)]	=	x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[sel^#(x₁, x₂)]	=	x₂ + 0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	1
[from(x₁)]	=	7569
[s^#(x₁)]	=	0
[nil]	=	3
[dbl1(x₁)]	=	40455
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[quote(x₁)]	=	x₁ + 40452
[cons(x₁, x₂)]	=	17067
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + 40455
[s1(x₁)]	=	40457

together with the usable rules

from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)

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

sel^#(X1,active(X2))	→	sel^#(X1,X2)	(70)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(131)

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

indx^#(X1,mark(X2))	→	indx^#(X1,X2)	(115)
indx^#(X1,active(X2))	→	indx^#(X1,X2)	(155)
indx^#(active(X1),X2)	→	indx^#(X1,X2)	(151)
indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(125)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	13417
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	27128
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	1
[indx(x₁, x₂)]	=	x₂ + 283
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	3
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	x₁ + x₂ + 0
[sel(x₁, x₂)]	=	1
[from(x₁)]	=	15382
[s^#(x₁)]	=	0
[nil]	=	24218
[dbl1(x₁)]	=	13415
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[quote(x₁)]	=	x₁ + 13412
[cons(x₁, x₂)]	=	15384
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + 13415
[s1(x₁)]	=	40542

together with the usable rules

from(mark(X))	→	from(X)	(50)
from(active(X))	→	from(X)	(51)

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

indx^#(X1,mark(X2))	→	indx^#(X1,X2)	(115)
indx^#(X1,active(X2))	→	indx^#(X1,X2)	(155)
indx^#(active(X1),X2)	→	indx^#(X1,X2)	(151)
indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(125)

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

s1^#(active(X))	→	s1^#(X)	(103)
s1^#(mark(X))	→	s1^#(X)	(147)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	13417
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	31582
[dbl(x₁)]	=	x₁ + 3558
[indx(x₁, x₂)]	=	x₁ + x₂ + 16414
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 21766
[from(x₁)]	=	x₁ + 36140
[s^#(x₁)]	=	0
[nil]	=	41828
[dbl1(x₁)]	=	x₁ + 1
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 21770
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[quote(x₁)]	=	1
[cons(x₁, x₂)]	=	x₂ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	x₁ + 0
[sel1(x₁, x₂)]	=	x₁ + 1602
[s1(x₁)]	=	x₁ + 61135

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

s1^#(active(X))	→	s1^#(X)	(103)
s1^#(mark(X))	→	s1^#(X)	(147)

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

quote^#(active(X))	→	quote^#(X)	(161)
quote^#(mark(X))	→	quote^#(X)	(80)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	2289
[dbl(x₁)]	=	x₁ + 1
[indx(x₁, x₂)]	=	x₁ + x₂ + 2
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1682
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	1
[from(x₁)]	=	1
[s^#(x₁)]	=	0
[nil]	=	6609
[dbl1(x₁)]	=	x₁ + 1
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 44155
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[quote(x₁)]	=	x₁ + 32392
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	x₁ + 0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₂ + 44152
[s1(x₁)]	=	16713

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

quote^#(active(X))	→	quote^#(X)	(161)
quote^#(mark(X))	→	quote^#(X)	(80)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(109)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(101)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(143)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(140)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	12353
[dbl(x₁)]	=	x₁ + 1
[indx(x₁, x₂)]	=	x₁ + x₂ + 1356
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	1
[from(x₁)]	=	3374
[s^#(x₁)]	=	0
[nil]	=	49735
[dbl1(x₁)]	=	x₁ + 2247
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 24419
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[quote(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₂ + 24416
[s1(x₁)]	=	40178

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

cons^#(active(X1),X2)	→	cons^#(X1,X2)	(101)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(143)

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

cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(140)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(109)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	2
[dbl(x₁)]	=	x₁ + 1
[indx(x₁, x₂)]	=	x₁ + x₂ + 12447
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	16844
[from(x₁)]	=	2
[s^#(x₁)]	=	0
[nil]	=	1
[dbl1(x₁)]	=	x₁ + 22707
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 22709
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[quote(x₁)]	=	x₁ + 8930
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₂ + 22706
[s1(x₁)]	=	55011

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

cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(140)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(109)

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

dbls^#(mark(X))	→	dbls^#(X)	(153)
dbls^#(active(X))	→	dbls^#(X)	(94)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	5874
[dbl(x₁)]	=	x₁ + 998
[indx(x₁, x₂)]	=	x₁ + x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	x₁ + 0
[mark^#(x₁)]	=	0
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	5899
[from(x₁)]	=	7049
[s^#(x₁)]	=	0
[nil]	=	1
[dbl1(x₁)]	=	x₁ + 6319
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 38103
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[quote(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₂ + 38100
[s1(x₁)]	=	9334

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

dbls^#(mark(X))	→	dbls^#(X)	(153)
dbls^#(active(X))	→	dbls^#(X)	(94)

could be deleted.

1.1.11.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 12^th component contains the pair

dbl^#(active(X))	→	dbl^#(X)	(116)
dbl^#(mark(X))	→	dbl^#(X)	(83)

1.1.12 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	6705
[dbl(x₁)]	=	x₁ + 1
[indx(x₁, x₂)]	=	x₁ + x₂ + 1
[dbl^#(x₁)]	=	x₁ + 0
[dbls^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	1
[from(x₁)]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[dbl1(x₁)]	=	x₁ + 10889
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 46324
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[quote(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₂ + 46321
[s1(x₁)]	=	11468

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

dbl^#(active(X))	→	dbl^#(X)	(116)
dbl^#(mark(X))	→	dbl^#(X)	(83)

could be deleted.

1.1.12.1 Dependency Graph Processor

The dependency pairs are split into 0 components.