Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex9_BLR02_iGM)

The rewrite relation of the following TRS is considered.

active(filter(cons(X,Y),0,M))	→	mark(cons(0,filter(Y,M,M)))	(1)
active(filter(cons(X,Y),s(N),M))	→	mark(cons(X,filter(Y,N,M)))	(2)
active(sieve(cons(0,Y)))	→	mark(cons(0,sieve(Y)))	(3)
active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
mark(filter(X1,X2,X3))	→	active(filter(mark(X1),mark(X2),mark(X3)))	(7)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(8)
mark(0)	→	active(0)	(9)
mark(s(X))	→	active(s(mark(X)))	(10)
mark(sieve(X))	→	active(sieve(mark(X)))	(11)
mark(nats(X))	→	active(nats(mark(X)))	(12)
mark(zprimes)	→	active(zprimes)	(13)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
cons(mark(X1),X2)	→	cons(X1,X2)	(20)
cons(X1,mark(X2))	→	cons(X1,X2)	(21)
cons(active(X1),X2)	→	cons(X1,X2)	(22)
cons(X1,active(X2))	→	cons(X1,X2)	(23)
s(mark(X))	→	s(X)	(24)
s(active(X))	→	s(X)	(25)
sieve(mark(X))	→	sieve(X)	(26)
sieve(active(X))	→	sieve(X)	(27)
nats(mark(X))	→	nats(X)	(28)
nats(active(X))	→	nats(X)	(29)

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^#(filter(cons(X,Y),s(N),M))	→	cons^#(X,filter(Y,N,M))	(30)
active^#(sieve(cons(0,Y)))	→	mark^#(cons(0,sieve(Y)))	(31)
mark^#(s(X))	→	s^#(mark(X))	(32)
nats^#(mark(X))	→	nats^#(X)	(33)
active^#(filter(cons(X,Y),0,M))	→	mark^#(cons(0,filter(Y,M,M)))	(34)
filter^#(X1,X2,mark(X3))	→	filter^#(X1,X2,X3)	(35)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(36)
sieve^#(active(X))	→	sieve^#(X)	(37)
active^#(filter(cons(X,Y),0,M))	→	cons^#(0,filter(Y,M,M))	(38)
active^#(sieve(cons(s(N),Y)))	→	mark^#(cons(s(N),sieve(filter(Y,N,N))))	(39)
active^#(filter(cons(X,Y),0,M))	→	filter^#(Y,M,M)	(40)
filter^#(active(X1),X2,X3)	→	filter^#(X1,X2,X3)	(41)
active^#(zprimes)	→	sieve^#(nats(s(s(0))))	(42)
active^#(sieve(cons(s(N),Y)))	→	sieve^#(filter(Y,N,N))	(43)
sieve^#(mark(X))	→	sieve^#(X)	(44)
mark^#(cons(X1,X2))	→	mark^#(X1)	(45)
mark^#(sieve(X))	→	sieve^#(mark(X))	(46)
active^#(zprimes)	→	s^#(0)	(47)
mark^#(0)	→	active^#(0)	(48)
filter^#(X1,active(X2),X3)	→	filter^#(X1,X2,X3)	(49)
mark^#(filter(X1,X2,X3))	→	filter^#(mark(X1),mark(X2),mark(X3))	(50)
mark^#(filter(X1,X2,X3))	→	active^#(filter(mark(X1),mark(X2),mark(X3)))	(51)
active^#(sieve(cons(0,Y)))	→	sieve^#(Y)	(52)
mark^#(sieve(X))	→	active^#(sieve(mark(X)))	(53)
active^#(nats(N))	→	mark^#(cons(N,nats(s(N))))	(54)
active^#(sieve(cons(s(N),Y)))	→	filter^#(Y,N,N)	(55)
mark^#(sieve(X))	→	mark^#(X)	(56)
mark^#(s(X))	→	mark^#(X)	(57)
filter^#(X1,mark(X2),X3)	→	filter^#(X1,X2,X3)	(58)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(59)
mark^#(filter(X1,X2,X3))	→	mark^#(X1)	(60)
filter^#(mark(X1),X2,X3)	→	filter^#(X1,X2,X3)	(61)
active^#(zprimes)	→	nats^#(s(s(0)))	(62)
filter^#(X1,X2,active(X3))	→	filter^#(X1,X2,X3)	(63)
mark^#(zprimes)	→	active^#(zprimes)	(64)
active^#(nats(N))	→	nats^#(s(N))	(65)
active^#(zprimes)	→	mark^#(sieve(nats(s(s(0)))))	(66)
active^#(sieve(cons(0,Y)))	→	cons^#(0,sieve(Y))	(67)
mark^#(s(X))	→	active^#(s(mark(X)))	(68)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(69)
active^#(nats(N))	→	s^#(N)	(70)
mark^#(filter(X1,X2,X3))	→	mark^#(X3)	(71)
mark^#(nats(X))	→	active^#(nats(mark(X)))	(72)
active^#(nats(N))	→	cons^#(N,nats(s(N)))	(73)
mark^#(nats(X))	→	mark^#(X)	(74)
mark^#(filter(X1,X2,X3))	→	mark^#(X2)	(75)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(76)
s^#(active(X))	→	s^#(X)	(77)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(78)
active^#(filter(cons(X,Y),s(N),M))	→	filter^#(Y,N,M)	(79)
active^#(filter(cons(X,Y),s(N),M))	→	mark^#(cons(X,filter(Y,N,M)))	(80)
active^#(sieve(cons(s(N),Y)))	→	cons^#(s(N),sieve(filter(Y,N,N)))	(81)
active^#(zprimes)	→	s^#(s(0))	(82)
s^#(mark(X))	→	s^#(X)	(83)
nats^#(active(X))	→	nats^#(X)	(84)
mark^#(cons(X1,X2))	→	cons^#(mark(X1),X2)	(85)
mark^#(nats(X))	→	nats^#(mark(X))	(86)

