Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex9_BLR02_C)

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)
active(filter(X1,X2,X3))	→	filter(active(X1),X2,X3)	(7)
active(filter(X1,X2,X3))	→	filter(X1,active(X2),X3)	(8)
active(filter(X1,X2,X3))	→	filter(X1,X2,active(X3))	(9)
active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
active(s(X))	→	s(active(X))	(11)
active(sieve(X))	→	sieve(active(X))	(12)
active(nats(X))	→	nats(active(X))	(13)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
s(mark(X))	→	mark(s(X))	(18)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(mark(X))	→	mark(nats(X))	(20)
proper(filter(X1,X2,X3))	→	filter(proper(X1),proper(X2),proper(X3))	(21)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(22)
proper(0)	→	ok(0)	(23)
proper(s(X))	→	s(proper(X))	(24)
proper(sieve(X))	→	sieve(proper(X))	(25)
proper(nats(X))	→	nats(proper(X))	(26)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)
s(ok(X))	→	ok(s(X))	(30)
sieve(ok(X))	→	ok(sieve(X))	(31)
nats(ok(X))	→	ok(nats(X))	(32)
top(mark(X))	→	top(proper(X))	(33)
top(ok(X))	→	top(active(X))	(34)

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

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))	(75)
top^#(ok(X))	→	top^#(active(X))	(42)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	51912
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	x₁ + 15261
[filter^#(x₁, x₂, x₃)]	=	0
[top(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	x₁ + 0
[ok(x₁)]	=	x₁ + 0
[0]	=	0
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[sieve(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[nats(x₁)]	=	x₁ + 21388
[active(x₁)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₁ + 21387
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[sieve^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
active(filter(X1,X2,X3))	→	filter(X1,active(X2),X3)	(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))	→	mark(filter(X1,X2,X3))	(16)
proper(filter(X1,X2,X3))	→	filter(proper(X1),proper(X2),proper(X3))	(21)
proper(nats(X))	→	nats(proper(X))	(26)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(22)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
active(filter(X1,X2,X3))	→	filter(active(X1),X2,X3)	(7)
nats(mark(X))	→	mark(nats(X))	(20)
proper(sieve(X))	→	sieve(proper(X))	(25)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
active(sieve(X))	→	sieve(active(X))	(12)
proper(0)	→	ok(0)	(23)
proper(s(X))	→	s(proper(X))	(24)
active(s(X))	→	s(active(X))	(11)
active(filter(X1,X2,X3))	→	filter(X1,X2,active(X3))	(9)
active(nats(X))	→	nats(active(X))	(13)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(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

top^#(mark(X))

→

top^#(proper(X))

(75)

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

(42)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	x₁ + 0
[filter^#(x₁, x₂, x₃)]	=	0
[top(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	18876
[ok(x₁)]	=	x₁ + 18875
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	0
[sieve(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[nats(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 18874
[cons(x₁, x₂)]	=	x₁ + 0
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	x₂ + 0
[sieve^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
active(filter(X1,X2,X3))	→	filter(X1,active(X2),X3)	(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))	→	mark(filter(X1,X2,X3))	(16)
proper(filter(X1,X2,X3))	→	filter(proper(X1),proper(X2),proper(X3))	(21)
proper(nats(X))	→	nats(proper(X))	(26)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
proper(cons(X1,X2))	→	cons(proper(X1),proper(X2))	(22)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
active(cons(X1,X2))	→	cons(active(X1),X2)	(10)
active(filter(X1,X2,X3))	→	filter(active(X1),X2,X3)	(7)
nats(mark(X))	→	mark(nats(X))	(20)
proper(sieve(X))	→	sieve(proper(X))	(25)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
active(sieve(X))	→	sieve(active(X))	(12)
proper(0)	→	ok(0)	(23)
proper(s(X))	→	s(proper(X))	(24)
active(s(X))	→	s(active(X))	(11)
active(filter(X1,X2,X3))	→	filter(X1,X2,active(X3))	(9)
active(nats(X))	→	nats(active(X))	(13)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(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

top^#(ok(X))

→

top^#(active(X))

(42)

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^#(filter(X1,X2,X3))	→	active^#(X1)	(67)
active^#(filter(X1,X2,X3))	→	active^#(X2)	(88)
active^#(filter(X1,X2,X3))	→	active^#(X3)	(55)
active^#(nats(X))	→	active^#(X)	(54)
active^#(s(X))	→	active^#(X)	(53)
active^#(sieve(X))	→	active^#(X)	(79)
active^#(cons(X1,X2))	→	active^#(X1)	(78)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[filter^#(x₁, x₂, x₃)]	=	0
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	18876
[ok(x₁)]	=	x₁ + 8375
[0]	=	9643
[s^#(x₁)]	=	0
[mark(x₁)]	=	0
[sieve(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	40828
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	x₁ + 0
[filter(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[sieve^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
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))	→	mark(filter(X1,X2,X3))	(16)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
nats(mark(X))	→	mark(nats(X))	(20)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
proper(0)	→	ok(0)	(23)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(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

active^#(filter(X1,X2,X3))	→	active^#(X1)	(67)
active^#(filter(X1,X2,X3))	→	active^#(X2)	(88)
active^#(filter(X1,X2,X3))	→	active^#(X3)	(55)
active^#(nats(X))	→	active^#(X)	(54)
active^#(s(X))	→	active^#(X)	(53)
active^#(sieve(X))	→	active^#(X)	(79)
active^#(cons(X1,X2))	→	active^#(X1)	(78)

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

proper^#(s(X))	→	proper^#(X)	(90)
proper^#(filter(X1,X2,X3))	→	proper^#(X1)	(59)
proper^#(cons(X1,X2))	→	proper^#(X2)	(83)
proper^#(sieve(X))	→	proper^#(X)	(76)
proper^#(filter(X1,X2,X3))	→	proper^#(X3)	(43)
proper^#(filter(X1,X2,X3))	→	proper^#(X2)	(39)
proper^#(cons(X1,X2))	→	proper^#(X1)	(38)
proper^#(nats(X))	→	proper^#(X)	(36)

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₁)]	=	x₁ + 1
[filter^#(x₁, x₂, x₃)]	=	0
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	0
[sieve(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	x₁ + 0
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	1
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[sieve^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
active(sieve(cons(s(N),Y)))	→	mark(cons(s(N),sieve(filter(Y,N,N))))	(4)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
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))	→	mark(filter(X1,X2,X3))	(16)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
active(nats(N))	→	mark(cons(N,nats(s(N))))	(5)
nats(mark(X))	→	mark(nats(X))	(20)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
proper(0)	→	ok(0)	(23)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(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

proper^#(s(X))	→	proper^#(X)	(90)
proper^#(filter(X1,X2,X3))	→	proper^#(X1)	(59)
proper^#(cons(X1,X2))	→	proper^#(X2)	(83)
proper^#(sieve(X))	→	proper^#(X)	(76)
proper^#(filter(X1,X2,X3))	→	proper^#(X3)	(43)
proper^#(filter(X1,X2,X3))	→	proper^#(X2)	(39)
proper^#(cons(X1,X2))	→	proper^#(X1)	(38)
proper^#(nats(X))	→	proper^#(X)	(36)

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^#(ok(X))	→	sieve^#(X)	(93)
sieve^#(mark(X))	→	sieve^#(X)	(41)

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₁)]	=	x₁ + 1
[filter^#(x₁, x₂, x₃)]	=	0
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[sieve(x₁)]	=	x₁ + 1
[proper^#(x₁)]	=	0
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	6
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 1
[sieve^#(x₁)]	=	x₁ + 0

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
nats(mark(X))	→	mark(nats(X))	(20)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
proper(0)	→	ok(0)	(23)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)

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

sieve^#(ok(X))	→	sieve^#(X)	(93)
sieve^#(mark(X))	→	sieve^#(X)	(41)

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^#(ok(X1),ok(X2))	→	cons^#(X1,X2)	(86)
cons^#(mark(X1),X2)	→	cons^#(X1,X2)	(70)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
nats(mark(X))	→	mark(nats(X))	(20)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
proper(0)	→	ok(0)	(23)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)

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

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

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

nats^#(mark(X))	→	nats^#(X)	(58)
nats^#(ok(X))	→	nats^#(X)	(51)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
nats(mark(X))	→	mark(nats(X))	(20)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
proper(0)	→	ok(0)	(23)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)

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

nats^#(mark(X))	→	nats^#(X)	(58)
nats^#(ok(X))	→	nats^#(X)	(51)

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

filter^#(mark(X1),X2,X3)	→	filter^#(X1,X2,X3)	(81)
filter^#(X1,mark(X2),X3)	→	filter^#(X1,X2,X3)	(50)
filter^#(X1,X2,mark(X3))	→	filter^#(X1,X2,X3)	(45)
filter^#(ok(X1),ok(X2),ok(X3))	→	filter^#(X1,X2,X3)	(72)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
nats(mark(X))	→	mark(nats(X))	(20)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
proper(0)	→	ok(0)	(23)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)

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

filter^#(mark(X1),X2,X3)	→	filter^#(X1,X2,X3)	(81)
filter^#(X1,mark(X2),X3)	→	filter^#(X1,X2,X3)	(50)
filter^#(ok(X1),ok(X2),ok(X3))	→	filter^#(X1,X2,X3)	(72)

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

filter^#(X1,X2,mark(X3))

→

filter^#(X1,X2,X3)

(45)

1.1.7.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zprimes]	=	1
[cons^#(x₁, x₂)]	=	0
[nats^#(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[filter^#(x₁, x₂, x₃)]	=	x₃ + 0
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[proper(x₁)]	=	2
[ok(x₁)]	=	x₁ + 1
[0]	=	1
[s^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 1
[sieve(x₁)]	=	x₁ + 30249
[proper^#(x₁)]	=	0
[nats(x₁)]	=	x₁ + 1
[active(x₁)]	=	62410
[cons(x₁, x₂)]	=	x₁ + x₂ + 1
[active^#(x₁)]	=	0
[filter(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 32158
[sieve^#(x₁)]	=	0

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
nats(mark(X))	→	mark(nats(X))	(20)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
proper(0)	→	ok(0)	(23)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)

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

filter^#(X1,X2,mark(X3))

→

filter^#(X1,X2,X3)

(45)

could be deleted.

1.1.7.1.1.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)	(68)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

s(mark(X))	→	mark(s(X))	(18)
filter(X1,mark(X2),X3)	→	mark(filter(X1,X2,X3))	(15)
filter(X1,X2,mark(X3))	→	mark(filter(X1,X2,X3))	(16)
sieve(mark(X))	→	mark(sieve(X))	(19)
nats(ok(X))	→	ok(nats(X))	(32)
cons(mark(X1),X2)	→	mark(cons(X1,X2))	(17)
proper(zprimes)	→	ok(zprimes)	(27)
filter(ok(X1),ok(X2),ok(X3))	→	ok(filter(X1,X2,X3))	(28)
nats(mark(X))	→	mark(nats(X))	(20)
s(ok(X))	→	ok(s(X))	(30)
filter(mark(X1),X2,X3)	→	mark(filter(X1,X2,X3))	(14)
sieve(ok(X))	→	ok(sieve(X))	(31)
proper(0)	→	ok(0)	(23)
active(zprimes)	→	mark(sieve(nats(s(s(0)))))	(6)
cons(ok(X1),ok(X2))	→	ok(cons(X1,X2))	(29)

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

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

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.