Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_7_Luc97_FR)

The rewrite relation of the following TRS is considered.

dbl(0)	→	0	(1)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)
dbls(nil)	→	nil	(3)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
sel(0,cons(X,Y))	→	activate(X)	(5)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
indx(nil,X)	→	nil	(7)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
dbl1(0)	→	01	(10)
dbl1(s(X))	→	s1(s1(dbl1(activate(X))))	(11)
sel1(0,cons(X,Y))	→	activate(X)	(12)
sel1(s(X),cons(Y,Z))	→	sel1(activate(X),activate(Z))	(13)
quote(0)	→	01	(14)
quote(s(X))	→	s1(quote(activate(X)))	(15)
quote(dbl(X))	→	dbl1(X)	(16)
quote(sel(X,Y))	→	sel1(X,Y)	(17)
s(X)	→	n__s(X)	(18)
dbl(X)	→	n__dbl(X)	(19)
dbls(X)	→	n__dbls(X)	(20)
sel(X1,X2)	→	n__sel(X1,X2)	(21)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
from(X)	→	n__from(X)	(23)
activate(n__s(X))	→	s(X)	(24)
activate(n__dbl(X))	→	dbl(activate(X))	(25)
activate(n__dbls(X))	→	dbls(activate(X))	(26)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(27)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(28)
activate(n__from(X))	→	from(X)	(29)
activate(X)	→	X	(30)

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.

dbl^#(s(X))	→	activate^#(X)	(31)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(32)
dbls^#(cons(X,Y))	→	activate^#(Y)	(33)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(34)
dbl1^#(s(X))	→	activate^#(X)	(35)
sel1^#(s(X),cons(Y,Z))	→	activate^#(Z)	(36)
from^#(X)	→	activate^#(X)	(37)
quote^#(sel(X,Y))	→	sel1^#(X,Y)	(38)
activate^#(n__sel(X1,X2))	→	activate^#(X2)	(39)
dbl1^#(s(X))	→	dbl1^#(activate(X))	(40)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(32)
activate^#(n__s(X))	→	s^#(X)	(41)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(42)
activate^#(n__dbls(X))	→	dbls^#(activate(X))	(43)
activate^#(n__indx(X1,X2))	→	activate^#(X1)	(44)
sel1^#(s(X),cons(Y,Z))	→	sel1^#(activate(X),activate(Z))	(45)
from^#(X)	→	activate^#(X)	(37)
quote^#(s(X))	→	activate^#(X)	(46)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(47)
indx^#(cons(X,Y),Z)	→	activate^#(X)	(48)
activate^#(n__sel(X1,X2))	→	activate^#(X1)	(49)
dbls^#(cons(X,Y))	→	activate^#(X)	(50)
quote^#(dbl(X))	→	dbl1^#(X)	(51)
activate^#(n__dbl(X))	→	activate^#(X)	(52)
quote^#(s(X))	→	quote^#(activate(X))	(53)
activate^#(n__indx(X1,X2))	→	indx^#(activate(X1),X2)	(54)
activate^#(n__dbls(X))	→	activate^#(X)	(55)
activate^#(n__sel(X1,X2))	→	sel^#(activate(X1),activate(X2))	(56)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(57)
activate^#(n__from(X))	→	from^#(X)	(58)
dbl^#(s(X))	→	s^#(n__s(n__dbl(activate(X))))	(59)
sel1^#(s(X),cons(Y,Z))	→	activate^#(X)	(60)
sel1^#(0,cons(X,Y))	→	activate^#(X)	(61)
sel^#(s(X),cons(Y,Z))	→	sel^#(activate(X),activate(Z))	(62)
sel^#(0,cons(X,Y))	→	activate^#(X)	(63)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

quote^#(s(X))

→

quote^#(activate(X))

