Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex9_BLR02_GM)

The rewrite relation of the following TRS is considered.

a__filter(cons(X,Y),0,M)	→	cons(0,filter(Y,M,M))	(1)
a__filter(cons(X,Y),s(N),M)	→	cons(mark(X),filter(Y,N,M))	(2)
a__sieve(cons(0,Y))	→	cons(0,sieve(Y))	(3)
a__sieve(cons(s(N),Y))	→	cons(s(mark(N)),sieve(filter(Y,N,N)))	(4)
a__nats(N)	→	cons(mark(N),nats(s(N)))	(5)
a__zprimes	→	a__sieve(a__nats(s(s(0))))	(6)
mark(filter(X1,X2,X3))	→	a__filter(mark(X1),mark(X2),mark(X3))	(7)
mark(sieve(X))	→	a__sieve(mark(X))	(8)
mark(nats(X))	→	a__nats(mark(X))	(9)
mark(zprimes)	→	a__zprimes	(10)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(11)
mark(0)	→	0	(12)
mark(s(X))	→	s(mark(X))	(13)
a__filter(X1,X2,X3)	→	filter(X1,X2,X3)	(14)
a__sieve(X)	→	sieve(X)	(15)
a__nats(X)	→	nats(X)	(16)
a__zprimes	→	zprimes	(17)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

a__filter^#(cons(X,Y),s(N),M)	→	mark^#(X)	(18)
a__sieve^#(cons(s(N),Y))	→	mark^#(N)	(19)
a__nats^#(N)	→	mark^#(N)	(20)
a__zprimes^#	→	a__nats^#(s(s(0)))	(21)
a__zprimes^#	→	a__sieve^#(a__nats(s(s(0))))	(22)
mark^#(filter(X1,X2,X3))	→	mark^#(X3)	(23)
mark^#(filter(X1,X2,X3))	→	mark^#(X2)	(24)
mark^#(filter(X1,X2,X3))	→	mark^#(X1)	(25)
mark^#(filter(X1,X2,X3))	→	a__filter^#(mark(X1),mark(X2),mark(X3))	(26)
mark^#(sieve(X))	→	mark^#(X)	(27)
mark^#(sieve(X))	→	a__sieve^#(mark(X))	(28)
mark^#(nats(X))	→	mark^#(X)	(29)
mark^#(nats(X))	→	a__nats^#(mark(X))	(30)
mark^#(zprimes)	→	a__zprimes^#	(31)
mark^#(cons(X1,X2))	→	mark^#(X1)	(32)
mark^#(s(X))	→	mark^#(X)	(33)

