Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_Luc02b_C)

The rewrite relation of the following TRS is considered.

active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(first(0,Z))	→	mark(nil)	(2)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(3)
active(sel(0,cons(X,Z)))	→	mark(X)	(4)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(5)
active(from(X))	→	from(active(X))	(6)
active(cons(X1,X2))	→	cons(active(X1),X2)	(7)
active(s(X))	→	s(active(X))	(8)
active(first(X1,X2))	→	first(active(X1),X2)	(9)
active(first(X1,X2))	→	first(X1,active(X2))	(10)
active(sel(X1,X2))	→	sel(active(X1),X2)	(11)
active(sel(X1,X2))	→	sel(X1,active(X2))	(12)
from(mark(X))	→	mark(from(X))	(13)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(14)
s(mark(X))	→	mark(s(X))	(15)
first(mark(X1),X2)	→	mark(first(X1,X2))	(16)
first(X1,mark(X2))	→	mark(first(X1,X2))	(17)
sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
proper(from(X))	→	from(proper(X))	(20)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(21)
proper(s(X))	→	s(proper(X))	(22)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(23)
proper(0)	→	ok(0)	(24)
proper(nil)	→	ok(nil)	(25)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
from(ok(X))	→	ok(from(X))	(27)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(28)
s(ok(X))	→	ok(s(X))	(29)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(30)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
top(mark(X))	→	top(proper(X))	(32)
top(ok(X))	→	top(active(X))	(33)

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^#(from(X))	→	from^#(active(X))	(34)
active^#(from(X))	→	cons^#(X,from(s(X)))	(35)
from^#(ok(X))	→	from^#(X)	(36)
proper^#(sel(X1,X2))	→	proper^#(X1)	(37)
active^#(s(X))	→	s^#(active(X))	(38)
active^#(first(s(X),cons(Y,Z)))	→	first^#(X,Z)	(39)
active^#(first(s(X),cons(Y,Z)))	→	cons^#(Y,first(X,Z))	(40)
proper^#(cons(X1,X2))	→	cons^#(proper(X1),proper(X2))	(41)
active^#(s(X))	→	active^#(X)	(42)
s^#(mark(X))	→	s^#(X)	(43)
proper^#(cons(X1,X2))	→	proper^#(X1)	(44)
active^#(first(X1,X2))	→	active^#(X1)	(45)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(46)
active^#(sel(X1,X2))	→	active^#(X2)	(47)
proper^#(first(X1,X2))	→	first^#(proper(X1),proper(X2))	(48)
proper^#(first(X1,X2))	→	proper^#(X2)	(49)
top^#(ok(X))	→	active^#(X)	(50)
top^#(ok(X))	→	top^#(active(X))	(51)
active^#(from(X))	→	s^#(X)	(52)
active^#(sel(X1,X2))	→	sel^#(X1,active(X2))	(53)
top^#(mark(X))	→	top^#(proper(X))	(54)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(55)
first^#(X1,mark(X2))	→	first^#(X1,X2)	(56)
sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(57)
active^#(sel(s(X),cons(Y,Z)))	→	sel^#(X,Z)	(58)
active^#(cons(X1,X2))	→	active^#(X1)	(59)
active^#(sel(X1,X2))	→	sel^#(active(X1),X2)	(60)
proper^#(cons(X1,X2))	→	proper^#(X2)	(61)
proper^#(first(X1,X2))	→	proper^#(X1)	(62)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(63)
active^#(first(X1,X2))	→	first^#(active(X1),X2)	(64)
active^#(from(X))	→	from^#(s(X))	(65)
proper^#(s(X))	→	proper^#(X)	(66)
active^#(first(X1,X2))	→	active^#(X2)	(67)
proper^#(sel(X1,X2))	→	sel^#(proper(X1),proper(X2))	(68)
proper^#(s(X))	→	s^#(proper(X))	(69)
proper^#(from(X))	→	from^#(proper(X))	(70)
top^#(mark(X))	→	proper^#(X)	(71)
active^#(cons(X1,X2))	→	cons^#(active(X1),X2)	(72)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(73)
proper^#(sel(X1,X2))	→	proper^#(X2)	(74)
active^#(first(X1,X2))	→	first^#(X1,active(X2))	(75)
first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(76)
active^#(from(X))	→	active^#(X)	(77)
s^#(ok(X))	→	s^#(X)	(78)
active^#(sel(X1,X2))	→	active^#(X1)	(79)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(80)
from^#(mark(X))	→	from^#(X)	(81)
proper^#(from(X))	→	proper^#(X)	(82)

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