(53)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(dbl1^#)	=	1
π(activate)	=	1
π(dbls^#)	=	1
π(sel1)	=	2

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

prec(01)	=	0	status(01)	=	[]	list-extension(01)	=	Lex
prec(s)	=	2	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbls)	=	1	status(dbls)	=	[1]	list-extension(dbls)	=	Lex
prec(dbl)	=	3	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	1	status(indx)	=	[2]	list-extension(indx)	=	Lex
prec(n__indx)	=	1	status(n__indx)	=	[2]	list-extension(n__indx)	=	Lex
prec(n__from)	=	0	status(n__from)	=	[]	list-extension(n__from)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(activate^#)	=	0	status(activate^#)	=	[]	list-extension(activate^#)	=	Lex
prec(n__dbls)	=	1	status(n__dbls)	=	[1]	list-extension(n__dbls)	=	Lex
prec(n__s)	=	2	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(n__dbl)	=	3	status(n__dbl)	=	[1]	list-extension(n__dbl)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(indx^#)	=	0	status(indx^#)	=	[2, 1]	list-extension(indx^#)	=	Lex
prec(sel)	=	0	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(from)	=	0	status(from)	=	[]	list-extension(from)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(nil)	=	1	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(dbl1)	=	0	status(dbl1)	=	[]	list-extension(dbl1)	=	Lex
prec(sel1^#)	=	0	status(sel1^#)	=	[]	list-extension(sel1^#)	=	Lex
prec(n__sel)	=	0	status(n__sel)	=	[]	list-extension(n__sel)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(quote)	=	0	status(quote)	=	[]	list-extension(quote)	=	Lex
prec(cons)	=	0	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(quote^#)	=	0	status(quote^#)	=	[1]	list-extension(quote^#)	=	Lex
prec(s1)	=	0	status(s1)	=	[]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[indx(x₁, x₂)]	=	x₂ + 4
[n__indx(x₁, x₂)]	=	x₂ + 4
[n__from(x₁)]	=	x₁ + 284
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[n__dbls(x₁)]	=	x₁ + 0
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	1
[indx^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 284
[s^#(x₁)]	=	1
[nil]	=	4
[dbl1(x₁)]	=	1
[sel1^#(x₁, x₂)]	=	x₁ + 1
[n__sel(x₁, x₂)]	=	x₂ + 1
[from^#(x₁)]	=	1
[quote(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[quote^#(x₁)]	=	x₁ + 1
[s1(x₁)]	=	1

together with the usable rules

s(X)	→	n__s(X)	(18)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
dbl(0)	→	0	(1)
dbls(nil)	→	nil	(3)
sel(X1,X2)	→	n__sel(X1,X2)	(21)
activate(n__dbls(X))	→	dbls(activate(X))	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(28)
sel(0,cons(X,Y))	→	activate(X)	(5)
indx(nil,X)	→	nil	(7)
dbls(X)	→	n__dbls(X)	(20)
activate(n__dbl(X))	→	dbl(activate(X))	(25)
activate(X)	→	X	(30)
from(X)	→	n__from(X)	(23)
activate(n__s(X))	→	s(X)	(24)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
activate(n__from(X))	→	from(X)	(29)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)

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

quote^#(s(X))

→

quote^#(activate(X))

(53)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

dbl1^#(s(X))

→

dbl1^#(activate(X))

(40)

1.1.2 Reduction Pair Processor with Usable Rules

Using the argument filter

π(dbl1^#)	=	1
π(activate)	=	1
π(dbls^#)	=	1
π(sel1)	=	2

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

prec(01)	=	0	status(01)	=	[]	list-extension(01)	=	Lex
prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbls)	=	2	status(dbls)	=	[1]	list-extension(dbls)	=	Lex
prec(dbl)	=	4	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	3	status(indx)	=	[]	list-extension(indx)	=	Lex
prec(n__indx)	=	3	status(n__indx)	=	[]	list-extension(n__indx)	=	Lex
prec(n__from)	=	1	status(n__from)	=	[]	list-extension(n__from)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(activate^#)	=	0	status(activate^#)	=	[]	list-extension(activate^#)	=	Lex
prec(n__dbls)	=	2	status(n__dbls)	=	[1]	list-extension(n__dbls)	=	Lex
prec(n__s)	=	3	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(n__dbl)	=	4	status(n__dbl)	=	[1]	list-extension(n__dbl)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(indx^#)	=	0	status(indx^#)	=	[2, 1]	list-extension(indx^#)	=	Lex
prec(sel)	=	0	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(from)	=	1	status(from)	=	[]	list-extension(from)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(nil)	=	2	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(dbl1)	=	0	status(dbl1)	=	[]	list-extension(dbl1)	=	Lex
prec(sel1^#)	=	0	status(sel1^#)	=	[]	list-extension(sel1^#)	=	Lex
prec(n__sel)	=	0	status(n__sel)	=	[]	list-extension(n__sel)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(quote)	=	0	status(quote)	=	[]	list-extension(quote)	=	Lex
prec(cons)	=	0	status(cons)	=	[1]	list-extension(cons)	=	Lex
prec(quote^#)	=	0	status(quote^#)	=	[1]	list-extension(quote^#)	=	Lex
prec(s1)	=	0	status(s1)	=	[]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[indx(x₁, x₂)]	=	x₂ + 4
[n__indx(x₁, x₂)]	=	x₂ + 4
[n__from(x₁)]	=	x₁ + 3
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[n__dbls(x₁)]	=	x₁ + 0
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	1
[indx^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 3
[s^#(x₁)]	=	1
[nil]	=	3
[dbl1(x₁)]	=	1
[sel1^#(x₁, x₂)]	=	x₁ + 1
[n__sel(x₁, x₂)]	=	x₂ + 1
[from^#(x₁)]	=	1
[quote(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 2, x₂ + 0, 0)
[quote^#(x₁)]	=	x₁ + 1
[s1(x₁)]	=	1

together with the usable rules

s(X)	→	n__s(X)	(18)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
dbl(0)	→	0	(1)
dbls(nil)	→	nil	(3)
sel(X1,X2)	→	n__sel(X1,X2)	(21)
activate(n__dbls(X))	→	dbls(activate(X))	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(28)
sel(0,cons(X,Y))	→	activate(X)	(5)
indx(nil,X)	→	nil	(7)
dbls(X)	→	n__dbls(X)	(20)
activate(n__dbl(X))	→	dbl(activate(X))	(25)
activate(X)	→	X	(30)
from(X)	→	n__from(X)	(23)
activate(n__s(X))	→	s(X)	(24)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
activate(n__from(X))	→	from(X)	(29)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)

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

dbl1^#(s(X))

→

dbl1^#(activate(X))

(40)

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

sel1^#(s(X),cons(Y,Z))

→

sel1^#(activate(X),activate(Z))

(45)

1.1.3 Reduction Pair Processor with Usable Rules

Using the argument filter

π(activate)	=	1
π(dbls^#)	=	1
π(sel1^#)	=	1
π(sel1)	=	2

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)	=	0	status(01)	=	[]	list-extension(01)	=	Lex
prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbls)	=	2	status(dbls)	=	[]	list-extension(dbls)	=	Lex
prec(dbl)	=	4	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	2	status(indx)	=	[]	list-extension(indx)	=	Lex
prec(n__indx)	=	2	status(n__indx)	=	[]	list-extension(n__indx)	=	Lex
prec(n__from)	=	1	status(n__from)	=	[]	list-extension(n__from)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(activate^#)	=	0	status(activate^#)	=	[]	list-extension(activate^#)	=	Lex
prec(n__dbls)	=	2	status(n__dbls)	=	[]	list-extension(n__dbls)	=	Lex
prec(n__s)	=	3	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(n__dbl)	=	4	status(n__dbl)	=	[1]	list-extension(n__dbl)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(sel^#)	=	0	status(sel^#)	=	[]	list-extension(sel^#)	=	Lex
prec(indx^#)	=	0	status(indx^#)	=	[2, 1]	list-extension(indx^#)	=	Lex
prec(sel)	=	0	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(from)	=	1	status(from)	=	[]	list-extension(from)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(nil)	=	2	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(dbl1)	=	0	status(dbl1)	=	[]	list-extension(dbl1)	=	Lex
prec(n__sel)	=	0	status(n__sel)	=	[]	list-extension(n__sel)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(quote)	=	0	status(quote)	=	[]	list-extension(quote)	=	Lex
prec(cons)	=	0	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(quote^#)	=	0	status(quote^#)	=	[]	list-extension(quote^#)	=	Lex
prec(s1)	=	0	status(s1)	=	[]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[indx(x₁, x₂)]	=	x₂ + 31603
[n__indx(x₁, x₂)]	=	x₂ + 31603
[n__from(x₁)]	=	x₁ + 4
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[n__dbls(x₁)]	=	x₁ + 0
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	1
[indx^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 4
[s^#(x₁)]	=	1
[nil]	=	20585
[dbl1(x₁)]	=	1
[n__sel(x₁, x₂)]	=	x₂ + 1
[from^#(x₁)]	=	1
[quote(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 3, x₂ + 0, 0)
[quote^#(x₁)]	=	1
[s1(x₁)]	=	1

together with the usable rules

s(X)	→	n__s(X)	(18)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
dbl(0)	→	0	(1)
dbls(nil)	→	nil	(3)
sel(X1,X2)	→	n__sel(X1,X2)	(21)
activate(n__dbls(X))	→	dbls(activate(X))	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(28)
sel(0,cons(X,Y))	→	activate(X)	(5)
indx(nil,X)	→	nil	(7)
dbls(X)	→	n__dbls(X)	(20)
activate(n__dbl(X))	→	dbl(activate(X))	(25)
activate(X)	→	X	(30)
from(X)	→	n__from(X)	(23)
activate(n__s(X))	→	s(X)	(24)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
activate(n__from(X))	→	from(X)	(29)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)

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

sel1^#(s(X),cons(Y,Z))

→

sel1^#(activate(X),activate(Z))

(45)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

sel^#(0,cons(X,Y))	→	activate^#(X)	(63)
activate^#(n__dbls(X))	→	dbls^#(activate(X))	(43)
sel^#(s(X),cons(Y,Z))	→	sel^#(activate(X),activate(Z))	(62)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(42)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(32)
activate^#(n__sel(X1,X2))	→	activate^#(X2)	(39)
activate^#(n__from(X))	→	from^#(X)	(58)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(57)
activate^#(n__sel(X1,X2))	→	sel^#(activate(X1),activate(X2))	(56)
activate^#(n__dbls(X))	→	activate^#(X)	(55)
from^#(X)	→	activate^#(X)	(37)
activate^#(n__indx(X1,X2))	→	indx^#(activate(X1),X2)	(54)
activate^#(n__dbl(X))	→	activate^#(X)	(52)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(34)
dbls^#(cons(X,Y))	→	activate^#(X)	(50)
activate^#(n__sel(X1,X2))	→	activate^#(X1)	(49)
indx^#(cons(X,Y),Z)	→	activate^#(X)	(48)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(47)
from^#(X)	→	activate^#(X)	(37)
dbls^#(cons(X,Y))	→	activate^#(Y)	(33)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(32)
dbl^#(s(X))	→	activate^#(X)	(31)
activate^#(n__indx(X1,X2))	→	activate^#(X1)	(44)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 2
[activate(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 2
[indx(x₁, x₂)]	=	max(x₁ + 67291, x₂ + 67293, 0)
[n__indx(x₁, x₂)]	=	max(x₁ + 67291, x₂ + 67293, 0)
[n__from(x₁)]	=	x₁ + 31893
[dbl^#(x₁)]	=	x₁ + 10424
[activate^#(x₁)]	=	x₁ + 10423
[dbls^#(x₁)]	=	x₁ + 10424
[n__dbls(x₁)]	=	x₁ + 2
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	max(x₁ + 10425, x₂ + 10424, 0)
[indx^#(x₁, x₂)]	=	max(x₁ + 18458, x₂ + 77715, 0)
[sel(x₁, x₂)]	=	max(x₁ + 45634, x₂ + 20979, 0)
[from(x₁)]	=	x₁ + 31893
[s^#(x₁)]	=	0
[nil]	=	67294
[dbl1(x₁)]	=	0
[sel1^#(x₁, x₂)]	=	max(0)
[n__sel(x₁, x₂)]	=	max(x₁ + 45634, x₂ + 20979, 0)
[from^#(x₁)]	=	x₁ + 10424
[quote(x₁)]	=	0
[cons(x₁, x₂)]	=	max(x₁ + 21657, x₂ + 0, 0)
[quote^#(x₁)]	=	0
[sel1(x₁, x₂)]	=	max(0)
[s1(x₁)]	=	0

together with the usable rules

s(X)	→	n__s(X)	(18)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
dbl(0)	→	0	(1)
dbls(nil)	→	nil	(3)
sel(X1,X2)	→	n__sel(X1,X2)	(21)
activate(n__dbls(X))	→	dbls(activate(X))	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(28)
sel(0,cons(X,Y))	→	activate(X)	(5)
indx(nil,X)	→	nil	(7)
dbls(X)	→	n__dbls(X)	(20)
activate(n__dbl(X))	→	dbl(activate(X))	(25)
activate(X)	→	X	(30)
from(X)	→	n__from(X)	(23)
activate(n__s(X))	→	s(X)	(24)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
activate(n__from(X))	→	from(X)	(29)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)

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

sel^#(0,cons(X,Y))	→	activate^#(X)	(63)
activate^#(n__dbls(X))	→	dbls^#(activate(X))	(43)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(42)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(32)
activate^#(n__sel(X1,X2))	→	activate^#(X2)	(39)
activate^#(n__from(X))	→	from^#(X)	(58)
activate^#(n__dbl(X))	→	dbl^#(activate(X))	(57)
activate^#(n__sel(X1,X2))	→	sel^#(activate(X1),activate(X2))	(56)
activate^#(n__dbls(X))	→	activate^#(X)	(55)
from^#(X)	→	activate^#(X)	(37)
activate^#(n__indx(X1,X2))	→	indx^#(activate(X1),X2)	(54)
activate^#(n__dbl(X))	→	activate^#(X)	(52)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(34)
dbls^#(cons(X,Y))	→	activate^#(X)	(50)
activate^#(n__sel(X1,X2))	→	activate^#(X1)	(49)
indx^#(cons(X,Y),Z)	→	activate^#(X)	(48)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(47)
from^#(X)	→	activate^#(X)	(37)
dbls^#(cons(X,Y))	→	activate^#(Y)	(33)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(32)
dbl^#(s(X))	→	activate^#(X)	(31)
activate^#(n__indx(X1,X2))	→	activate^#(X1)	(44)

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

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

→

sel^#(activate(X),activate(Z))

(62)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(activate)	=	1
π(dbls^#)	=	1
π(sel^#)	=	1
π(sel1^#)	=	1
π(sel1)	=	2

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)	=	0	status(01)	=	[]	list-extension(01)	=	Lex
prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbls)	=	2	status(dbls)	=	[]	list-extension(dbls)	=	Lex
prec(dbl)	=	4	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	2	status(indx)	=	[]	list-extension(indx)	=	Lex
prec(n__indx)	=	2	status(n__indx)	=	[]	list-extension(n__indx)	=	Lex
prec(n__from)	=	1	status(n__from)	=	[]	list-extension(n__from)	=	Lex
prec(dbl^#)	=	0	status(dbl^#)	=	[]	list-extension(dbl^#)	=	Lex
prec(activate^#)	=	0	status(activate^#)	=	[]	list-extension(activate^#)	=	Lex
prec(n__dbls)	=	2	status(n__dbls)	=	[]	list-extension(n__dbls)	=	Lex
prec(n__s)	=	3	status(n__s)	=	[1]	list-extension(n__s)	=	Lex
prec(n__dbl)	=	4	status(n__dbl)	=	[1]	list-extension(n__dbl)	=	Lex
prec(0)	=	1	status(0)	=	[]	list-extension(0)	=	Lex
prec(indx^#)	=	0	status(indx^#)	=	[2, 1]	list-extension(indx^#)	=	Lex
prec(sel)	=	0	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(from)	=	1	status(from)	=	[]	list-extension(from)	=	Lex
prec(s^#)	=	0	status(s^#)	=	[]	list-extension(s^#)	=	Lex
prec(nil)	=	2	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(dbl1)	=	0	status(dbl1)	=	[]	list-extension(dbl1)	=	Lex
prec(n__sel)	=	0	status(n__sel)	=	[]	list-extension(n__sel)	=	Lex
prec(from^#)	=	0	status(from^#)	=	[]	list-extension(from^#)	=	Lex
prec(quote)	=	0	status(quote)	=	[]	list-extension(quote)	=	Lex
prec(cons)	=	0	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(quote^#)	=	0	status(quote^#)	=	[]	list-extension(quote^#)	=	Lex
prec(s1)	=	0	status(s1)	=	[]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

[dbl1^#(x₁)]	=	0
[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[indx(x₁, x₂)]	=	x₂ + 31603
[n__indx(x₁, x₂)]	=	x₂ + 31603
[n__from(x₁)]	=	x₁ + 491
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[n__dbls(x₁)]	=	x₁ + 0
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 0
[0]	=	1
[indx^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 491
[s^#(x₁)]	=	1
[nil]	=	7579
[dbl1(x₁)]	=	1
[n__sel(x₁, x₂)]	=	x₂ + 1
[from^#(x₁)]	=	1
[quote(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 490, x₂ + 0, 0)
[quote^#(x₁)]	=	1
[s1(x₁)]	=	1

together with the usable rules

s(X)	→	n__s(X)	(18)
dbls(cons(X,Y))	→	cons(n__dbl(activate(X)),n__dbls(activate(Y)))	(4)
indx(cons(X,Y),Z)	→	cons(n__sel(activate(X),activate(Z)),n__indx(activate(Y),activate(Z)))	(8)
dbl(0)	→	0	(1)
dbls(nil)	→	nil	(3)
sel(X1,X2)	→	n__sel(X1,X2)	(21)
activate(n__dbls(X))	→	dbls(activate(X))	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(activate(X1),activate(X2))	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(activate(X1),X2)	(28)
sel(0,cons(X,Y))	→	activate(X)	(5)
indx(nil,X)	→	nil	(7)
dbls(X)	→	n__dbls(X)	(20)
activate(n__dbl(X))	→	dbl(activate(X))	(25)
activate(X)	→	X	(30)
from(X)	→	n__from(X)	(23)
activate(n__s(X))	→	s(X)	(24)
from(X)	→	cons(activate(X),n__from(n__s(activate(X))))	(9)
sel(s(X),cons(Y,Z))	→	sel(activate(X),activate(Z))	(6)
activate(n__from(X))	→	from(X)	(29)
dbl(s(X))	→	s(n__s(n__dbl(activate(X))))	(2)

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

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

→

sel^#(activate(X),activate(Z))

(62)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.