1.1 Dependency Graph Processor

The dependency pairs are split into 6 components.

The 1^st component contains the pair

mark^#(filter(X1,X2,X3))	→	mark^#(X1)	(60)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(59)
mark^#(s(X))	→	mark^#(X)	(57)
mark^#(sieve(X))	→	mark^#(X)	(56)
active^#(nats(N))	→	mark^#(cons(N,nats(s(N))))	(54)
mark^#(sieve(X))	→	active^#(sieve(mark(X)))	(53)
active^#(filter(cons(X,Y),s(N),M))	→	mark^#(cons(X,filter(Y,N,M)))	(80)
mark^#(filter(X1,X2,X3))	→	active^#(filter(mark(X1),mark(X2),mark(X3)))	(51)
mark^#(filter(X1,X2,X3))	→	mark^#(X2)	(75)
mark^#(cons(X1,X2))	→	mark^#(X1)	(45)
mark^#(nats(X))	→	mark^#(X)	(74)
mark^#(nats(X))	→	active^#(nats(mark(X)))	(72)
mark^#(filter(X1,X2,X3))	→	mark^#(X3)	(71)
active^#(sieve(cons(s(N),Y)))	→	mark^#(cons(s(N),sieve(filter(Y,N,N))))	(39)
mark^#(s(X))	→	active^#(s(mark(X)))	(68)
active^#(zprimes)	→	mark^#(sieve(nats(s(s(0)))))	(66)
mark^#(zprimes)	→	active^#(zprimes)	(64)
active^#(filter(cons(X,Y),0,M))	→	mark^#(cons(0,filter(Y,M,M)))	(34)
active^#(sieve(cons(0,Y)))	→	mark^#(cons(0,sieve(Y)))	(31)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	71737
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	x₁ + 1143
[filter^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	38551
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[sieve(x₁)]	=	x₁ + 283
[nats(x₁)]	=	x₁ + 30615
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + 30613
[active^#(x₁)]	=	x₁ + 0
[filter(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 5855
[sieve^#(x₁)]	=	0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(8)
active(filter(cons(X,Y),0,M))	→	mark(cons(0,filter(Y,M,M)))	(1)
active(sieve(cons(0,Y)))	→	mark(cons(0,sieve(Y)))	(3)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
cons(X1,mark(X2))	→	cons(X1,X2)	(21)
sieve(mark(X))	→	sieve(X)	(26)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
sieve(active(X))	→	sieve(X)	(27)
cons(active(X1),X2)	→	cons(X1,X2)	(22)
nats(mark(X))	→	nats(X)	(28)
active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
mark(s(X))	→	active(s(mark(X)))	(10)
mark(filter(X1,X2,X3))	→	active(filter(mark(X1),mark(X2),mark(X3)))	(7)
cons(mark(X1),X2)	→	cons(X1,X2)	(20)
s(active(X))	→	s(X)	(25)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)
mark(nats(X))	→	active(nats(mark(X)))	(12)
cons(X1,active(X2))	→	cons(X1,X2)	(23)
s(mark(X))	→	s(X)	(24)
mark(sieve(X))	→	active(sieve(mark(X)))	(11)
mark(0)	→	active(0)	(9)
mark(zprimes)	→	active(zprimes)	(13)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
nats(active(X))	→	nats(X)	(29)
active(filter(cons(X,Y),s(N),M))	→	mark(cons(X,filter(Y,N,M)))	(2)

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

mark^#(filter(X1,X2,X3))	→	mark^#(X1)	(60)
mark^#(cons(X1,X2))	→	active^#(cons(mark(X1),X2))	(59)
mark^#(s(X))	→	mark^#(X)	(57)
mark^#(sieve(X))	→	mark^#(X)	(56)
active^#(nats(N))	→	mark^#(cons(N,nats(s(N))))	(54)
mark^#(sieve(X))	→	active^#(sieve(mark(X)))	(53)
active^#(filter(cons(X,Y),s(N),M))	→	mark^#(cons(X,filter(Y,N,M)))	(80)
mark^#(filter(X1,X2,X3))	→	active^#(filter(mark(X1),mark(X2),mark(X3)))	(51)
mark^#(filter(X1,X2,X3))	→	mark^#(X2)	(75)
mark^#(cons(X1,X2))	→	mark^#(X1)	(45)
mark^#(nats(X))	→	mark^#(X)	(74)
mark^#(nats(X))	→	active^#(nats(mark(X)))	(72)
mark^#(filter(X1,X2,X3))	→	mark^#(X3)	(71)
active^#(sieve(cons(s(N),Y)))	→	mark^#(cons(s(N),sieve(filter(Y,N,N))))	(39)
mark^#(s(X))	→	active^#(s(mark(X)))	(68)
active^#(zprimes)	→	mark^#(sieve(nats(s(s(0)))))	(66)
mark^#(zprimes)	→	active^#(zprimes)	(64)
active^#(filter(cons(X,Y),0,M))	→	mark^#(cons(0,filter(Y,M,M)))	(34)
active^#(sieve(cons(0,Y)))	→	mark^#(cons(0,sieve(Y)))	(31)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

nats^#(active(X))	→	nats^#(X)	(84)
nats^#(mark(X))	→	nats^#(X)	(33)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	2451
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	x₁ + 0
[s(x₁)]	=	1
[filter^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[sieve(x₁)]	=	x₁ + 1
[nats(x₁)]	=	x₁ + 2448
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	x₁ + 0
[filter(x₁, x₂, x₃)]	=	x₂ + 1
[sieve^#(x₁)]	=	0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
mark(cons(X1,X2))	→	active(cons(mark(X1),X2))	(8)
active(filter(cons(X,Y),0,M))	→	mark(cons(0,filter(Y,M,M)))	(1)
active(sieve(cons(0,Y)))	→	mark(cons(0,sieve(Y)))	(3)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
cons(X1,mark(X2))	→	cons(X1,X2)	(21)
sieve(mark(X))	→	sieve(X)	(26)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
sieve(active(X))	→	sieve(X)	(27)
cons(active(X1),X2)	→	cons(X1,X2)	(22)
nats(mark(X))	→	nats(X)	(28)
active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
mark(s(X))	→	active(s(mark(X)))	(10)
mark(filter(X1,X2,X3))	→	active(filter(mark(X1),mark(X2),mark(X3)))	(7)
cons(mark(X1),X2)	→	cons(X1,X2)	(20)
s(active(X))	→	s(X)	(25)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)
mark(nats(X))	→	active(nats(mark(X)))	(12)
cons(X1,active(X2))	→	cons(X1,X2)	(23)
s(mark(X))	→	s(X)	(24)
mark(sieve(X))	→	active(sieve(mark(X)))	(11)
mark(0)	→	active(0)	(9)
mark(zprimes)	→	active(zprimes)	(13)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
nats(active(X))	→	nats(X)	(29)
active(filter(cons(X,Y),s(N),M))	→	mark(cons(X,filter(Y,N,M)))	(2)

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

nats^#(mark(X))

→

nats^#(X)

(33)

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

nats^#(active(X))

→

nats^#(X)

(84)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	x₁ + 0
[s(x₁)]	=	1
[filter^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	1
[0]	=	36251
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 2
[sieve(x₁)]	=	x₁ + 1
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	1
[sieve^#(x₁)]	=	0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)

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

nats^#(active(X))

→

nats^#(X)

(84)

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

s^#(mark(X))	→	s^#(X)	(83)
s^#(active(X))	→	s^#(X)	(77)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	1
[filter^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	1
[0]	=	17897
[s^#(x₁)]	=	x₁ + 0
[mark(x₁)]	=	x₁ + 2
[sieve(x₁)]	=	x₁ + 1
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	1
[sieve^#(x₁)]	=	0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)

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

s^#(mark(X))	→	s^#(X)	(83)
s^#(active(X))	→	s^#(X)	(77)

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

sieve^#(mark(X))	→	sieve^#(X)	(44)
sieve^#(active(X))	→	sieve^#(X)	(37)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	1
[filter^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	1
[0]	=	56247
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 2
[sieve(x₁)]	=	x₁ + 1
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	1
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	1
[sieve^#(x₁)]	=	x₁ + 0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)

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

sieve^#(mark(X))	→	sieve^#(X)	(44)
sieve^#(active(X))	→	sieve^#(X)	(37)

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

cons^#(X1,active(X2))	→	cons^#(X1,X2)	(78)
cons^#(active(X1),X2)	→	cons^#(X1,X2)	(76)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(69)
cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(36)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	23712
[cons^#(x₁, x₂)]	=	x₁ + 0
[nats^#(x₁)]	=	0
[s(x₁)]	=	1
[filter^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	1
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 2
[sieve(x₁)]	=	x₁ + 23086
[nats(x₁)]	=	x₁ + 625
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	39946
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	1
[sieve^#(x₁)]	=	0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)

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

cons^#(active(X1),X2)	→	cons^#(X1,X2)	(76)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(69)

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

cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(36)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(78)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	x₂ + 0
[nats^#(x₁)]	=	0
[s(x₁)]	=	47098
[filter^#(x₁, x₂, x₃)]	=	0
[mark^#(x₁)]	=	1
[0]	=	21734
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[sieve(x₁)]	=	x₁ + 1
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	2
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	1
[sieve^#(x₁)]	=	0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)

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

cons^#(X1,mark(X2))	→	cons^#(X1,X2)	(36)
cons^#(X1,active(X2))	→	cons^#(X1,X2)	(78)

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

filter^#(X1,mark(X2),X3)	→	filter^#(X1,X2,X3)	(58)
filter^#(X1,active(X2),X3)	→	filter^#(X1,X2,X3)	(49)
filter^#(active(X1),X2,X3)	→	filter^#(X1,X2,X3)	(41)
filter^#(X1,X2,mark(X3))	→	filter^#(X1,X2,X3)	(35)
filter^#(X1,X2,active(X3))	→	filter^#(X1,X2,X3)	(63)
filter^#(mark(X1),X2,X3)	→	filter^#(X1,X2,X3)	(61)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	33859
[filter^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[mark^#(x₁)]	=	1
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[sieve(x₁)]	=	x₁ + 5969
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	2
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	1
[sieve^#(x₁)]	=	0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)

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

filter^#(X1,mark(X2),X3)	→	filter^#(X1,X2,X3)	(58)
filter^#(X1,active(X2),X3)	→	filter^#(X1,X2,X3)	(49)
filter^#(X1,X2,mark(X3))	→	filter^#(X1,X2,X3)	(35)
filter^#(X1,X2,active(X3))	→	filter^#(X1,X2,X3)	(63)

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

filter^#(active(X1),X2,X3)	→	filter^#(X1,X2,X3)	(41)
filter^#(mark(X1),X2,X3)	→	filter^#(X1,X2,X3)	(61)

1.1.6.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	42224
[filter^#(x₁, x₂, x₃)]	=	x₁ + 0
[mark^#(x₁)]	=	1
[0]	=	436
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[sieve(x₁)]	=	x₁ + 11668
[nats(x₁)]	=	x₁ + 977
[active(x₁)]	=	x₁ + 1
[cons(x₁, x₂)]	=	29162
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	1
[sieve^#(x₁)]	=	0

together with the usable rules

filter(X1,active(X2),X3)	→	filter(X1,X2,X3)	(18)
filter(X1,mark(X2),X3)	→	filter(X1,X2,X3)	(15)
filter(X1,X2,mark(X3))	→	filter(X1,X2,X3)	(16)
filter(X1,X2,active(X3))	→	filter(X1,X2,X3)	(19)
filter(active(X1),X2,X3)	→	filter(X1,X2,X3)	(17)
filter(mark(X1),X2,X3)	→	filter(X1,X2,X3)	(14)

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

filter^#(active(X1),X2,X3)	→	filter^#(X1,X2,X3)	(41)
filter^#(mark(X1),X2,X3)	→	filter^#(X1,X2,X3)	(61)

could be deleted.

1.1.6.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.