Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex3_2_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(dbl(X))	→	dbl(active(X))	(10)
active(dbls(X))	→	dbls(active(X))	(11)
active(sel(X1,X2))	→	sel(active(X1),X2)	(12)
active(sel(X1,X2))	→	sel(X1,active(X2))	(13)
active(indx(X1,X2))	→	indx(active(X1),X2)	(14)
dbl(mark(X))	→	mark(dbl(X))	(15)
dbls(mark(X))	→	mark(dbls(X))	(16)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
proper(dbl(X))	→	dbl(proper(X))	(20)
proper(0)	→	ok(0)	(21)
proper(s(X))	→	s(proper(X))	(22)
proper(dbls(X))	→	dbls(proper(X))	(23)
proper(nil)	→	ok(nil)	(24)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(25)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
proper(indx(X1,X2))	→	indx(proper(X1),proper(X2))	(27)
proper(from(X))	→	from(proper(X))	(28)
dbl(ok(X))	→	ok(dbl(X))	(29)
s(ok(X))	→	ok(s(X))	(30)
dbls(ok(X))	→	ok(dbls(X))	(31)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
from(ok(X))	→	ok(from(X))	(35)
top(mark(X))	→	top(proper(X))	(36)
top(ok(X))	→	top(active(X))	(37)

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

1.1 Dependency Graph Processor

