Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM01_C)

The rewrite relation of the following TRS is considered.

active(incr(nil))	→	mark(nil)	(1)
active(incr(cons(X,L)))	→	mark(cons(s(X),incr(L)))	(2)
active(adx(nil))	→	mark(nil)	(3)
active(adx(cons(X,L)))	→	mark(incr(cons(X,adx(L))))	(4)
active(nats)	→	mark(adx(zeros))	(5)
active(zeros)	→	mark(cons(0,zeros))	(6)
active(head(cons(X,L)))	→	mark(X)	(7)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(X))	→	incr(active(X))	(9)
active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
active(s(X))	→	s(active(X))	(11)
active(adx(X))	→	adx(active(X))	(12)
active(head(X))	→	head(active(X))	(13)
active(tail(X))	→	tail(active(X))	(14)
incr(mark(X))	→	mark(incr(X))	(15)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(16)
s(mark(X))	→	mark(s(X))	(17)
adx(mark(X))	→	mark(adx(X))	(18)
head(mark(X))	→	mark(head(X))	(19)
tail(mark(X))	→	mark(tail(X))	(20)
proper(incr(X))	→	incr(proper(X))	(21)
proper(nil)	→	ok(nil)	(22)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(23)
proper(s(X))	→	s(proper(X))	(24)
proper(adx(X))	→	adx(proper(X))	(25)
proper(nats)	→	ok(nats)	(26)
proper(zeros)	→	ok(zeros)	(27)
proper(0)	→	ok(0)	(28)
proper(head(X))	→	head(proper(X))	(29)
proper(tail(X))	→	tail(proper(X))	(30)
incr(ok(X))	→	ok(incr(X))	(31)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
s(ok(X))	→	ok(s(X))	(33)
adx(ok(X))	→	ok(adx(X))	(34)
head(ok(X))	→	ok(head(X))	(35)
tail(ok(X))	→	ok(tail(X))	(36)
top(mark(X))	→	top(proper(X))	(37)
top(ok(X))	→	top(active(X))	(38)

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^#(incr(cons(X,L)))	→	s^#(X)	(39)
proper^#(incr(X))	→	proper^#(X)	(40)
proper^#(tail(X))	→	proper^#(X)	(41)
s^#(ok(X))	→	s^#(X)	(42)
active^#(adx(cons(X,L)))	→	incr^#(cons(X,adx(L)))	(43)
proper^#(incr(X))	→	incr^#(proper(X))	(44)
tail^#(ok(X))	→	tail^#(X)	(45)
adx^#(ok(X))	→	adx^#(X)	(46)
active^#(adx(cons(X,L)))	→	cons^#(X,adx(L))	(47)
active^#(adx(cons(X,L)))	→	adx^#(L)	(48)
s^#(mark(X))	→	s^#(X)	(49)
head^#(ok(X))	→	head^#(X)	(50)
head^#(mark(X))	→	head^#(X)	(51)
active^#(head(X))	→	active^#(X)	(52)
top^#(ok(X))	→	top^#(active(X))	(53)
active^#(zeros)	→	cons^#(0,zeros)	(54)
active^#(adx(X))	→	active^#(X)	(55)
active^#(adx(X))	→	adx^#(active(X))	(56)
incr^#(mark(X))	→	incr^#(X)	(57)
active^#(head(X))	→	head^#(active(X))	(58)
proper^#(adx(X))	→	proper^#(X)	(59)
active^#(incr(X))	→	incr^#(active(X))	(60)
proper^#(adx(X))	→	adx^#(proper(X))	(61)
adx^#(mark(X))	→	adx^#(X)	(62)
incr^#(ok(X))	→	incr^#(X)	(63)
proper^#(cons(X1,X2))	→	cons^#(proper(X1),proper(X2))	(64)
top^#(mark(X))	→	top^#(proper(X))	(65)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(66)
top^#(ok(X))	→	active^#(X)	(67)
active^#(cons(X1,X2))	→	cons^#(active(X1),X2)	(68)
proper^#(head(X))	→	proper^#(X)	(69)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(70)
proper^#(tail(X))	→	tail^#(proper(X))	(71)
proper^#(cons(X1,X2))	→	proper^#(X2)	(72)
active^#(cons(X1,X2))	→	active^#(X1)	(73)
active^#(tail(X))	→	active^#(X)	(74)
active^#(s(X))	→	active^#(X)	(75)
tail^#(mark(X))	→	tail^#(X)	(76)
proper^#(s(X))	→	proper^#(X)	(77)
active^#(tail(X))	→	tail^#(active(X))	(78)
active^#(nats)	→	adx^#(zeros)	(79)
proper^#(cons(X1,X2))	→	proper^#(X1)	(80)
active^#(s(X))	→	s^#(active(X))	(81)
active^#(incr(cons(X,L)))	→	incr^#(L)	(82)
active^#(incr(cons(X,L)))	→	cons^#(s(X),incr(L))	(83)
top^#(mark(X))	→	proper^#(X)	(84)
active^#(incr(X))	→	active^#(X)	(85)
proper^#(head(X))	→	head^#(proper(X))	(86)
proper^#(s(X))	→	s^#(proper(X))	(87)

