Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM01_iGM)

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)
mark(incr(X))	→	active(incr(mark(X)))	(9)
mark(nil)	→	active(nil)	(10)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(11)
mark(s(X))	→	active(s(mark(X)))	(12)
mark(adx(X))	→	active(adx(mark(X)))	(13)
mark(nats)	→	active(nats)	(14)
mark(zeros)	→	active(zeros)	(15)
mark(0)	→	active(0)	(16)
mark(head(X))	→	active(head(mark(X)))	(17)
mark(tail(X))	→	active(tail(mark(X)))	(18)
incr(mark(X))	→	incr(X)	(19)
incr(active(X))	→	incr(X)	(20)
cons(mark(X1),X2)	→	cons(X1,X2)	(21)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
s(mark(X))	→	s(X)	(25)
s(active(X))	→	s(X)	(26)
adx(mark(X))	→	adx(X)	(27)
adx(active(X))	→	adx(X)	(28)
head(mark(X))	→	head(X)	(29)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
tail(active(X))	→	tail(X)	(32)

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

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

mark^#(tail(X))	→	active^#(tail(mark(X)))	(83)
mark^#(tail(X))	→	mark^#(X)	(57)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(55)
mark^#(adx(X))	→	active^#(adx(mark(X)))	(80)
mark^#(zeros)	→	active^#(zeros)	(52)
active^#(incr(cons(X,L)))	→	mark^#(cons(s(X),incr(L)))	(79)
mark^#(nats)	→	active^#(nats)	(51)
mark^#(cons(X1,X2))	→	mark^#(X1)	(77)
mark^#(s(X))	→	mark^#(X)	(76)
mark^#(head(X))	→	mark^#(X)	(75)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(49)
mark^#(incr(X))	→	mark^#(X)	(47)
mark^#(s(X))	→	active^#(s(mark(X)))	(73)
active^#(zeros)	→	mark^#(cons(0,zeros))	(44)
active^#(head(cons(X,L)))	→	mark^#(X)	(70)
mark^#(head(X))	→	active^#(head(mark(X)))	(69)
active^#(tail(cons(X,L)))	→	mark^#(L)	(66)
mark^#(adx(X))	→	mark^#(X)	(63)
active^#(adx(cons(X,L)))	→	mark^#(incr(cons(X,adx(L))))	(37)
active^#(nats)	→	mark^#(adx(zeros))	(35)

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
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 1
[zeros]	=	1
[tail(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	x₁ + 0
[0]	=	0
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[incr^#(x₁)]	=	0
[nats]	=	3
[active(x₁)]	=	x₁ + 0
[head(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + x₂ + 0
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

mark(tail(X))	→	active(tail(mark(X)))	(18)
active(adx(cons(X,L)))	→	mark(incr(cons(X,adx(L))))	(4)
mark(zeros)	→	active(zeros)	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
mark(0)	→	active(0)	(16)
cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
mark(head(X))	→	active(head(mark(X)))	(17)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
active(nats)	→	mark(adx(zeros))	(5)
mark(nil)	→	active(nil)	(10)
active(head(cons(X,L)))	→	mark(X)	(7)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
mark(nats)	→	active(nats)	(14)
tail(mark(X))	→	tail(X)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(11)
mark(incr(X))	→	active(incr(mark(X)))	(9)
mark(adx(X))	→	active(adx(mark(X)))	(13)
active(zeros)	→	mark(cons(0,zeros))	(6)
head(mark(X))	→	head(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 pairs

mark^#(tail(X))	→	mark^#(X)	(57)
mark^#(head(X))	→	mark^#(X)	(75)
active^#(head(cons(X,L)))	→	mark^#(X)	(70)
active^#(tail(cons(X,L)))	→	mark^#(L)	(66)
mark^#(adx(X))	→	mark^#(X)	(63)
active^#(nats)	→	mark^#(adx(zeros))	(35)

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

mark^#(tail(X))	→	active^#(tail(mark(X)))	(83)
active^#(adx(cons(X,L)))	→	mark^#(incr(cons(X,adx(L))))	(37)
mark^#(zeros)	→	active^#(zeros)	(52)
mark^#(head(X))	→	active^#(head(mark(X)))	(69)
mark^#(s(X))	→	mark^#(X)	(76)
mark^#(s(X))	→	active^#(s(mark(X)))	(73)
mark^#(cons(X1,X2))	→	mark^#(X1)	(77)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(55)
mark^#(incr(X))	→	mark^#(X)	(47)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(49)
mark^#(adx(X))	→	active^#(adx(mark(X)))	(80)
active^#(zeros)	→	mark^#(cons(0,zeros))	(44)
active^#(incr(cons(X,L)))	→	mark^#(cons(s(X),incr(L)))	(79)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	21035
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	841
[head^#(x₁)]	=	0
[adx(x₁)]	=	21035
[zeros]	=	21035
[tail(x₁)]	=	1
[mark^#(x₁)]	=	21035
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	1
[incr^#(x₁)]	=	0
[nats]	=	1
[active(x₁)]	=	1
[head(x₁)]	=	16908
[cons(x₁, x₂)]	=	18588
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

mark^#(tail(X))	→	active^#(tail(mark(X)))	(83)
mark^#(head(X))	→	active^#(head(mark(X)))	(69)
mark^#(s(X))	→	active^#(s(mark(X)))	(73)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(55)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(adx(cons(X,L)))	→	mark^#(incr(cons(X,adx(L))))	(37)
mark^#(zeros)	→	active^#(zeros)	(52)
mark^#(s(X))	→	mark^#(X)	(76)
mark^#(cons(X1,X2))	→	mark^#(X1)	(77)
mark^#(incr(X))	→	mark^#(X)	(47)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(49)
mark^#(adx(X))	→	active^#(adx(mark(X)))	(80)
active^#(zeros)	→	mark^#(cons(0,zeros))	(44)
active^#(incr(cons(X,L)))	→	mark^#(cons(s(X),incr(L)))	(79)

1.1.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₂)]	=	max(0)
[s(x₁)]	=	x₁ + 0
[head^#(x₁)]	=	0
[adx(x₁)]	=	x₁ + 18459
[zeros]	=	16006
[tail(x₁)]	=	x₁ + 47562
[mark^#(x₁)]	=	x₁ + 0
[0]	=	16004
[s^#(x₁)]	=	0
[nil]	=	49858
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[incr^#(x₁)]	=	0
[nats]	=	34465
[active(x₁)]	=	x₁ + 0
[head(x₁)]	=	x₁ + 34132
[cons(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[active^#(x₁)]	=	x₁ + 0

together with the usable rules

mark(tail(X))	→	active(tail(mark(X)))	(18)
active(adx(cons(X,L)))	→	mark(incr(cons(X,adx(L))))	(4)
mark(zeros)	→	active(zeros)	(15)
active(tail(cons(X,L)))	→	mark(L)	(8)
active(incr(nil))	→	mark(nil)	(1)
active(adx(nil))	→	mark(nil)	(3)
mark(0)	→	active(0)	(16)
cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
mark(head(X))	→	active(head(mark(X)))	(17)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
active(nats)	→	mark(adx(zeros))	(5)
mark(nil)	→	active(nil)	(10)
active(head(cons(X,L)))	→	mark(X)	(7)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
mark(nats)	→	active(nats)	(14)
tail(mark(X))	→	tail(X)	(31)
mark(s(X))	→	active(s(mark(X)))	(12)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(11)
mark(incr(X))	→	active(incr(mark(X)))	(9)
mark(adx(X))	→	active(adx(mark(X)))	(13)
active(zeros)	→	mark(cons(0,zeros))	(6)
head(mark(X))	→	head(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

mark^#(cons(X1,X2))

→

mark^#(X1)

(77)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(adx(cons(X,L)))	→	mark^#(incr(cons(X,adx(L))))	(37)
mark^#(s(X))	→	mark^#(X)	(76)
mark^#(incr(X))	→	mark^#(X)	(47)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(49)
mark^#(adx(X))	→	active^#(adx(mark(X)))	(80)
active^#(incr(cons(X,L)))	→	mark^#(cons(s(X),incr(L)))	(79)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	x₁ + 8405
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 26929
[head^#(x₁)]	=	0
[adx(x₁)]	=	8406
[zeros]	=	2685
[tail(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 12630
[0]	=	1103
[s^#(x₁)]	=	0
[nil]	=	1
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 21654
[incr^#(x₁)]	=	0
[nats]	=	0
[active(x₁)]	=	x₁ + 0
[head(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	0
[active^#(x₁)]	=	21035

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)

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

mark^#(s(X))	→	mark^#(X)	(76)
mark^#(incr(X))	→	mark^#(X)	(47)
mark^#(adx(X))	→	active^#(adx(mark(X)))	(80)
active^#(incr(cons(X,L)))	→	mark^#(cons(s(X),incr(L)))	(79)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(adx(cons(X,L)))	→	mark^#(incr(cons(X,adx(L))))	(37)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(49)

1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	2805
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	2809
[head^#(x₁)]	=	0
[adx(x₁)]	=	2807
[zeros]	=	1
[tail(x₁)]	=	3048
[mark^#(x₁)]	=	12630
[0]	=	2809
[s^#(x₁)]	=	0
[nil]	=	26313
[tail^#(x₁)]	=	0
[mark(x₁)]	=	2808
[incr^#(x₁)]	=	0
[nats]	=	0
[active(x₁)]	=	x₁ + 0
[head(x₁)]	=	2809
[cons(x₁, x₂)]	=	2809
[active^#(x₁)]	=	x₁ + 9824

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

active^#(adx(cons(X,L)))	→	mark^#(incr(cons(X,adx(L))))	(37)
mark^#(incr(X))	→	active^#(incr(mark(X)))	(49)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

head^#(active(X))	→	head^#(X)	(50)
head^#(mark(X))	→	head^#(X)	(65)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	41350
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	37697
[head^#(x₁)]	=	x₁ + 0
[adx(x₁)]	=	25729
[zeros]	=	2
[tail(x₁)]	=	36467
[mark^#(x₁)]	=	12630
[0]	=	36868
[s^#(x₁)]	=	0
[nil]	=	41352
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[nats]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	36560
[cons(x₁, x₂)]	=	72601
[active^#(x₁)]	=	x₁ + 9824

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

head^#(active(X))	→	head^#(X)	(50)
head^#(mark(X))	→	head^#(X)	(65)

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

incr^#(active(X))	→	incr^#(X)	(74)
incr^#(mark(X))	→	incr^#(X)	(43)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	11940
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	39990
[head^#(x₁)]	=	0
[adx(x₁)]	=	5970
[zeros]	=	3578
[tail(x₁)]	=	37145
[mark^#(x₁)]	=	12630
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	17910
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	x₁ + 0
[nats]	=	0
[active(x₁)]	=	x₁ + 5970
[head(x₁)]	=	31381
[cons(x₁, x₂)]	=	17910
[active^#(x₁)]	=	x₁ + 9824

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

incr^#(active(X))	→	incr^#(X)	(74)
incr^#(mark(X))	→	incr^#(X)	(43)

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

adx^#(active(X))	→	adx^#(X)	(54)
adx^#(mark(X))	→	adx^#(X)	(64)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	x₁ + 0
[incr(x₁)]	=	19288
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	39990
[head^#(x₁)]	=	0
[adx(x₁)]	=	9644
[zeros]	=	1
[tail(x₁)]	=	12644
[mark^#(x₁)]	=	12630
[0]	=	61688
[s^#(x₁)]	=	0
[nil]	=	28932
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[nats]	=	0
[active(x₁)]	=	x₁ + 9644
[head(x₁)]	=	30638
[cons(x₁, x₂)]	=	28932
[active^#(x₁)]	=	x₁ + 9824

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

adx^#(active(X))	→	adx^#(X)	(54)
adx^#(mark(X))	→	adx^#(X)	(64)

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)	(68)
tail^#(active(X))	→	tail^#(X)	(40)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	15084
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	39990
[head^#(x₁)]	=	0
[adx(x₁)]	=	15082
[zeros]	=	1
[tail(x₁)]	=	21691
[mark^#(x₁)]	=	12630
[0]	=	25011
[s^#(x₁)]	=	0
[nil]	=	15086
[tail^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[nats]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	38969
[cons(x₁, x₂)]	=	16148
[active^#(x₁)]	=	x₁ + 9824

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

tail^#(mark(X))	→	tail^#(X)	(68)
tail^#(active(X))	→	tail^#(X)	(40)

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

cons^#(active(X1),X2)	→	cons^#(X1,X2)	(84)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(72)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(71)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(45)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	16763
[cons^#(x₁, x₂)]	=	x₁ + 0
[s(x₁)]	=	16892
[head^#(x₁)]	=	0
[adx(x₁)]	=	16761
[zeros]	=	1
[tail(x₁)]	=	13927
[mark^#(x₁)]	=	12630
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	16765
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[nats]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	1
[cons(x₁, x₂)]	=	16765
[active^#(x₁)]	=	x₁ + 9824

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

cons^#(active(X1),X2)	→	cons^#(X1,X2)	(84)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(45)

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^#(X1,mark(X2))	→	cons^#(X1,X2)	(72)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(71)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	32799
[cons^#(x₁, x₂)]	=	x₂ + 0
[s(x₁)]	=	16892
[head^#(x₁)]	=	0
[adx(x₁)]	=	8823
[zeros]	=	1
[tail(x₁)]	=	31671
[mark^#(x₁)]	=	12630
[0]	=	1
[s^#(x₁)]	=	0
[nil]	=	32801
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[nats]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	49077
[cons(x₁, x₂)]	=	61271
[active^#(x₁)]	=	x₁ + 9824

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(72)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(71)

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

s^#(mark(X))	→	s^#(X)	(59)
s^#(active(X))	→	s^#(X)	(62)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[adx^#(x₁)]	=	0
[incr(x₁)]	=	6440
[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	16892
[head^#(x₁)]	=	0
[adx(x₁)]	=	6438
[zeros]	=	1
[tail(x₁)]	=	1
[mark^#(x₁)]	=	12630
[0]	=	20631
[s^#(x₁)]	=	x₁ + 0
[nil]	=	32801
[tail^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[incr^#(x₁)]	=	0
[nats]	=	0
[active(x₁)]	=	x₁ + 2
[head(x₁)]	=	19864
[cons(x₁, x₂)]	=	6442
[active^#(x₁)]	=	x₁ + 9824

together with the usable rules

cons(mark(X1),X2)	→	cons(X1,X2)	(21)
s(active(X))	→	s(X)	(26)
incr(mark(X))	→	incr(X)	(19)
tail(active(X))	→	tail(X)	(32)
adx(mark(X))	→	adx(X)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(22)
adx(active(X))	→	adx(X)	(28)
incr(active(X))	→	incr(X)	(20)
s(mark(X))	→	s(X)	(25)
head(active(X))	→	head(X)	(30)
tail(mark(X))	→	tail(X)	(31)
cons(active(X1),X2)	→	cons(X1,X2)	(23)
cons(X1,active(X2))	→	cons(X1,X2)	(24)
head(mark(X))	→	head(X)	(29)

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

s^#(mark(X))	→	s^#(X)	(59)
s^#(active(X))	→	s^#(X)	(62)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.