Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_GL02a_iGM)

The rewrite relation of the following TRS is considered.

active(eq(0,0))	→	mark(true)	(1)
active(eq(s(X),s(Y)))	→	mark(eq(X,Y))	(2)
active(eq(X,Y))	→	mark(false)	(3)
active(inf(X))	→	mark(cons(X,inf(s(X))))	(4)
active(take(0,X))	→	mark(nil)	(5)
active(take(s(X),cons(Y,L)))	→	mark(cons(Y,take(X,L)))	(6)
active(length(nil))	→	mark(0)	(7)
active(length(cons(X,L)))	→	mark(s(length(L)))	(8)
mark(eq(X1,X2))	→	active(eq(X1,X2))	(9)
mark(0)	→	active(0)	(10)
mark(true)	→	active(true)	(11)
mark(s(X))	→	active(s(X))	(12)
mark(false)	→	active(false)	(13)
mark(inf(X))	→	active(inf(mark(X)))	(14)
mark(cons(X1,X2))	→	active(cons(X1,X2))	(15)
mark(take(X1,X2))	→	active(take(mark(X1),mark(X2)))	(16)
mark(nil)	→	active(nil)	(17)
mark(length(X))	→	active(length(mark(X)))	(18)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
eq(active(X1),X2)	→	eq(X1,X2)	(21)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
inf(mark(X))	→	inf(X)	(25)
inf(active(X))	→	inf(X)	(26)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
cons(active(X1),X2)	→	cons(X1,X2)	(29)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
take(X1,mark(X2))	→	take(X1,X2)	(32)
take(active(X1),X2)	→	take(X1,X2)	(33)
take(X1,active(X2))	→	take(X1,X2)	(34)
length(mark(X))	→	length(X)	(35)
length(active(X))	→	length(X)	(36)

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^#(eq(s(X),s(Y)))	→	eq^#(X,Y)	(37)
active^#(length(cons(X,L)))	→	length^#(L)	(38)
mark^#(nil)	→	active^#(nil)	(39)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(40)
active^#(inf(X))	→	cons^#(X,inf(s(X)))	(41)
active^#(length(cons(X,L)))	→	s^#(length(L))	(42)
active^#(length(cons(X,L)))	→	mark^#(s(length(L)))	(43)
mark^#(take(X1,X2))	→	mark^#(X1)	(44)
active^#(inf(X))	→	inf^#(s(X))	(45)
active^#(inf(X))	→	s^#(X)	(46)
mark^#(take(X1,X2))	→	mark^#(X2)	(47)
active^#(take(s(X),cons(Y,L)))	→	cons^#(Y,take(X,L))	(48)
active^#(eq(0,0))	→	mark^#(true)	(49)
mark^#(length(X))	→	mark^#(X)	(50)
mark^#(s(X))	→	active^#(s(X))	(51)
mark^#(eq(X1,X2))	→	active^#(eq(X1,X2))	(52)
s^#(active(X))	→	s^#(X)	(53)
active^#(take(0,X))	→	mark^#(nil)	(54)
take^#(active(X1),X2)	→	take^#(X1,X2)	(55)
active^#(inf(X))	→	mark^#(cons(X,inf(s(X))))	(56)
s^#(mark(X))	→	s^#(X)	(57)
eq^#(mark(X1),X2)	→	eq^#(X1,X2)	(58)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(59)
take^#(X1,mark(X2))	→	take^#(X1,X2)	(60)
mark^#(length(X))	→	active^#(length(mark(X)))	(61)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(62)
eq^#(X1,mark(X2))	→	eq^#(X1,X2)	(63)
active^#(take(s(X),cons(Y,L)))	→	take^#(X,L)	(64)
active^#(eq(X,Y))	→	mark^#(false)	(65)
mark^#(true)	→	active^#(true)	(66)
length^#(active(X))	→	length^#(X)	(67)
active^#(take(s(X),cons(Y,L)))	→	mark^#(cons(Y,take(X,L)))	(68)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(69)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(70)
mark^#(0)	→	active^#(0)	(71)
eq^#(active(X1),X2)	→	eq^#(X1,X2)	(72)
take^#(X1,active(X2))	→	take^#(X1,X2)	(73)
mark^#(inf(X))	→	mark^#(X)	(74)
inf^#(active(X))	→	inf^#(X)	(75)
inf^#(mark(X))	→	inf^#(X)	(76)
eq^#(X1,active(X2))	→	eq^#(X1,X2)	(77)
mark^#(take(X1,X2))	→	take^#(mark(X1),mark(X2))	(78)
active^#(length(nil))	→	mark^#(0)	(79)
mark^#(inf(X))	→	inf^#(mark(X))	(80)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(81)
active^#(eq(s(X),s(Y)))	→	mark^#(eq(X,Y))	(82)
mark^#(false)	→	active^#(false)	(83)
mark^#(inf(X))	→	active^#(inf(mark(X)))	(84)
length^#(mark(X))	→	length^#(X)	(85)
mark^#(length(X))	→	length^#(mark(X))	(86)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(87)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

