Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex5_7_Luc97_Z)

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(X)	(25)
activate(n__dbls(X))	→	dbls(X)	(26)
activate(n__sel(X1,X2))	→	sel(X1,X2)	(27)
activate(n__indx(X1,X2))	→	indx(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)
dbls^#(cons(X,Y))	→	activate^#(X)	(32)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(33)
dbl1^#(s(X))	→	activate^#(X)	(34)
sel1^#(s(X),cons(Y,Z))	→	activate^#(Z)	(35)
from^#(X)	→	activate^#(X)	(36)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(37)
indx^#(cons(X,Y),Z)	→	activate^#(X)	(38)
dbl1^#(s(X))	→	dbl1^#(activate(X))	(39)
activate^#(n__s(X))	→	s^#(X)	(40)
dbls^#(cons(X,Y))	→	activate^#(Y)	(41)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(42)
quote^#(sel(X,Y))	→	sel1^#(X,Y)	(43)
sel1^#(s(X),cons(Y,Z))	→	sel1^#(activate(X),activate(Z))	(44)
from^#(X)	→	activate^#(X)	(36)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(45)
quote^#(s(X))	→	activate^#(X)	(46)
quote^#(dbl(X))	→	dbl1^#(X)	(47)
quote^#(s(X))	→	quote^#(activate(X))	(48)
sel^#(0,cons(X,Y))	→	activate^#(X)	(49)
activate^#(n__sel(X1,X2))	→	sel^#(X1,X2)	(50)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(37)
activate^#(n__dbls(X))	→	dbls^#(X)	(51)
activate^#(n__dbl(X))	→	dbl^#(X)	(52)
activate^#(n__from(X))	→	from^#(X)	(53)
dbl^#(s(X))	→	s^#(n__s(n__dbl(activate(X))))	(54)
sel1^#(s(X),cons(Y,Z))	→	activate^#(X)	(55)
sel1^#(0,cons(X,Y))	→	activate^#(X)	(56)
sel^#(s(X),cons(Y,Z))	→	sel^#(activate(X),activate(Z))	(57)
activate^#(n__indx(X1,X2))	→	indx^#(X1,X2)	(58)

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

(48)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(dbls^#)	=	1
π(indx^#)	=	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)	=	0	status(01)	=	[]	list-extension(01)	=	Lex
prec(s)	=	3	status(s)	=	[1]	list-extension(s)	=	Lex
prec(dbls)	=	0	status(dbls)	=	[1]	list-extension(dbls)	=	Lex
prec(activate)	=	2	status(activate)	=	[1]	list-extension(activate)	=	Lex
prec(dbl)	=	4	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	2	status(indx)	=	[1]	list-extension(indx)	=	Lex
prec(n__indx)	=	1	status(n__indx)	=	[1, 2]	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)	=	0	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^#)	=	[1, 2]	list-extension(sel^#)	=	Lex
prec(sel)	=	4	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(from)	=	2	status(from)	=	[1]	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)	=	4	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(sel1)	=	0	status(sel1)	=	[2, 1]	list-extension(sel1)	=	Lex
prec(s1)	=	0	status(s1)	=	[]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