The 1^st component contains the pair

top^#(mark(X))	→	top^#(proper(X))	(54)
top^#(ok(X))	→	top^#(active(X))	(51)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(cons^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(first^#)	=	1
π(active)	=	1

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

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

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 0
[top(x₁)]	=	1
[top^#(x₁)]	=	x₁ + 1
[0]	=	38608
[sel^#(x₁, x₂)]	=	1
[from(x₁)]	=	x₁ + 2243
[sel(x₁, x₂)]	=	x₁ + x₂ + 2241
[s^#(x₁)]	=	1
[nil]	=	38607
[mark(x₁)]	=	x₁ + 0
[first(x₁, x₂)]	=	x₁ + x₂ + 2242
[proper^#(x₁)]	=	1
[from^#(x₁)]	=	1
[cons(x₁, x₂)]	=	max(x₁ + 2242, x₂ + 0, 0)
[active^#(x₁)]	=	1

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
active(sel(0,cons(X,Z)))	→	mark(X)	(4)
s(mark(X))	→	mark(s(X))	(15)
active(s(X))	→	s(active(X))	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(3)
first(mark(X1),X2)	→	mark(first(X1,X2))	(16)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(21)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
first(X1,mark(X2))	→	mark(first(X1,X2))	(17)
from(ok(X))	→	ok(from(X))	(27)
proper(s(X))	→	s(proper(X))	(22)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(28)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(5)
active(first(X1,X2))	→	first(X1,active(X2))	(10)
active(cons(X1,X2))	→	cons(active(X1),X2)	(7)
proper(from(X))	→	from(proper(X))	(20)
proper(nil)	→	ok(nil)	(25)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(30)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(14)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(sel(X1,X2))	→	sel(X1,active(X2))	(12)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(23)
proper(0)	→	ok(0)	(24)
active(sel(X1,X2))	→	sel(active(X1),X2)	(11)
active(first(X1,X2))	→	first(active(X1),X2)	(9)
from(mark(X))	→	mark(from(X))	(13)
active(from(X))	→	from(active(X))	(6)
s(ok(X))	→	ok(s(X))	(29)
active(first(0,Z))	→	mark(nil)	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(54)

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

(51)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	3
[ok(x₁)]	=	x₁ + 2
[0]	=	1
[sel^#(x₁, x₂)]	=	0
[from(x₁)]	=	x₁ + 0
[sel(x₁, x₂)]	=	x₁ + 0
[s^#(x₁)]	=	0
[first^#(x₁, x₂)]	=	0
[nil]	=	1
[mark(x₁)]	=	0
[first(x₁, x₂)]	=	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(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
active(sel(0,cons(X,Z)))	→	mark(X)	(4)
s(mark(X))	→	mark(s(X))	(15)
active(s(X))	→	s(active(X))	(8)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(3)
first(mark(X1),X2)	→	mark(first(X1,X2))	(16)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(21)
proper(sel(X1,X2))	→	sel(proper(X1),proper(X2))	(26)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
first(X1,mark(X2))	→	mark(first(X1,X2))	(17)
from(ok(X))	→	ok(from(X))	(27)
proper(s(X))	→	s(proper(X))	(22)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(28)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(5)
active(first(X1,X2))	→	first(X1,active(X2))	(10)
active(cons(X1,X2))	→	cons(active(X1),X2)	(7)
proper(from(X))	→	from(proper(X))	(20)
proper(nil)	→	ok(nil)	(25)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(30)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(14)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(sel(X1,X2))	→	sel(X1,active(X2))	(12)
proper(first(X1,X2))	→	first(proper(X1),proper(X2))	(23)
proper(0)	→	ok(0)	(24)
active(sel(X1,X2))	→	sel(active(X1),X2)	(11)
active(first(X1,X2))	→	first(active(X1),X2)	(9)
from(mark(X))	→	mark(from(X))	(13)
active(from(X))	→	from(active(X))	(6)
s(ok(X))	→	ok(s(X))	(29)
active(first(0,Z))	→	mark(nil)	(2)

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

top^#(ok(X))

→

top^#(active(X))

(51)

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

proper^#(from(X))	→	proper^#(X)	(82)
proper^#(sel(X1,X2))	→	proper^#(X2)	(74)
proper^#(first(X1,X2))	→	proper^#(X2)	(49)
proper^#(cons(X1,X2))	→	proper^#(X1)	(44)
proper^#(s(X))	→	proper^#(X)	(66)
proper^#(first(X1,X2))	→	proper^#(X1)	(62)
proper^#(cons(X1,X2))	→	proper^#(X2)	(61)
proper^#(sel(X1,X2))	→	proper^#(X1)	(37)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
active(sel(0,cons(X,Z)))	→	mark(X)	(4)
s(mark(X))	→	mark(s(X))	(15)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(3)
first(mark(X1),X2)	→	mark(first(X1,X2))	(16)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(5)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(30)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

proper^#(from(X))	→	proper^#(X)	(82)
proper^#(sel(X1,X2))	→	proper^#(X2)	(74)
proper^#(first(X1,X2))	→	proper^#(X2)	(49)
proper^#(cons(X1,X2))	→	proper^#(X1)	(44)
proper^#(s(X))	→	proper^#(X)	(66)
proper^#(first(X1,X2))	→	proper^#(X1)	(62)
proper^#(cons(X1,X2))	→	proper^#(X2)	(61)
proper^#(sel(X1,X2))	→	proper^#(X1)	(37)

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

active^#(sel(X1,X2))	→	active^#(X1)	(79)
active^#(from(X))	→	active^#(X)	(77)
active^#(sel(X1,X2))	→	active^#(X2)	(47)
active^#(first(X1,X2))	→	active^#(X1)	(45)
active^#(first(X1,X2))	→	active^#(X2)	(67)
active^#(s(X))	→	active^#(X)	(42)
active^#(cons(X1,X2))	→	active^#(X1)	(59)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
active(sel(0,cons(X,Z)))	→	mark(X)	(4)
s(mark(X))	→	mark(s(X))	(15)
active(from(X))	→	mark(cons(X,from(s(X))))	(1)
active(first(s(X),cons(Y,Z)))	→	mark(cons(Y,first(X,Z)))	(3)
first(mark(X1),X2)	→	mark(first(X1,X2))	(16)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
active(sel(s(X),cons(Y,Z)))	→	mark(sel(X,Z))	(5)
first(ok(X1),ok(X2))	→	ok(first(X1,X2))	(30)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

active^#(sel(X1,X2))	→	active^#(X1)	(79)
active^#(from(X))	→	active^#(X)	(77)
active^#(sel(X1,X2))	→	active^#(X2)	(47)
active^#(first(X1,X2))	→	active^#(X1)	(45)
active^#(first(X1,X2))	→	active^#(X2)	(67)
active^#(s(X))	→	active^#(X)	(42)
active^#(cons(X1,X2))	→	active^#(X1)	(59)

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^#(mark(X1),X2)	→	sel^#(X1,X2)	(57)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(55)
sel^#(X1,mark(X2))	→	sel^#(X1,X2)	(63)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

sel^#(mark(X1),X2)	→	sel^#(X1,X2)	(57)
sel^#(ok(X1),ok(X2))	→	sel^#(X1,X2)	(55)

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^#(X1,mark(X2))

→

sel^#(X1,X2)

(63)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

sel^#(X1,mark(X2))

→

sel^#(X1,X2)

(63)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

first^#(X1,mark(X2))	→	first^#(X1,X2)	(56)
first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(76)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(46)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

first^#(ok(X1),ok(X2))	→	first^#(X1,X2)	(76)
first^#(mark(X1),X2)	→	first^#(X1,X2)	(46)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

first^#(X1,mark(X2))

→

first^#(X1,X2)

(56)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

first^#(X1,mark(X2))

→

first^#(X1,X2)

(56)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(80)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(73)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

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

→

cons^#(X1,X2)

(73)

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

cons^#(mark(X1),X2)

→

cons^#(X1,X2)

(80)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

cons^#(mark(X1),X2)

→

cons^#(X1,X2)

(80)

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

from^#(mark(X))	→	from^#(X)	(81)
from^#(ok(X))	→	from^#(X)	(36)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

from^#(mark(X))	→	from^#(X)	(81)
from^#(ok(X))	→	from^#(X)	(36)

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

s^#(ok(X))	→	s^#(X)	(78)
s^#(mark(X))	→	s^#(X)	(43)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

sel(mark(X1),X2)	→	mark(sel(X1,X2))	(18)
sel(X1,mark(X2))	→	mark(sel(X1,X2))	(19)
sel(ok(X1),ok(X2))	→	ok(sel(X1,X2))	(31)
active(first(0,Z))	→	mark(nil)	(2)

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

s^#(ok(X))	→	s^#(X)	(78)
s^#(mark(X))	→	s^#(X)	(43)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.