mark^#(length(X))	→	active^#(length(mark(X)))	(61)
mark^#(inf(X))	→	active^#(inf(mark(X)))	(84)
active^#(inf(X))	→	mark^#(cons(X,inf(s(X))))	(56)
active^#(eq(s(X),s(Y)))	→	mark^#(eq(X,Y))	(82)
mark^#(eq(X1,X2))	→	active^#(eq(X1,X2))	(52)
mark^#(s(X))	→	active^#(s(X))	(51)
mark^#(length(X))	→	mark^#(X)	(50)
mark^#(inf(X))	→	mark^#(X)	(74)
mark^#(take(X1,X2))	→	mark^#(X2)	(47)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(69)
active^#(take(s(X),cons(Y,L)))	→	mark^#(cons(Y,take(X,L)))	(68)
mark^#(take(X1,X2))	→	mark^#(X1)	(44)
active^#(length(cons(X,L)))	→	mark^#(s(length(L)))	(43)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(40)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	18588
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + x₂ + 15521
[eq(x₁, x₂)]	=	23423
[false]	=	11302
[true]	=	9726
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	27821
[s^#(x₁)]	=	0
[nil]	=	26497
[mark(x₁)]	=	x₁ + 0
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + 47339
[active^#(x₁)]	=	x₁ + 0
[length(x₁)]	=	x₁ + 1324
[length^#(x₁)]	=	0
[inf(x₁)]	=	x₁ + 47340

together with the usable rules

mark(length(X))	→	active(length(mark(X)))	(18)
active(inf(X))	→	mark(cons(X,inf(s(X))))	(4)
mark(cons(X1,X2))	→	active(cons(X1,X2))	(15)
active(length(cons(X,L)))	→	mark(s(length(L)))	(8)
active(eq(0,0))	→	mark(true)	(1)
active(eq(X,Y))	→	mark(false)	(3)
mark(take(X1,X2))	→	active(take(mark(X1),mark(X2)))	(16)
eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
mark(nil)	→	active(nil)	(17)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
active(take(0,X))	→	mark(nil)	(5)
take(active(X1),X2)	→	take(X1,X2)	(33)
mark(0)	→	active(0)	(10)
active(length(nil))	→	mark(0)	(7)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
mark(inf(X))	→	active(inf(mark(X)))	(14)
take(mark(X1),X2)	→	take(X1,X2)	(31)
mark(s(X))	→	active(s(X))	(12)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
mark(true)	→	active(true)	(11)
mark(eq(X1,X2))	→	active(eq(X1,X2))	(9)
mark(false)	→	active(false)	(13)
active(take(s(X),cons(Y,L)))	→	mark(cons(Y,take(X,L)))	(6)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)
active(eq(s(X),s(Y)))	→	mark(eq(X,Y))	(2)

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

active^#(inf(X))	→	mark^#(cons(X,inf(s(X))))	(56)
mark^#(length(X))	→	mark^#(X)	(50)
mark^#(inf(X))	→	mark^#(X)	(74)
mark^#(take(X1,X2))	→	mark^#(X2)	(47)
active^#(take(s(X),cons(Y,L)))	→	mark^#(cons(Y,take(X,L)))	(68)
mark^#(take(X1,X2))	→	mark^#(X1)	(44)
active^#(length(cons(X,L)))	→	mark^#(s(length(L)))	(43)

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^#(length(X))	→	active^#(length(mark(X)))	(61)
mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(69)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(40)
mark^#(inf(X))	→	active^#(inf(mark(X)))	(84)
mark^#(s(X))	→	active^#(s(X))	(51)
mark^#(eq(X1,X2))	→	active^#(eq(X1,X2))	(52)
active^#(eq(s(X),s(Y)))	→	mark^#(eq(X,Y))	(82)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	5398
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + 5399
[eq(x₁, x₂)]	=	5398
[false]	=	17728
[true]	=	8280
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[0]	=	29384
[s^#(x₁)]	=	0
[nil]	=	23984
[mark(x₁)]	=	x₁ + 33401
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 33401
[cons(x₁, x₂)]	=	x₁ + 5398
[active^#(x₁)]	=	5398
[length(x₁)]	=	x₁ + 5399
[length^#(x₁)]	=	0
[inf(x₁)]	=	5399

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

mark^#(length(X))	→	active^#(length(mark(X)))	(61)
mark^#(take(X1,X2))	→	active^#(take(mark(X1),mark(X2)))	(40)
mark^#(inf(X))	→	active^#(inf(mark(X)))	(84)

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

mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(69)
mark^#(s(X))	→	active^#(s(X))	(51)
mark^#(eq(X1,X2))	→	active^#(eq(X1,X2))	(52)
active^#(eq(s(X),s(Y)))	→	mark^#(eq(X,Y))	(82)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	4188
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	x₁ + 1
[eq(x₁, x₂)]	=	4187
[false]	=	4188
[true]	=	4188
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	31886
[s^#(x₁)]	=	0
[nil]	=	16913
[mark(x₁)]	=	x₁ + 56905
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 56905
[cons(x₁, x₂)]	=	x₁ + 4188
[active^#(x₁)]	=	5398
[length(x₁)]	=	x₁ + 14972
[length^#(x₁)]	=	0
[inf(x₁)]	=	5399

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

mark^#(cons(X1,X2))	→	active^#(cons(X1,X2))	(69)
mark^#(s(X))	→	active^#(s(X))	(51)

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

mark^#(eq(X1,X2))	→	active^#(eq(X1,X2))	(52)
active^#(eq(s(X),s(Y)))	→	mark^#(eq(X,Y))	(82)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	43950
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	2
[true]	=	98732
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	49365
[s^#(x₁)]	=	0
[nil]	=	43950
[mark(x₁)]	=	x₁ + 1
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 15620
[active^#(x₁)]	=	x₁ + 1210
[length(x₁)]	=	49364
[length^#(x₁)]	=	0
[inf(x₁)]	=	15620

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

mark^#(eq(X1,X2))	→	active^#(eq(X1,X2))	(52)
active^#(eq(s(X),s(Y)))	→	mark^#(eq(X,Y))	(82)

could be deleted.

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

take^#(X1,mark(X2))	→	take^#(X1,X2)	(60)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(59)
take^#(active(X1),X2)	→	take^#(X1,X2)	(55)
take^#(X1,active(X2))	→	take^#(X1,X2)	(73)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	x₁ + x₂ + 0
[take(x₁, x₂)]	=	35082
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	2
[true]	=	52106
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	26052
[s^#(x₁)]	=	0
[nil]	=	35082
[mark(x₁)]	=	x₁ + 1
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 5969
[active^#(x₁)]	=	x₁ + 1210
[length(x₁)]	=	1
[length^#(x₁)]	=	0
[inf(x₁)]	=	5969

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

take^#(X1,mark(X2))	→	take^#(X1,X2)	(60)
take^#(mark(X1),X2)	→	take^#(X1,X2)	(59)
take^#(active(X1),X2)	→	take^#(X1,X2)	(55)
take^#(X1,active(X2))	→	take^#(X1,X2)	(73)

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

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(87)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(62)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(81)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(70)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	x₁ + x₂ + 0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	1
[eq(x₁, x₂)]	=	x₁ + x₂ + 55691
[false]	=	55692
[true]	=	208460
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	76384
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 1210
[length(x₁)]	=	44249
[length^#(x₁)]	=	0
[inf(x₁)]	=	436

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(87)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(62)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(81)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(70)

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

inf^#(active(X))	→	inf^#(X)	(75)
inf^#(mark(X))	→	inf^#(X)	(76)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	1
[eq(x₁, x₂)]	=	x₁ + x₂ + 4
[false]	=	5
[true]	=	12
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	3
[s^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 1
[inf^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 1210
[length(x₁)]	=	2
[length^#(x₁)]	=	0
[inf(x₁)]	=	15081

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

inf^#(active(X))	→	inf^#(X)	(75)
inf^#(mark(X))	→	inf^#(X)	(76)

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

s^#(mark(X))	→	s^#(X)	(57)
s^#(active(X))	→	s^#(X)	(53)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	11495
[eq(x₁, x₂)]	=	x₁ + x₂ + 35616
[false]	=	35617
[true]	=	93887
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	29135
[s^#(x₁)]	=	x₁ + 0
[nil]	=	5481
[mark(x₁)]	=	x₁ + 1
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 1
[active^#(x₁)]	=	x₁ + 1210
[length(x₁)]	=	1
[length^#(x₁)]	=	0
[inf(x₁)]	=	28652

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

s^#(mark(X))	→	s^#(X)	(57)
s^#(active(X))	→	s^#(X)	(53)

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

length^#(mark(X))	→	length^#(X)	(85)
length^#(active(X))	→	length^#(X)	(67)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	52787
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	2
[true]	=	39828
[eq^#(x₁, x₂)]	=	0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	19913
[s^#(x₁)]	=	0
[nil]	=	52787
[mark(x₁)]	=	x₁ + 1
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 20631
[active^#(x₁)]	=	x₁ + 1210
[length(x₁)]	=	19912
[length^#(x₁)]	=	x₁ + 0
[inf(x₁)]	=	20631

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

length^#(mark(X))	→	length^#(X)	(85)
length^#(active(X))	→	length^#(X)	(67)

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

eq^#(mark(X1),X2)	→	eq^#(X1,X2)	(58)
eq^#(X1,active(X2))	→	eq^#(X1,X2)	(77)
eq^#(active(X1),X2)	→	eq^#(X1,X2)	(72)
eq^#(X1,mark(X2))	→	eq^#(X1,X2)	(63)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	64373
[eq(x₁, x₂)]	=	x₁ + x₂ + 24552
[false]	=	44970
[true]	=	24557
[eq^#(x₁, x₂)]	=	x₂ + 0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	2
[s^#(x₁)]	=	0
[nil]	=	64373
[mark(x₁)]	=	x₁ + 1
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 38169
[active^#(x₁)]	=	x₁ + 1210
[length(x₁)]	=	1
[length^#(x₁)]	=	0
[inf(x₁)]	=	38169

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

eq^#(X1,active(X2))	→	eq^#(X1,X2)	(77)
eq^#(X1,mark(X2))	→	eq^#(X1,X2)	(63)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

eq^#(active(X1),X2)	→	eq^#(X1,X2)	(72)
eq^#(mark(X1),X2)	→	eq^#(X1,X2)	(58)

1.1.7.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[cons^#(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 15876
[take^#(x₁, x₂)]	=	0
[take(x₁, x₂)]	=	42490
[eq(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	2
[true]	=	24557
[eq^#(x₁, x₂)]	=	x₁ + 0
[mark^#(x₁)]	=	x₁ + 1211
[0]	=	2562
[s^#(x₁)]	=	0
[nil]	=	42490
[mark(x₁)]	=	x₁ + 1
[inf^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	x₁ + 42490
[active^#(x₁)]	=	x₁ + 1210
[length(x₁)]	=	1
[length^#(x₁)]	=	0
[inf(x₁)]	=	42490

together with the usable rules

eq(active(X1),X2)	→	eq(X1,X2)	(21)
length(active(X))	→	length(X)	(36)
inf(active(X))	→	inf(X)	(26)
eq(mark(X1),X2)	→	eq(X1,X2)	(19)
take(X1,mark(X2))	→	take(X1,X2)	(32)
cons(mark(X1),X2)	→	cons(X1,X2)	(27)
take(X1,active(X2))	→	take(X1,X2)	(34)
eq(X1,active(X2))	→	eq(X1,X2)	(22)
cons(X1,mark(X2))	→	cons(X1,X2)	(28)
take(active(X1),X2)	→	take(X1,X2)	(33)
eq(X1,mark(X2))	→	eq(X1,X2)	(20)
inf(mark(X))	→	inf(X)	(25)
cons(X1,active(X2))	→	cons(X1,X2)	(30)
take(mark(X1),X2)	→	take(X1,X2)	(31)
s(mark(X))	→	s(X)	(23)
s(active(X))	→	s(X)	(24)
length(mark(X))	→	length(X)	(35)
cons(active(X1),X2)	→	cons(X1,X2)	(29)

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

eq^#(active(X1),X2)	→	eq^#(X1,X2)	(72)
eq^#(mark(X1),X2)	→	eq^#(X1,X2)	(58)

could be deleted.

1.1.7.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.