Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_7_Luc97_C)

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)
active(dbl(X))	→	dbl(active(X))	(18)
active(dbls(X))	→	dbls(active(X))	(19)
active(sel(X1,X2))	→	sel(active(X1),X2)	(20)
active(sel(X1,X2))	→	sel(X1,active(X2))	(21)
active(indx(X1,X2))	→	indx(active(X1),X2)	(22)
active(dbl1(X))	→	dbl1(active(X))	(23)
active(s1(X))	→	s1(active(X))	(24)
active(sel1(X1,X2))	→	sel1(active(X1),X2)	(25)
active(sel1(X1,X2))	→	sel1(X1,active(X2))	(26)
active(quote(X))	→	quote(active(X))	(27)
dbl(mark(X))	→	mark(dbl(X))	(28)
dbls(mark(X))	→	mark(dbls(X))	(29)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(30)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(31)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(32)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
s1(mark(X))	→	mark(s1(X))	(34)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
quote(mark(X))	→	mark(quote(X))	(37)
proper(dbl(X))	→	dbl(proper(X))	(38)
proper(0)	→	ok(0)	(39)
proper(s(X))	→	s(proper(X))	(40)
proper(dbls(X))	→	dbls(proper(X))	(41)
proper(nil)	→	ok(nil)	(42)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(43)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(44)
proper(indx(X1,X2))	→	indx(proper(X1),proper(X2))	(45)
proper(from(X))	→	from(proper(X))	(46)
proper(dbl1(X))	→	dbl1(proper(X))	(47)
proper(01)	→	ok(01)	(48)
proper(s1(X))	→	s1(proper(X))	(49)
proper(sel1(X1,X2))	→	sel1(proper(X1),proper(X2))	(50)
proper(quote(X))	→	quote(proper(X))	(51)
dbl(ok(X))	→	ok(dbl(X))	(52)
s(ok(X))	→	ok(s(X))	(53)
dbls(ok(X))	→	ok(dbls(X))	(54)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(55)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(56)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(57)
from(ok(X))	→	ok(from(X))	(58)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
s1(ok(X))	→	ok(s1(X))	(60)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
quote(ok(X))	→	ok(quote(X))	(62)
top(mark(X))	→	top(proper(X))	(63)
top(ok(X))	→	top(active(X))	(64)

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

1.1 Dependency Graph Processor