1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[s(x₁)]	=	0 · x₁ + 0
[a__nats^#(x₁)]	=	0 · x₁ + 0
[a__nats(x₁)]	=	0 · x₁ + 0
[0]	=	0
[filter(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[a__zprimes^#]	=	0
[mark(x₁)]	=	0 · x₁ + 0
[a__zprimes]	=	2
[cons(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[sieve(x₁)]	=	0 · x₁ + 0
[a__sieve^#(x₁)]	=	0 · x₁ + 0
[a__filter^#(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[zprimes]	=	2
[nats(x₁)]	=	0 · x₁ + -∞
[mark^#(x₁)]	=	0 · x₁ + 0
[a__sieve(x₁)]	=	0 · x₁ + 0
[a__filter(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0

together with the usable rules

a__filter(cons(X,Y),0,M)	→	cons(0,filter(Y,M,M))	(1)
a__filter(cons(X,Y),s(N),M)	→	cons(mark(X),filter(Y,N,M))	(2)
a__sieve(cons(0,Y))	→	cons(0,sieve(Y))	(3)
a__sieve(cons(s(N),Y))	→	cons(s(mark(N)),sieve(filter(Y,N,N)))	(4)
a__nats(N)	→	cons(mark(N),nats(s(N)))	(5)
a__zprimes	→	a__sieve(a__nats(s(s(0))))	(6)
mark(filter(X1,X2,X3))	→	a__filter(mark(X1),mark(X2),mark(X3))	(7)
mark(sieve(X))	→	a__sieve(mark(X))	(8)
mark(nats(X))	→	a__nats(mark(X))	(9)
mark(zprimes)	→	a__zprimes	(10)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(11)
mark(0)	→	0	(12)
mark(s(X))	→	s(mark(X))	(13)
a__filter(X1,X2,X3)	→	filter(X1,X2,X3)	(14)
a__sieve(X)	→	sieve(X)	(15)
a__nats(X)	→	nats(X)	(16)
a__zprimes	→	zprimes	(17)

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

mark^#(zprimes)

→

a__zprimes^#

(31)

could be deleted.

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__nats^#(N)	→	mark^#(N)	(20)
mark^#(filter(X1,X2,X3))	→	mark^#(X3)	(23)
mark^#(filter(X1,X2,X3))	→	mark^#(X2)	(24)
mark^#(filter(X1,X2,X3))	→	mark^#(X1)	(25)
mark^#(filter(X1,X2,X3))	→	a__filter^#(mark(X1),mark(X2),mark(X3))	(26)
a__filter^#(cons(X,Y),s(N),M)	→	mark^#(X)	(18)
mark^#(sieve(X))	→	mark^#(X)	(27)
mark^#(sieve(X))	→	a__sieve^#(mark(X))	(28)
a__sieve^#(cons(s(N),Y))	→	mark^#(N)	(19)
mark^#(nats(X))	→	mark^#(X)	(29)
mark^#(nats(X))	→	a__nats^#(mark(X))	(30)
mark^#(cons(X1,X2))	→	mark^#(X1)	(32)
mark^#(s(X))	→	mark^#(X)	(33)

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[s(x₁)]	=	0 · x₁ + 0
[a__nats^#(x₁)]	=	2 · x₁ + 2
[a__nats(x₁)]	=	0 · x₁ + 0
[0]	=	0
[filter(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[mark(x₁)]	=	0 · x₁ + 0
[a__zprimes]	=	4
[cons(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[sieve(x₁)]	=	2 · x₁ + 2
[a__sieve^#(x₁)]	=	3 · x₁ + 0
[a__filter^#(x₁, x₂, x₃)]	=	2 · x₁ + 2 · x₂ + 2 · x₃ + 0
[zprimes]	=	4
[nats(x₁)]	=	0 · x₁ + -∞
[mark^#(x₁)]	=	2 · x₁ + 2
[a__sieve(x₁)]	=	2 · x₁ + 2
[a__filter(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0

together with the usable rules

a__filter(cons(X,Y),0,M)	→	cons(0,filter(Y,M,M))	(1)
a__filter(cons(X,Y),s(N),M)	→	cons(mark(X),filter(Y,N,M))	(2)
a__sieve(cons(0,Y))	→	cons(0,sieve(Y))	(3)
a__sieve(cons(s(N),Y))	→	cons(s(mark(N)),sieve(filter(Y,N,N)))	(4)
a__nats(N)	→	cons(mark(N),nats(s(N)))	(5)
a__zprimes	→	a__sieve(a__nats(s(s(0))))	(6)
mark(filter(X1,X2,X3))	→	a__filter(mark(X1),mark(X2),mark(X3))	(7)
mark(sieve(X))	→	a__sieve(mark(X))	(8)
mark(nats(X))	→	a__nats(mark(X))	(9)
mark(zprimes)	→	a__zprimes	(10)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(11)
mark(0)	→	0	(12)
mark(s(X))	→	s(mark(X))	(13)
a__filter(X1,X2,X3)	→	filter(X1,X2,X3)	(14)
a__sieve(X)	→	sieve(X)	(15)
a__nats(X)	→	nats(X)	(16)
a__zprimes	→	zprimes	(17)

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

mark^#(sieve(X))	→	mark^#(X)	(27)
mark^#(sieve(X))	→	a__sieve^#(mark(X))	(28)
a__sieve^#(cons(s(N),Y))	→	mark^#(N)	(19)

could be deleted.

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[s(x₁)]	=	0 · x₁ + 0
[a__nats^#(x₁)]	=	0 · x₁ + 0
[a__nats(x₁)]	=	1 · x₁ + 1
[0]	=	0
[filter(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0
[mark(x₁)]	=	0 · x₁ + 0
[a__zprimes]	=	1
[cons(x₁, x₂)]	=	0 · x₁ + 0 · x₂ + -∞
[sieve(x₁)]	=	0 · x₁ + 0
[a__filter^#(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + -∞
[zprimes]	=	1
[nats(x₁)]	=	1 · x₁ + 1
[mark^#(x₁)]	=	0 · x₁ + 0
[a__sieve(x₁)]	=	0 · x₁ + 0
[a__filter(x₁, x₂, x₃)]	=	0 · x₁ + 0 · x₂ + 0 · x₃ + 0

together with the usable rules

a__filter(cons(X,Y),0,M)	→	cons(0,filter(Y,M,M))	(1)
a__filter(cons(X,Y),s(N),M)	→	cons(mark(X),filter(Y,N,M))	(2)
a__sieve(cons(0,Y))	→	cons(0,sieve(Y))	(3)
a__sieve(cons(s(N),Y))	→	cons(s(mark(N)),sieve(filter(Y,N,N)))	(4)
a__nats(N)	→	cons(mark(N),nats(s(N)))	(5)
a__zprimes	→	a__sieve(a__nats(s(s(0))))	(6)
mark(filter(X1,X2,X3))	→	a__filter(mark(X1),mark(X2),mark(X3))	(7)
mark(sieve(X))	→	a__sieve(mark(X))	(8)
mark(nats(X))	→	a__nats(mark(X))	(9)
mark(zprimes)	→	a__zprimes	(10)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(11)
mark(0)	→	0	(12)
mark(s(X))	→	s(mark(X))	(13)
a__filter(X1,X2,X3)	→	filter(X1,X2,X3)	(14)
a__sieve(X)	→	sieve(X)	(15)
a__nats(X)	→	nats(X)	(16)
a__zprimes	→	zprimes	(17)

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

mark^#(nats(X))	→	mark^#(X)	(29)
mark^#(nats(X))	→	a__nats^#(mark(X))	(30)

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^#(filter(X1,X2,X3))	→	mark^#(X3)	(23)
mark^#(filter(X1,X2,X3))	→	mark^#(X2)	(24)
mark^#(filter(X1,X2,X3))	→	mark^#(X1)	(25)
mark^#(filter(X1,X2,X3))	→	a__filter^#(mark(X1),mark(X2),mark(X3))	(26)
a__filter^#(cons(X,Y),s(N),M)	→	mark^#(X)	(18)
mark^#(cons(X1,X2))	→	mark^#(X1)	(32)
mark^#(s(X))	→	mark^#(X)	(33)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the arctic semiring over the integers

[s(x₁)]	=	0 · x₁ + 0
[a__nats(x₁)]	=	5 · x₁ + 0
[0]	=	2
[filter(x₁, x₂, x₃)]	=	2 · x₁ + 0 · x₂ + 0 · x₃ + -∞
[mark(x₁)]	=	0 · x₁ + -∞
[a__zprimes]	=	7
[cons(x₁, x₂)]	=	0 · x₁ + -∞ · x₂ + 0
[sieve(x₁)]	=	0 · x₁ + 6
[a__filter^#(x₁, x₂, x₃)]	=	0 · x₁ + -∞ · x₂ + -∞ · x₃ + -∞
[zprimes]	=	7
[nats(x₁)]	=	5 · x₁ + 0
[mark^#(x₁)]	=	0 · x₁ + 0
[a__sieve(x₁)]	=	0 · x₁ + 6
[a__filter(x₁, x₂, x₃)]	=	2 · x₁ + 0 · x₂ + 0 · x₃ + -∞

together with the usable rules

a__filter(cons(X,Y),0,M)	→	cons(0,filter(Y,M,M))	(1)
a__filter(cons(X,Y),s(N),M)	→	cons(mark(X),filter(Y,N,M))	(2)
a__sieve(cons(0,Y))	→	cons(0,sieve(Y))	(3)
a__sieve(cons(s(N),Y))	→	cons(s(mark(N)),sieve(filter(Y,N,N)))	(4)
a__nats(N)	→	cons(mark(N),nats(s(N)))	(5)
a__zprimes	→	a__sieve(a__nats(s(s(0))))	(6)
mark(filter(X1,X2,X3))	→	a__filter(mark(X1),mark(X2),mark(X3))	(7)
mark(sieve(X))	→	a__sieve(mark(X))	(8)
mark(nats(X))	→	a__nats(mark(X))	(9)
mark(zprimes)	→	a__zprimes	(10)
mark(cons(X1,X2))	→	cons(mark(X1),X2)	(11)
mark(0)	→	0	(12)
mark(s(X))	→	s(mark(X))	(13)
a__filter(X1,X2,X3)	→	filter(X1,X2,X3)	(14)
a__sieve(X)	→	sieve(X)	(15)
a__nats(X)	→	nats(X)	(16)
a__zprimes	→	zprimes	(17)

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

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

→

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

(26)

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^#(s(X))	→	mark^#(X)	(33)
mark^#(filter(X1,X2,X3))	→	mark^#(X3)	(23)
mark^#(filter(X1,X2,X3))	→	mark^#(X2)	(24)
mark^#(filter(X1,X2,X3))	→	mark^#(X1)	(25)
mark^#(cons(X1,X2))	→	mark^#(X1)	(32)

1.1.1.1.1.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

mark^#(s(X))	→	mark^#(X)	(33)

1	>	1
mark^#(filter(X1,X2,X3))	→	mark^#(X3)	(23)

1	>	1
mark^#(filter(X1,X2,X3))	→	mark^#(X2)	(24)

1	>	1
mark^#(filter(X1,X2,X3))	→	mark^#(X1)	(25)

1	>	1
mark^#(cons(X1,X2))	→	mark^#(X1)	(32)

1	>	1

As there is no critical graph in the transitive closure, there are no infinite chains.