[dbl1^#(x₁)]	=	1
[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 1
[activate(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 1
[indx(x₁, x₂)]	=	x₁ + x₂ + 4
[n__indx(x₁, x₂)]	=	x₁ + x₂ + 4
[n__from(x₁)]	=	x₁ + 17890
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[n__dbls(x₁)]	=	x₁ + 1
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 17890
[s^#(x₁)]	=	1
[nil]	=	35102
[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
[sel1(x₁, x₂)]	=	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(X)	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(X1,X2)	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(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(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))

(48)

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

(39)

1.1.2 Reduction Pair Processor with Usable Rules

Using the argument filter

π(dbls^#)	=	1
π(indx^#)	=	1

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

prec(dbl1^#)	=	0	status(dbl1^#)	=	[1]	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)	=	0	status(dbls)	=	[]	list-extension(dbls)	=	Lex
prec(activate)	=	2	status(activate)	=	[1]	list-extension(activate)	=	Lex
prec(dbl)	=	4	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	2	status(indx)	=	[2]	list-extension(indx)	=	Lex
prec(n__indx)	=	1	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)	=	0	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^#)	=	[1, 2]	list-extension(sel^#)	=	Lex
prec(sel)	=	4	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(from)	=	2	status(from)	=	[1]	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)	=	4	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(sel1)	=	0	status(sel1)	=	[2, 1]	list-extension(sel1)	=	Lex
prec(s1)	=	0	status(s1)	=	[]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

[dbl1^#(x₁)]	=	x₁ + 1
[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 27858
[activate(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 27857
[indx(x₁, x₂)]	=	x₂ + 27861
[n__indx(x₁, x₂)]	=	x₂ + 27861
[n__from(x₁)]	=	x₁ + 27860
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[n__dbls(x₁)]	=	x₁ + 27858
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 27857
[0]	=	1
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 27860
[s^#(x₁)]	=	1
[nil]	=	5599
[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₁ + 27859, x₂ + 0, 0)
[quote^#(x₁)]	=	x₁ + 1
[sel1(x₁, x₂)]	=	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(X)	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(X1,X2)	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(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(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))

(39)

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

(44)

1.1.3 Reduction Pair Processor with Usable Rules

Using the argument filter

π(dbls^#)	=	1
π(indx^#)	=	1

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

prec(dbl1^#)	=	0	status(dbl1^#)	=	[1]	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)	=	1	status(dbls)	=	[]	list-extension(dbls)	=	Lex
prec(activate)	=	2	status(activate)	=	[1]	list-extension(activate)	=	Lex
prec(dbl)	=	4	status(dbl)	=	[1]	list-extension(dbl)	=	Lex
prec(indx)	=	2	status(indx)	=	[2]	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)	=	1	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^#)	=	[1, 2]	list-extension(sel^#)	=	Lex
prec(sel)	=	4	status(sel)	=	[]	list-extension(sel)	=	Lex
prec(from)	=	2	status(from)	=	[1]	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^#)	=	[1]	list-extension(sel1^#)	=	Lex
prec(n__sel)	=	4	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)	=	1	status(cons)	=	[]	list-extension(cons)	=	Lex
prec(quote^#)	=	0	status(quote^#)	=	[1]	list-extension(quote^#)	=	Lex
prec(sel1)	=	0	status(sel1)	=	[2, 1]	list-extension(sel1)	=	Lex
prec(s1)	=	0	status(s1)	=	[]	list-extension(s1)	=	Lex

and the following Max-polynomial interpretation

[dbl1^#(x₁)]	=	x₁ + 1
[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 13215
[activate(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 13214
[indx(x₁, x₂)]	=	x₂ + 13218
[n__indx(x₁, x₂)]	=	x₂ + 13218
[n__from(x₁)]	=	x₁ + 13217
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[n__dbls(x₁)]	=	x₁ + 13215
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 13214
[0]	=	1
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 13217
[s^#(x₁)]	=	1
[nil]	=	1
[dbl1(x₁)]	=	1
[sel1^#(x₁, x₂)]	=	x₁ + 0
[n__sel(x₁, x₂)]	=	x₂ + 1
[from^#(x₁)]	=	1
[quote(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 13216, x₂ + 0, 0)
[quote^#(x₁)]	=	x₁ + 1
[sel1(x₁, x₂)]	=	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(X)	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(X1,X2)	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(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(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))

(44)

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

activate^#(n__indx(X1,X2))	→	indx^#(X1,X2)	(58)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(42)
sel^#(s(X),cons(Y,Z))	→	sel^#(activate(X),activate(Z))	(57)
dbls^#(cons(X,Y))	→	activate^#(Y)	(41)
indx^#(cons(X,Y),Z)	→	activate^#(X)	(38)
activate^#(n__from(X))	→	from^#(X)	(53)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(37)
activate^#(n__dbl(X))	→	dbl^#(X)	(52)
activate^#(n__dbls(X))	→	dbls^#(X)	(51)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(37)
from^#(X)	→	activate^#(X)	(36)
activate^#(n__sel(X1,X2))	→	sel^#(X1,X2)	(50)
sel^#(0,cons(X,Y))	→	activate^#(X)	(49)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(33)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(45)
from^#(X)	→	activate^#(X)	(36)
dbls^#(cons(X,Y))	→	activate^#(X)	(32)
dbl^#(s(X))	→	activate^#(X)	(31)

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₁ + 14682
[activate(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 14682
[indx(x₁, x₂)]	=	max(x₁ + 61181, x₂ + 34894, 0)
[n__indx(x₁, x₂)]	=	max(x₁ + 61181, x₂ + 34894, 0)
[n__from(x₁)]	=	x₁ + 21657
[dbl^#(x₁)]	=	x₁ + 15348
[activate^#(x₁)]	=	x₁ + 667
[dbls^#(x₁)]	=	x₁ + 668
[n__dbls(x₁)]	=	x₁ + 14682
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 14682
[0]	=	1
[sel^#(x₁, x₂)]	=	max(x₁ + 670, x₂ + 668, 0)
[indx^#(x₁, x₂)]	=	max(x₁ + 61847, x₂ + 1991, 0)
[sel(x₁, x₂)]	=	max(x₁ + 31895, x₂ + 31896, 0)
[from(x₁)]	=	x₁ + 21657
[s^#(x₁)]	=	0
[nil]	=	34895
[dbl1(x₁)]	=	0
[sel1^#(x₁, x₂)]	=	max(0)
[n__sel(x₁, x₂)]	=	max(x₁ + 31895, x₂ + 31896, 0)
[from^#(x₁)]	=	x₁ + 668
[quote(x₁)]	=	0
[cons(x₁, x₂)]	=	max(x₁ + 1, 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(X)	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(X1,X2)	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(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(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

activate^#(n__indx(X1,X2))	→	indx^#(X1,X2)	(58)
indx^#(cons(X,Y),Z)	→	activate^#(Y)	(42)
dbls^#(cons(X,Y))	→	activate^#(Y)	(41)
indx^#(cons(X,Y),Z)	→	activate^#(X)	(38)
activate^#(n__from(X))	→	from^#(X)	(53)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(37)
activate^#(n__dbl(X))	→	dbl^#(X)	(52)
activate^#(n__dbls(X))	→	dbls^#(X)	(51)
indx^#(cons(X,Y),Z)	→	activate^#(Z)	(37)
from^#(X)	→	activate^#(X)	(36)
activate^#(n__sel(X1,X2))	→	sel^#(X1,X2)	(50)
sel^#(0,cons(X,Y))	→	activate^#(X)	(49)
sel^#(s(X),cons(Y,Z))	→	activate^#(Z)	(33)
sel^#(s(X),cons(Y,Z))	→	activate^#(X)	(45)
from^#(X)	→	activate^#(X)	(36)
dbls^#(cons(X,Y))	→	activate^#(X)	(32)
dbl^#(s(X))	→	activate^#(X)	(31)

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

(57)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

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

and the following Max-polynomial interpretation

[dbl1^#(x₁)]	=	1
[01]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 7069
[activate(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 7067
[indx(x₁, x₂)]	=	x₁ + x₂ + 12833
[n__indx(x₁, x₂)]	=	x₁ + x₂ + 12833
[n__from(x₁)]	=	x₁ + 7069
[dbl^#(x₁)]	=	1
[activate^#(x₁)]	=	1
[n__dbls(x₁)]	=	x₁ + 7069
[n__s(x₁)]	=	x₁ + 0
[n__dbl(x₁)]	=	x₁ + 7067
[0]	=	1
[sel^#(x₁, x₂)]	=	x₁ + 1
[sel(x₁, x₂)]	=	x₂ + 5764
[from(x₁)]	=	x₁ + 7069
[s^#(x₁)]	=	1
[nil]	=	51737
[dbl1(x₁)]	=	1
[sel1^#(x₁, x₂)]	=	0
[n__sel(x₁, x₂)]	=	x₂ + 5764
[from^#(x₁)]	=	1
[quote(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 7068, x₂ + 0, 0)
[quote^#(x₁)]	=	1
[sel1(x₁, x₂)]	=	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(X)	(26)
dbl(X)	→	n__dbl(X)	(19)
activate(n__sel(X1,X2))	→	sel(X1,X2)	(27)
indx(X1,X2)	→	n__indx(X1,X2)	(22)
activate(n__indx(X1,X2))	→	indx(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(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))

(57)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.