The dependency pairs are split into 14 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(150)
top^#(mark(X))	→	top^#(proper(X))	(80)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(top)	=	1
π(dbls^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(sel^#)	=	1
π(sel1^#)	=	1
π(active)	=	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^#)	=	[2, 1]	list-extension(cons^#)	=	Lex
prec(s)	=	1	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbls)	=	8	status(dbls)	=	[1]	list-extension(dbls)	=	Lex
prec(dbl)	=	8	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	7	status(indx)	=	[1]	list-extension(indx)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(top^#)	=	0	status(top^#)	=	[1]	list-extension(top^#)	=	Lex
prec(0)	=	3	status(0)	=	[]	list-extension(0)	=	Lex
prec(indx^#)	=	0	status(indx^#)	=	[]	list-extension(indx^#)	=	Lex
prec(sel)	=	5	status(sel)	=	[1, 2]	list-extension(sel)	=	Lex
prec(from)	=	8	status(from)	=	[1]	list-extension(from)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(nil)	=	7	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(dbl1)	=	4	status(dbl1)	=	[1]	list-extension(dbl1)	=	Lex
prec(mark)	=	2	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(quote)	=	6	status(quote)	=	[1]	list-extension(quote)	=	Lex
prec(cons)	=	7	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(active^#)	=	0	status(active^#)	=	[]	list-extension(active^#)	=	Lex
prec(quote^#)	=	0	status(quote^#)	=	[]	list-extension(quote^#)	=	Lex
prec(s1^#)	=	0	status(s1^#)	=	[]	list-extension(s1^#)	=	Lex
prec(sel1)	=	6	status(sel1)	=	[1, 2]	list-extension(sel1)	=	Lex
prec(s1)	=	3	status(s1)	=	[1]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

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

together with the usable rules

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

top^#(mark(X))

→

top^#(proper(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

top^#(ok(X))

→

top^#(active(X))

(150)

1.1.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₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + 20347
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	x₁ + 2
[ok(x₁)]	=	x₁ + 2
[0]	=	38312
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + 1
[from(x₁)]	=	x₁ + 20298
[s^#(x₁)]	=	0
[nil]	=	38027
[dbl1(x₁)]	=	x₁ + 1
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[quote(x₁)]	=	x₁ + 41745
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₂ + 10392
[s1(x₁)]	=	x₁ + 47830

together with the usable rules

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

top^#(ok(X))

→

top^#(active(X))

(150)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

active^#(indx(X1,X2))	→	active^#(X1)	(113)
active^#(sel(X1,X2))	→	active^#(X2)	(148)
active^#(dbls(X))	→	active^#(X)	(100)
active^#(sel1(X1,X2))	→	active^#(X1)	(93)
active^#(sel1(X1,X2))	→	active^#(X2)	(83)
active^#(sel(X1,X2))	→	active^#(X1)	(79)
active^#(quote(X))	→	active^#(X)	(129)
active^#(s1(X))	→	active^#(X)	(75)
active^#(dbl(X))	→	active^#(X)	(123)
active^#(dbl1(X))	→	active^#(X)	(121)

1.1.2 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₁)]	=	x₁ + 9335
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + 30478
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 19182
[s^#(x₁)]	=	0
[nil]	=	43183
[dbl1(x₁)]	=	x₁ + 1
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	11967
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 22498
[quote(x₁)]	=	x₁ + 1373
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	x₁ + 0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + x₂ + 1
[s1(x₁)]	=	x₁ + 1

together with the usable rules

active(dbl(X))	→	dbl(active(X))	(18)
proper(sel1(X1,X2))	→	sel1(proper(X1),proper(X2))	(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)
dbls(ok(X))	→	ok(dbls(X))	(54)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
active(sel(X1,X2))	→	sel(X1,active(X2))	(21)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
active(sel1(X1,X2))	→	sel1(X1,active(X2))	(26)
active(dbls(X))	→	dbls(active(X))	(19)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(32)
active(quote(sel(X,Y)))	→	mark(sel1(X,Y))	(17)
s1(ok(X))	→	ok(s1(X))	(60)
active(quote(X))	→	quote(active(X))	(27)
s1(mark(X))	→	mark(s1(X))	(34)
active(indx(X1,X2))	→	indx(active(X1),X2)	(22)
dbl(mark(X))	→	mark(dbl(X))	(28)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(44)
active(sel(0,cons(X,Y)))	→	mark(X)	(5)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
active(dbl1(0))	→	mark(01)	(10)
proper(0)	→	ok(0)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
active(sel(X1,X2))	→	sel(active(X1),X2)	(20)
active(sel1(X1,X2))	→	sel1(active(X1),X2)	(25)
proper(s1(X))	→	s1(proper(X))	(49)
dbl(ok(X))	→	ok(dbl(X))	(52)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(30)
quote(ok(X))	→	ok(quote(X))	(62)
active(quote(0))	→	mark(01)	(14)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(56)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(31)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
proper(indx(X1,X2))	→	indx(proper(X1),proper(X2))	(45)
active(dbl1(X))	→	dbl1(active(X))	(23)
active(s1(X))	→	s1(active(X))	(24)
indx(ok(X1),ok(X2))	→	ok(indx(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)
proper(quote(X))	→	quote(proper(X))	(51)
proper(s(X))	→	s(proper(X))	(40)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(55)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(6)
proper(dbl(X))	→	dbl(proper(X))	(38)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
from(ok(X))	→	ok(from(X))	(58)
proper(01)	→	ok(01)	(48)
s(ok(X))	→	ok(s(X))	(53)
proper(dbl1(X))	→	dbl1(proper(X))	(47)
quote(mark(X))	→	mark(quote(X))	(37)
proper(dbls(X))	→	dbls(proper(X))	(41)
proper(nil)	→	ok(nil)	(42)
proper(from(X))	→	from(proper(X))	(46)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)
dbls(mark(X))	→	mark(dbls(X))	(29)
proper(cons(X1,X2))	→	cons(proper(X1),proper(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^#(indx(X1,X2))	→	active^#(X1)	(113)
active^#(sel(X1,X2))	→	active^#(X2)	(148)
active^#(dbls(X))	→	active^#(X)	(100)
active^#(sel1(X1,X2))	→	active^#(X1)	(93)
active^#(sel1(X1,X2))	→	active^#(X2)	(83)
active^#(sel(X1,X2))	→	active^#(X1)	(79)
active^#(quote(X))	→	active^#(X)	(129)
active^#(s1(X))	→	active^#(X)	(75)
active^#(dbl(X))	→	active^#(X)	(123)
active^#(dbl1(X))	→	active^#(X)	(121)

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

proper^#(s(X))	→	proper^#(X)	(117)
proper^#(s1(X))	→	proper^#(X)	(116)
proper^#(dbl1(X))	→	proper^#(X)	(152)
proper^#(sel1(X1,X2))	→	proper^#(X1)	(110)
proper^#(dbls(X))	→	proper^#(X)	(106)
proper^#(sel1(X1,X2))	→	proper^#(X2)	(92)
proper^#(sel(X1,X2))	→	proper^#(X2)	(88)
proper^#(cons(X1,X2))	→	proper^#(X2)	(87)
proper^#(quote(X))	→	proper^#(X)	(135)
proper^#(sel(X1,X2))	→	proper^#(X1)	(84)
proper^#(cons(X1,X2))	→	proper^#(X1)	(127)
proper^#(indx(X1,X2))	→	proper^#(X1)	(74)
proper^#(indx(X1,X2))	→	proper^#(X2)	(73)
proper^#(from(X))	→	proper^#(X)	(122)
proper^#(dbl(X))	→	proper^#(X)	(118)

1.1.3 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₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 3137
[s^#(x₁)]	=	0
[nil]	=	1
[dbl1(x₁)]	=	x₁ + 1
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 26962
[proper^#(x₁)]	=	x₁ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 26964
[quote(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + x₂ + 1
[s1(x₁)]	=	x₁ + 1

together with the usable rules

active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
active(quote(sel(X,Y)))	→	mark(sel1(X,Y))	(17)
s1(ok(X))	→	ok(s1(X))	(60)
s1(mark(X))	→	mark(s1(X))	(34)
active(sel(0,cons(X,Y)))	→	mark(X)	(5)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
active(dbl1(0))	→	mark(01)	(10)
proper(0)	→	ok(0)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(30)
quote(ok(X))	→	ok(quote(X))	(62)
active(quote(0))	→	mark(01)	(14)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(56)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(31)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(57)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
active(sel1(s(X),cons(Y,Z)))	→	mark(sel1(X,Z))	(13)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(6)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
from(ok(X))	→	ok(from(X))	(58)
proper(01)	→	ok(01)	(48)
quote(mark(X))	→	mark(quote(X))	(37)
proper(nil)	→	ok(nil)	(42)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)

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

proper^#(s(X))	→	proper^#(X)	(117)
proper^#(s1(X))	→	proper^#(X)	(116)
proper^#(dbl1(X))	→	proper^#(X)	(152)
proper^#(sel1(X1,X2))	→	proper^#(X1)	(110)
proper^#(dbls(X))	→	proper^#(X)	(106)
proper^#(sel1(X1,X2))	→	proper^#(X2)	(92)
proper^#(sel(X1,X2))	→	proper^#(X2)	(88)
proper^#(cons(X1,X2))	→	proper^#(X2)	(87)
proper^#(quote(X))	→	proper^#(X)	(135)
proper^#(sel(X1,X2))	→	proper^#(X1)	(84)
proper^#(cons(X1,X2))	→	proper^#(X1)	(127)
proper^#(indx(X1,X2))	→	proper^#(X1)	(74)
proper^#(indx(X1,X2))	→	proper^#(X2)	(73)
proper^#(from(X))	→	proper^#(X)	(122)
proper^#(dbl(X))	→	proper^#(X)	(118)

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

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

→

cons^#(X1,X2)

(101)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
s1(ok(X))	→	ok(s1(X))	(60)
s1(mark(X))	→	mark(s1(X))	(34)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
active(dbl1(0))	→	mark(01)	(10)
proper(0)	→	ok(0)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
quote(ok(X))	→	ok(quote(X))	(62)
active(quote(0))	→	mark(01)	(14)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
proper(01)	→	ok(01)	(48)
quote(mark(X))	→	mark(quote(X))	(37)
proper(nil)	→	ok(nil)	(42)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)

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

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

→

cons^#(X1,X2)

(101)

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

from^#(ok(X))

→

from^#(X)

(137)

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

together with the usable rules

active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
s1(ok(X))	→	ok(s1(X))	(60)
s1(mark(X))	→	mark(s1(X))	(34)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
active(dbl1(0))	→	mark(01)	(10)
proper(0)	→	ok(0)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
quote(ok(X))	→	ok(quote(X))	(62)
active(quote(0))	→	mark(01)	(14)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
proper(01)	→	ok(01)	(48)
quote(mark(X))	→	mark(quote(X))	(37)
proper(nil)	→	ok(nil)	(42)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)

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

from^#(ok(X))

→

from^#(X)

(137)

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

dbls^#(ok(X))	→	dbls^#(X)	(108)
dbls^#(mark(X))	→	dbls^#(X)	(120)

1.1.6 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₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₂ + 0
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₂ + 0
[from(x₁)]	=	2
[s^#(x₁)]	=	0
[nil]	=	1
[dbl1(x₁)]	=	x₁ + 0
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 18562
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 21050
[quote(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 2489
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + x₂ + 768
[s1(x₁)]	=	x₁ + 1

together with the usable rules

active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
s1(ok(X))	→	ok(s1(X))	(60)
s1(mark(X))	→	mark(s1(X))	(34)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
active(dbl1(0))	→	mark(01)	(10)
proper(0)	→	ok(0)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
quote(ok(X))	→	ok(quote(X))	(62)
active(quote(0))	→	mark(01)	(14)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
proper(01)	→	ok(01)	(48)
quote(mark(X))	→	mark(quote(X))	(37)
proper(nil)	→	ok(nil)	(42)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)

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

dbls^#(ok(X))	→	dbls^#(X)	(108)
dbls^#(mark(X))	→	dbls^#(X)	(120)

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

dbl1^#(mark(X))	→	dbl1^#(X)	(109)
dbl1^#(ok(X))	→	dbl1^#(X)	(131)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
s1(ok(X))	→	ok(s1(X))	(60)
s1(mark(X))	→	mark(s1(X))	(34)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
active(dbl1(0))	→	mark(01)	(10)
proper(0)	→	ok(0)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
quote(ok(X))	→	ok(quote(X))	(62)
active(quote(0))	→	mark(01)	(14)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
proper(01)	→	ok(01)	(48)
quote(mark(X))	→	mark(quote(X))	(37)
proper(nil)	→	ok(nil)	(42)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)

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

dbl1^#(mark(X))	→	dbl1^#(X)	(109)
dbl1^#(ok(X))	→	dbl1^#(X)	(131)

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

dbl^#(mark(X))	→	dbl^#(X)	(136)
dbl^#(ok(X))	→	dbl^#(X)	(78)

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

together with the usable rules

active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
s1(ok(X))	→	ok(s1(X))	(60)
s1(mark(X))	→	mark(s1(X))	(34)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
active(dbl1(0))	→	mark(01)	(10)
proper(0)	→	ok(0)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
quote(ok(X))	→	ok(quote(X))	(62)
active(quote(0))	→	mark(01)	(14)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
proper(01)	→	ok(01)	(48)
quote(mark(X))	→	mark(quote(X))	(37)
proper(nil)	→	ok(nil)	(42)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)

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

dbl^#(mark(X))	→	dbl^#(X)	(136)
dbl^#(ok(X))	→	dbl^#(X)	(78)

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

s^#(ok(X))

→

s^#(X)

(146)

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₁ + 31771
[dbls(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₂ + 0
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₂ + 0
[from(x₁)]	=	1
[s^#(x₁)]	=	x₁ + 0
[nil]	=	1
[dbl1(x₁)]	=	x₁ + 0
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 31772
[quote(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 31772
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + x₂ + 1
[s1(x₁)]	=	x₁ + 1

together with the usable rules

active(quote(s(X)))	→	mark(s1(quote(X)))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(quote(dbl(X)))	→	mark(dbl1(X))	(16)
sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
s1(ok(X))	→	ok(s1(X))	(60)
s1(mark(X))	→	mark(s1(X))	(34)
dbl1(mark(X))	→	mark(dbl1(X))	(33)
active(dbl1(0))	→	mark(01)	(10)
proper(0)	→	ok(0)	(39)
active(indx(nil,X))	→	mark(nil)	(7)
quote(ok(X))	→	ok(quote(X))	(62)
active(quote(0))	→	mark(01)	(14)
active(sel1(0,cons(X,Y)))	→	mark(X)	(12)
active(dbl1(s(X)))	→	mark(s1(s1(dbl1(X))))	(11)
dbl1(ok(X))	→	ok(dbl1(X))	(59)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
proper(01)	→	ok(01)	(48)
quote(mark(X))	→	mark(quote(X))	(37)
proper(nil)	→	ok(nil)	(42)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)

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

s^#(ok(X))

→

s^#(X)

(146)

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

quote^#(ok(X))	→	quote^#(X)	(104)
quote^#(mark(X))	→	quote^#(X)	(94)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	37405
[dbls(x₁)]	=	2
[dbl(x₁)]	=	x₁ + 19369
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₂ + 32596
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 22166
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 16414
[from(x₁)]	=	x₁ + 50566
[s^#(x₁)]	=	0
[nil]	=	1
[dbl1(x₁)]	=	x₁ + 31582
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 5
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[quote(x₁)]	=	2
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	x₁ + 0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	x₁ + x₂ + 1602
[s1(x₁)]	=	2

together with the usable rules

sel1(X1,mark(X2))	→	mark(sel1(X1,X2))	(36)
dbl(mark(X))	→	mark(dbl(X))	(28)
dbl(ok(X))	→	ok(dbl(X))	(52)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(30)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(56)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(31)
sel1(ok(X1),ok(X2))	→	ok(sel1(X1,X2))	(61)
sel1(mark(X1),X2)	→	mark(sel1(X1,X2))	(35)

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

quote^#(ok(X))	→	quote^#(X)	(104)
quote^#(mark(X))	→	quote^#(X)	(94)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 11^th component contains the pair

indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(143)
indx^#(ok(X1),ok(X2))	→	indx^#(X1,X2)	(69)

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₁)]	=	1
[dbls(x₁)]	=	2
[dbl(x₁)]	=	x₁ + 36386
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	26007
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	x₁ + x₂ + 0
[sel(x₁, x₂)]	=	16415
[from(x₁)]	=	x₁ + 36986
[s^#(x₁)]	=	0
[nil]	=	2247
[dbl1(x₁)]	=	2
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 5
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[quote(x₁)]	=	2
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	12354
[s1(x₁)]	=	x₁ + 1

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

indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(143)
indx^#(ok(X1),ok(X2))	→	indx^#(X1,X2)	(69)

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

s1^#(mark(X))	→	s1^#(X)	(140)
s1^#(ok(X))	→	s1^#(X)	(71)

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₁)]	=	1
[dbls(x₁)]	=	4
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	4
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 8925
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	4
[from(x₁)]	=	x₁ + 32653
[s^#(x₁)]	=	0
[nil]	=	25321
[dbl1(x₁)]	=	4
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 5
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	3
[quote(x₁)]	=	4
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	x₁ + 0
[sel1(x₁, x₂)]	=	12356
[s1(x₁)]	=	x₁ + 1

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

s1^#(mark(X))	→	s1^#(X)	(140)
s1^#(ok(X))	→	s1^#(X)	(71)

could be deleted.

1.1.12.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 13^th component contains the pair

sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(128)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(72)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(67)

1.1.13 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	39255
[dbls(x₁)]	=	2
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	14731
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 24144
[ok(x₁)]	=	x₁ + 24145
[0]	=	10913
[sel^#(x₁, x₂)]	=	x₁ + 0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	9335
[from(x₁)]	=	x₁ + 11912
[s^#(x₁)]	=	0
[nil]	=	52396
[dbl1(x₁)]	=	5875
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 17234
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[quote(x₁)]	=	28880
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	2
[s1(x₁)]	=	x₁ + 27188

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

sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(128)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(72)

could be deleted.

1.1.13.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

sel^#(X1,mark(X2))

→

sel^#(X1,X2)

(67)

1.1.13.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₁)]	=	2
[dbl(x₁)]	=	x₁ + 1130
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	14731
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 2
[0]	=	18238
[sel^#(x₁, x₂)]	=	x₂ + 0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	7158
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	12332
[dbl1(x₁)]	=	16038
[sel1^#(x₁, x₂)]	=	0
[mark(x₁)]	=	x₁ + 17234
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[quote(x₁)]	=	27469
[cons(x₁, x₂)]	=	51094
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	17083
[s1(x₁)]	=	x₁ + 1

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

sel^#(X1,mark(X2))

→

sel^#(X1,X2)

(67)

could be deleted.

1.1.13.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 14^th component contains the pair

sel1^#(ok(X1),ok(X2))	→	sel1^#(X1,X2)	(156)
sel1^#(mark(X1),X2)	→	sel1^#(X1,X2)	(151)
sel1^#(X1,mark(X2))	→	sel1^#(X1,X2)	(82)

1.1.14 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₁)]	=	20438
[dbl(x₁)]	=	x₁ + 17534
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	28379
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 10310
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	52493
[from(x₁)]	=	x₁ + 39797
[s^#(x₁)]	=	0
[nil]	=	25029
[dbl1(x₁)]	=	20438
[sel1^#(x₁, x₂)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 37670
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	20437
[quote(x₁)]	=	47905
[cons(x₁, x₂)]	=	35066
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	37519
[s1(x₁)]	=	x₁ + 36536

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

sel1^#(ok(X1),ok(X2))	→	sel1^#(X1,X2)	(156)
sel1^#(mark(X1),X2)	→	sel1^#(X1,X2)	(151)

could be deleted.

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

(82)

1.1.14.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₁)]	=	2
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	7943
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 10310
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	32359
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[dbl1(x₁)]	=	2
[sel1^#(x₁, x₂)]	=	x₂ + 0
[mark(x₁)]	=	x₁ + 11794
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	1
[quote(x₁)]	=	27469
[cons(x₁, x₂)]	=	35066
[active^#(x₁)]	=	0
[quote^#(x₁)]	=	0
[s1^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	17083
[s1(x₁)]	=	x₁ + 20350

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

sel1^#(X1,mark(X2))

→

sel1^#(X1,X2)

(82)

could be deleted.

1.1.14.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.