The dependency pairs are split into 10 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(50)
top^#(mark(X))	→	top^#(proper(X))	(42)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(cons^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(sel^#)	=	2
π(from^#)	=	1
π(active)	=	1
π(active^#)	=	1

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

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

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 31113
[dbl(x₁)]	=	x₁ + 31112
[top(x₁)]	=	1
[indx(x₁, x₂)]	=	x₁ + x₂ + 62230
[dbl^#(x₁)]	=	1
[dbls^#(x₁)]	=	1
[top^#(x₁)]	=	x₁ + 1
[0]	=	1
[indx^#(x₁, x₂)]	=	x₁ + x₂ + 1
[sel(x₁, x₂)]	=	x₁ + x₂ + 31115
[from(x₁)]	=	x₁ + 51699
[s^#(x₁)]	=	1
[nil]	=	19791
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 31114, x₂ + 0, 0)

together with the usable rules

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

(42)

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

(50)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[dbls(x₁)]	=	x₁ + 0
[dbl(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + 0
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	16337
[ok(x₁)]	=	x₁ + 2
[0]	=	16335
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + 0
[from(x₁)]	=	x₁ + 0
[s^#(x₁)]	=	0
[nil]	=	5969
[mark(x₁)]	=	0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₂ + 0
[active^#(x₁)]	=	0

together with the usable rules

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

(50)

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^#(dbl(X))	→	active^#(X)	(64)
active^#(dbls(X))	→	active^#(X)	(90)
active^#(sel(X1,X2))	→	active^#(X1)	(81)
active^#(indx(X1,X2))	→	active^#(X1)	(76)
active^#(sel(X1,X2))	→	active^#(X2)	(71)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 22857
[s^#(x₁)]	=	0
[nil]	=	425
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	16335
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
dbl(mark(X))	→	mark(dbl(X))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
dbls(mark(X))	→	mark(dbls(X))	(16)
proper(0)	→	ok(0)	(21)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(indx(nil,X))	→	mark(nil)	(7)
dbls(ok(X))	→	ok(dbls(X))	(31)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)
dbl(ok(X))	→	ok(dbl(X))	(29)

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

active^#(dbl(X))	→	active^#(X)	(64)
active^#(dbls(X))	→	active^#(X)	(90)
active^#(sel(X1,X2))	→	active^#(X1)	(81)
active^#(indx(X1,X2))	→	active^#(X1)	(76)
active^#(sel(X1,X2))	→	active^#(X2)	(71)

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^#(cons(X1,X2))	→	proper^#(X1)	(67)
proper^#(sel(X1,X2))	→	proper^#(X2)	(59)
proper^#(cons(X1,X2))	→	proper^#(X2)	(82)
proper^#(dbls(X))	→	proper^#(X)	(79)
proper^#(indx(X1,X2))	→	proper^#(X1)	(49)
proper^#(dbl(X))	→	proper^#(X)	(75)
proper^#(sel(X1,X2))	→	proper^#(X1)	(74)
proper^#(from(X))	→	proper^#(X)	(72)
proper^#(indx(X1,X2))	→	proper^#(X2)	(70)
proper^#(s(X))	→	proper^#(X)	(41)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 8822
[ok(x₁)]	=	x₁ + 1911
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	x₁ + 0
[from^#(x₁)]	=	0
[active(x₁)]	=	16335
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
dbl(mark(X))	→	mark(dbl(X))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
dbls(mark(X))	→	mark(dbls(X))	(16)
proper(0)	→	ok(0)	(21)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(indx(nil,X))	→	mark(nil)	(7)
dbls(ok(X))	→	ok(dbls(X))	(31)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)
dbl(ok(X))	→	ok(dbl(X))	(29)

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

proper^#(cons(X1,X2))	→	proper^#(X1)	(67)
proper^#(sel(X1,X2))	→	proper^#(X2)	(59)
proper^#(cons(X1,X2))	→	proper^#(X2)	(82)
proper^#(dbls(X))	→	proper^#(X)	(79)
proper^#(indx(X1,X2))	→	proper^#(X1)	(49)
proper^#(dbl(X))	→	proper^#(X)	(75)
proper^#(sel(X1,X2))	→	proper^#(X1)	(74)
proper^#(from(X))	→	proper^#(X)	(72)
proper^#(indx(X1,X2))	→	proper^#(X2)	(70)
proper^#(s(X))	→	proper^#(X)	(41)

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)

(44)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 2056
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 7556
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	16335
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
dbl(mark(X))	→	mark(dbl(X))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
dbls(mark(X))	→	mark(dbls(X))	(16)
proper(0)	→	ok(0)	(21)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(indx(nil,X))	→	mark(nil)	(7)
dbls(ok(X))	→	ok(dbls(X))	(31)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)
dbl(ok(X))	→	ok(dbl(X))	(29)

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

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

→

cons^#(X1,X2)

(44)

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)

(73)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + x₂ + 2561
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 10620
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	16335
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
dbl(mark(X))	→	mark(dbl(X))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
dbls(mark(X))	→	mark(dbls(X))	(16)
proper(0)	→	ok(0)	(21)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(indx(nil,X))	→	mark(nil)	(7)
dbls(ok(X))	→	ok(dbls(X))	(31)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)
dbl(ok(X))	→	ok(dbl(X))	(29)

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

from^#(ok(X))

→

from^#(X)

(73)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

indx^#(ok(X1),ok(X2))	→	indx^#(X1,X2)	(83)
indx^#(mark(X1),X2)	→	indx^#(X1,X2)	(43)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	x₁ + 1
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + x₂ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	x₁ + 1
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + x₂ + 1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	3
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	3
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
dbl(mark(X))	→	mark(dbl(X))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
dbls(mark(X))	→	mark(dbls(X))	(16)
proper(0)	→	ok(0)	(21)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(indx(nil,X))	→	mark(nil)	(7)
dbls(ok(X))	→	ok(dbls(X))	(31)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)
dbl(ok(X))	→	ok(dbl(X))	(29)

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

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

→

indx^#(X1,X2)

(83)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

indx^#(mark(X1),X2)

→

indx^#(X1,X2)

(43)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
dbl(mark(X))	→	mark(dbl(X))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
dbls(mark(X))	→	mark(dbls(X))	(16)
proper(0)	→	ok(0)	(21)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(indx(nil,X))	→	mark(nil)	(7)
dbls(ok(X))	→	ok(dbls(X))	(31)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)
dbl(ok(X))	→	ok(dbl(X))	(29)

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

indx^#(mark(X1),X2)

→

indx^#(X1,X2)

(43)

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

dbl^#(mark(X))	→	dbl^#(X)	(65)
dbl^#(ok(X))	→	dbl^#(X)	(91)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
dbl(mark(X))	→	mark(dbl(X))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
dbls(mark(X))	→	mark(dbls(X))	(16)
proper(0)	→	ok(0)	(21)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(indx(nil,X))	→	mark(nil)	(7)
dbls(ok(X))	→	ok(dbls(X))	(31)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)
dbl(ok(X))	→	ok(dbl(X))	(29)

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

dbl^#(mark(X))	→	dbl^#(X)	(65)
dbl^#(ok(X))	→	dbl^#(X)	(91)

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

sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(62)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(61)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(52)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(X1,mark(X2))	→	mark(sel(X1,X2))	(18)
dbl(mark(X))	→	mark(dbl(X))	(15)
active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
dbls(mark(X))	→	mark(dbls(X))	(16)
proper(0)	→	ok(0)	(21)
indx(mark(X1),X2)	→	mark(indx(X1,X2))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(17)
indx(ok(X1),ok(X2))	→	ok(indx(X1,X2))	(34)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(33)
active(indx(nil,X))	→	mark(nil)	(7)
dbls(ok(X))	→	ok(dbls(X))	(31)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)
dbl(ok(X))	→	ok(dbl(X))	(29)

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

sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(61)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(52)

could be deleted.

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

(62)

1.1.8.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	20056
[dbls(x₁)]	=	26956
[dbl(x₁)]	=	59710
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	33991
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 0
[0]	=	1
[sel^#(x₁, x₂)]	=	x₂ + 0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₂ + 1
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	26955
[cons(x₁, x₂)]	=	26954
[active^#(x₁)]	=	0

together with the usable rules

active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
proper(0)	→	ok(0)	(21)
active(indx(nil,X))	→	mark(nil)	(7)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)

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

sel^#(X1,mark(X2))

→

sel^#(X1,X2)

(62)

could be deleted.

1.1.8.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

s^#(ok(X))

→

s^#(X)

(58)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	20057
[dbls(x₁)]	=	24197
[dbl(x₁)]	=	24197
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	24197
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	26480
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	24196
[from(x₁)]	=	x₁ + 2089
[s^#(x₁)]	=	x₁ + 0
[nil]	=	1
[mark(x₁)]	=	24196
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	24196
[cons(x₁, x₂)]	=	x₂ + 31797
[active^#(x₁)]	=	0

together with the usable rules

active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(indx(nil,X))	→	mark(nil)	(7)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)

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

s^#(ok(X))

→

s^#(X)

(58)

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

dbls^#(mark(X))	→	dbls^#(X)	(48)
dbls^#(ok(X))	→	dbls^#(X)	(68)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	22613
[dbls(x₁)]	=	55753
[dbl(x₁)]	=	55753
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + 1
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[proper(x₁)]	=	22612
[ok(x₁)]	=	x₁ + 1
[0]	=	22612
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	22613
[from(x₁)]	=	x₁ + 25337
[s^#(x₁)]	=	0
[nil]	=	22611
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	55752
[cons(x₁, x₂)]	=	x₂ + 7802
[active^#(x₁)]	=	0

together with the usable rules

active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(indx(nil,X))	→	mark(nil)	(7)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)

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

dbls^#(ok(X))

→

dbls^#(X)

(68)

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

dbls^#(mark(X))

→

dbls^#(X)

(48)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[dbls(x₁)]	=	41144
[dbl(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[indx(x₁, x₂)]	=	x₁ + 12340
[dbl^#(x₁)]	=	0
[dbls^#(x₁)]	=	x₁ + 0
[top^#(x₁)]	=	0
[proper(x₁)]	=	39292
[ok(x₁)]	=	x₁ + 25150
[0]	=	14143
[sel^#(x₁, x₂)]	=	0
[indx^#(x₁, x₂)]	=	0
[sel(x₁, x₂)]	=	x₁ + x₂ + 16688
[from(x₁)]	=	x₁ + 1
[s^#(x₁)]	=	0
[nil]	=	8590
[mark(x₁)]	=	x₁ + 12114
[proper^#(x₁)]	=	0
[from^#(x₁)]	=	0
[active(x₁)]	=	41143
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

active(dbl(0))	→	mark(0)	(1)
active(dbls(nil))	→	mark(nil)	(3)
active(indx(nil,X))	→	mark(nil)	(7)
proper(nil)	→	ok(nil)	(24)
from(ok(X))	→	ok(from(X))	(35)

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

dbls^#(mark(X))

→

dbls^#(X)

(48)

could be deleted.

1.1.10.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.