1.1 Dependency Graph Processor

The dependency pairs are split into 9 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(53)
top^#(mark(X))	→	top^#(proper(X))	(65)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(s)	=	1
π(top^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(s^#)	=	1
π(active)	=	1

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

prec(adx^#)	=	0	status(adx^#)	=	[]	list-extension(adx^#)	=	Lex
prec(incr)	=	7	status(incr)	=	[1]	list-extension(incr)	=	Lex
prec(cons^#)	=	0	status(cons^#)	=	[]	list-extension(cons^#)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(head^#)	=	0	status(head^#)	=	[]	list-extension(head^#)	=	Lex
prec(adx)	=	8	status(adx)	=	[1]	list-extension(adx)	=	Lex
prec(zeros)	=	3	status(zeros)	=	[]	list-extension(zeros)	=	Lex
prec(tail)	=	3	status(tail)	=	[1]	list-extension(tail)	=	Lex
prec(0)	=	3	status(0)	=	[]	list-extension(0)	=	Lex
prec(nil)	=	4	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(tail^#)	=	0	status(tail^#)	=	[]	list-extension(tail^#)	=	Lex
prec(mark)	=	1	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(incr^#)	=	0	status(incr^#)	=	[]	list-extension(incr^#)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(nats)	=	3	status(nats)	=	[]	list-extension(nats)	=	Lex
prec(head)	=	4	status(head)	=	[1]	list-extension(head)	=	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

[adx^#(x₁)]	=	1
[incr(x₁)]	=	x₁ + 0
[cons^#(x₁, x₂)]	=	x₁ + 1
[top(x₁)]	=	1
[head^#(x₁)]	=	1
[adx(x₁)]	=	x₁ + 1
[zeros]	=	36983
[tail(x₁)]	=	x₁ + 1
[0]	=	0
[nil]	=	24696
[tail^#(x₁)]	=	1
[mark(x₁)]	=	x₁ + 0
[incr^#(x₁)]	=	1
[proper^#(x₁)]	=	1
[nats]	=	36985
[head(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[active^#(x₁)]	=	1

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
active(adx(cons(X,L)))	→	mark(incr(cons(X,adx(L))))	(4)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(16)
proper(incr(X))	→	incr(proper(X))	(21)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
proper(adx(X))	→	adx(proper(X))	(25)
proper(tail(X))	→	tail(proper(X))	(30)
active(tail(X))	→	tail(active(X))	(14)
incr(ok(X))	→	ok(incr(X))	(31)
active(adx(X))	→	adx(active(X))	(12)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(23)
proper(s(X))	→	s(proper(X))	(24)
active(s(X))	→	s(active(X))	(11)
active(incr(X))	→	incr(active(X))	(9)
active(head(X))	→	head(active(X))	(13)
active(zeros)	→	mark(cons(0,zeros))	(6)
head(ok(X))	→	ok(head(X))	(35)
proper(head(X))	→	head(proper(X))	(29)
active(incr(cons(X,L)))	→	mark(cons(s(X),incr(L)))	(2)

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

top^#(mark(X))

→

top^#(proper(X))

(65)

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

(53)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 0
[zeros]	=	1
[tail(x₁)]	=	x₁ + 0
[proper(x₁)]	=	18006
[ok(x₁)]	=	18006
[0]	=	16674
[s^#(x₁)]	=	0
[nil]	=	14972
[tail^#(x₁)]	=	0
[mark(x₁)]	=	1
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[nats]	=	1
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + 0
[active^#(x₁)]	=	0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
active(adx(cons(X,L)))	→	mark(incr(cons(X,adx(L))))	(4)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(16)
proper(incr(X))	→	incr(proper(X))	(21)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
proper(adx(X))	→	adx(proper(X))	(25)
proper(tail(X))	→	tail(proper(X))	(30)
active(tail(X))	→	tail(active(X))	(14)
incr(ok(X))	→	ok(incr(X))	(31)
active(adx(X))	→	adx(active(X))	(12)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(23)
proper(s(X))	→	s(proper(X))	(24)
active(s(X))	→	s(active(X))	(11)
active(incr(X))	→	incr(active(X))	(9)
active(head(X))	→	head(active(X))	(13)
active(zeros)	→	mark(cons(0,zeros))	(6)
head(ok(X))	→	ok(head(X))	(35)
proper(head(X))	→	head(proper(X))	(29)
active(incr(cons(X,L)))	→	mark(cons(s(X),incr(L)))	(2)

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

top^#(ok(X))

→

top^#(active(X))

(53)

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^#(incr(X))	→	active^#(X)	(85)
active^#(adx(X))	→	active^#(X)	(55)
active^#(head(X))	→	active^#(X)	(52)
active^#(s(X))	→	active^#(X)	(75)
active^#(tail(X))	→	active^#(X)	(74)
active^#(cons(X1,X2))	→	active^#(X1)	(73)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 0
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 0
[zeros]	=	1
[tail(x₁)]	=	x₁ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	1
[0]	=	27691
[s^#(x₁)]	=	0
[nil]	=	240
[tail^#(x₁)]	=	0
[mark(x₁)]	=	1
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[nats]	=	1
[active(x₁)]	=	1
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
active(adx(cons(X,L)))	→	mark(incr(cons(X,adx(L))))	(4)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(16)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
active(zeros)	→	mark(cons(0,zeros))	(6)
head(ok(X))	→	ok(head(X))	(35)
active(incr(cons(X,L)))	→	mark(cons(s(X),incr(L)))	(2)

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

active^#(s(X))

→

active^#(X)

(75)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(cons(X1,X2))	→	active^#(X1)	(73)
active^#(tail(X))	→	active^#(X)	(74)
active^#(adx(X))	→	active^#(X)	(55)
active^#(incr(X))	→	active^#(X)	(85)
active^#(head(X))	→	active^#(X)	(52)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 12831
[zeros]	=	2
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	1
[ok(x₁)]	=	1
[0]	=	36868
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	15620
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[nats]	=	2
[active(x₁)]	=	x₁ + 56977
[head(x₁)]	=	x₁ + 23637
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
active(adx(cons(X,L)))	→	mark(incr(cons(X,adx(L))))	(4)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(16)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(32)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
active(zeros)	→	mark(cons(0,zeros))	(6)
head(ok(X))	→	ok(head(X))	(35)
active(incr(cons(X,L)))	→	mark(cons(s(X),incr(L)))	(2)

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

active^#(cons(X1,X2))	→	active^#(X1)	(73)
active^#(tail(X))	→	active^#(X)	(74)
active^#(adx(X))	→	active^#(X)	(55)
active^#(incr(X))	→	active^#(X)	(85)
active^#(head(X))	→	active^#(X)	(52)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

proper^#(adx(X))	→	proper^#(X)	(59)
proper^#(cons(X1,X2))	→	proper^#(X1)	(80)
proper^#(s(X))	→	proper^#(X)	(77)
proper^#(cons(X1,X2))	→	proper^#(X2)	(72)
proper^#(head(X))	→	proper^#(X)	(69)
proper^#(tail(X))	→	proper^#(X)	(41)
proper^#(incr(X))	→	proper^#(X)	(40)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 1
[zeros]	=	1
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	10378
[ok(x₁)]	=	x₁ + 10377
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	2
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	x₁ + 0
[nats]	=	1
[active(x₁)]	=	x₁ + 1
[head(x₁)]	=	x₁ + 23637
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
active(adx(cons(X,L)))	→	mark(incr(cons(X,adx(L))))	(4)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(16)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
active(zeros)	→	mark(cons(0,zeros))	(6)
head(ok(X))	→	ok(head(X))	(35)
active(incr(cons(X,L)))	→	mark(cons(s(X),incr(L)))	(2)

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

proper^#(adx(X))	→	proper^#(X)	(59)
proper^#(cons(X1,X2))	→	proper^#(X1)	(80)
proper^#(s(X))	→	proper^#(X)	(77)
proper^#(cons(X1,X2))	→	proper^#(X2)	(72)
proper^#(head(X))	→	proper^#(X)	(69)
proper^#(tail(X))	→	proper^#(X)	(41)
proper^#(incr(X))	→	proper^#(X)	(40)

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

head^#(mark(X))	→	head^#(X)	(51)
head^#(ok(X))	→	head^#(X)	(50)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	x₁ + 0
[adx(x₁)]	=	x₁ + 1
[zeros]	=	35712
[tail(x₁)]	=	x₁ + 15047
[proper(x₁)]	=	35713
[ok(x₁)]	=	x₁ + 1
[0]	=	32582
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 14459
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[nats]	=	35712
[active(x₁)]	=	x₁ + 14460
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 55803
[active^#(x₁)]	=	0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
head(ok(X))	→	ok(head(X))	(35)

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

head^#(mark(X))	→	head^#(X)	(51)
head^#(ok(X))	→	head^#(X)	(50)

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

tail^#(mark(X))	→	tail^#(X)	(76)
tail^#(ok(X))	→	tail^#(X)	(45)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 1
[zeros]	=	1
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[nats]	=	1
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
head(ok(X))	→	ok(head(X))	(35)

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

tail^#(mark(X))	→	tail^#(X)	(76)
tail^#(ok(X))	→	tail^#(X)	(45)

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

adx^#(mark(X))	→	adx^#(X)	(62)
adx^#(ok(X))	→	adx^#(X)	(46)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	x₁ + 0
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 1
[zeros]	=	1
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[nats]	=	1
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
head(ok(X))	→	ok(head(X))	(35)

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

adx^#(mark(X))	→	adx^#(X)	(62)
adx^#(ok(X))	→	adx^#(X)	(46)

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

incr^#(ok(X))	→	incr^#(X)	(63)
incr^#(mark(X))	→	incr^#(X)	(57)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 26205
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 11842
[zeros]	=	1
[tail(x₁)]	=	x₁ + 8855
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[nats]	=	1
[active(x₁)]	=	x₁ + 42699
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 42698
[active^#(x₁)]	=	0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
head(ok(X))	→	ok(head(X))	(35)

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

incr^#(ok(X))	→	incr^#(X)	(63)
incr^#(mark(X))	→	incr^#(X)	(57)

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^#(mark(X))	→	s^#(X)	(49)
s^#(ok(X))	→	s^#(X)	(42)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 1
[zeros]	=	1
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	x₁ + 0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[nats]	=	1
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
head(ok(X))	→	ok(head(X))	(35)

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

s^#(mark(X))	→	s^#(X)	(49)
s^#(ok(X))	→	s^#(X)	(42)

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(70)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(66)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 1
[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 1
[zeros]	=	29430
[tail(x₁)]	=	x₁ + 1
[proper(x₁)]	=	29431
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[proper^#(x₁)]	=	0
[nats]	=	29430
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0

together with the usable rules

adx(mark(X))	→	mark(adx(X))	(18)
incr(mark(X))	→	mark(incr(X))	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
tail(ok(X))	→	ok(tail(X))	(36)
proper(nats)	→	ok(nats)	(26)
head(mark(X))	→	mark(head(X))	(19)
s(mark(X))	→	mark(s(X))	(17)
proper(zeros)	→	ok(zeros)	(27)
adx(ok(X))	→	ok(adx(X))	(34)
proper(nil)	→	ok(nil)	(22)
proper(0)	→	ok(0)	(28)
active(nats)	→	mark(adx(zeros))	(5)
s(ok(X))	→	ok(s(X))	(33)
active(head(cons(X,L)))	→	mark(X)	(7)
tail(mark(X))	→	mark(tail(X))	(20)
incr(ok(X))	→	ok(incr(X))	(31)
head(ok(X))	→	ok(head(X))	(35)

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

cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(70)
cons^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(66)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 0 components.