Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex7_BLR02_Z)

The rewrite relation of the following TRS is considered.

from(X)	→	cons(X,n__from(s(X)))	(1)
head(cons(X,XS))	→	X	(2)
2nd(cons(X,XS))	→	head(activate(XS))	(3)
take(0,XS)	→	nil	(4)
take(s(N),cons(X,XS))	→	cons(X,n__take(N,activate(XS)))	(5)
sel(0,cons(X,XS))	→	X	(6)
sel(s(N),cons(X,XS))	→	sel(N,activate(XS))	(7)
from(X)	→	n__from(X)	(8)
take(X1,X2)	→	n__take(X1,X2)	(9)
activate(n__from(X))	→	from(X)	(10)
activate(n__take(X1,X2))	→	take(X1,X2)	(11)
activate(X)	→	X	(12)

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.

sel^#(s(N),cons(X,XS))	→	sel^#(N,activate(XS))	(13)
2nd^#(cons(X,XS))	→	head^#(activate(XS))	(14)
2nd^#(cons(X,XS))	→	activate^#(XS)	(15)
take^#(s(N),cons(X,XS))	→	activate^#(XS)	(16)
sel^#(s(N),cons(X,XS))	→	activate^#(XS)	(17)
activate^#(n__take(X1,X2))	→	take^#(X1,X2)	(18)
activate^#(n__from(X))	→	from^#(X)	(19)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

sel^#(s(N),cons(X,XS))

→

sel^#(N,activate(XS))

(13)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	0
[activate(x₁)]	=	x₁ + 1
[take(x₁, x₂)]	=	x₁ + x₂ + 38978
[n__from(x₁)]	=	19306
[activate^#(x₁)]	=	0
[2nd(x₁)]	=	0
[head^#(x₁)]	=	0
[0]	=	44083
[n__take(x₁, x₂)]	=	x₁ + x₂ + 38978
[sel^#(x₁, x₂)]	=	x₁ + x₂ + 0
[from(x₁)]	=	19307
[sel(x₁, x₂)]	=	0
[nil]	=	0
[2nd^#(x₁)]	=	0
[from^#(x₁)]	=	0
[head(x₁)]	=	0
[cons(x₁, x₂)]	=	x₂ + 1

together with the usable rules

take(0,XS)	→	nil	(4)
from(X)	→	n__from(X)	(8)
from(X)	→	cons(X,n__from(s(X)))	(1)
take(s(N),cons(X,XS))	→	cons(X,n__take(N,activate(XS)))	(5)
activate(n__from(X))	→	from(X)	(10)
activate(X)	→	X	(12)
activate(n__take(X1,X2))	→	take(X1,X2)	(11)
take(X1,X2)	→	n__take(X1,X2)	(9)

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

sel^#(s(N),cons(X,XS))

→

sel^#(N,activate(XS))

(13)

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

activate^#(n__take(X1,X2))	→	take^#(X1,X2)	(18)
take^#(s(N),cons(X,XS))	→	activate^#(XS)	(16)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[take^#(x₁, x₂)]	=	x₁ + x₂ + 0
[activate(x₁)]	=	x₁ + 18919
[take(x₁, x₂)]	=	x₁ + x₂ + 18919
[n__from(x₁)]	=	35231
[activate^#(x₁)]	=	x₁ + 0
[2nd(x₁)]	=	0
[head^#(x₁)]	=	0
[0]	=	44083
[n__take(x₁, x₂)]	=	x₁ + x₂ + 1
[sel^#(x₁, x₂)]	=	x₂ + 0
[from(x₁)]	=	54150
[sel(x₁, x₂)]	=	0
[nil]	=	0
[2nd^#(x₁)]	=	0
[from^#(x₁)]	=	0
[head(x₁)]	=	0
[cons(x₁, x₂)]	=	x₂ + 18919

together with the usable rules

take(0,XS)	→	nil	(4)
from(X)	→	n__from(X)	(8)
from(X)	→	cons(X,n__from(s(X)))	(1)
take(s(N),cons(X,XS))	→	cons(X,n__take(N,activate(XS)))	(5)
activate(n__from(X))	→	from(X)	(10)
activate(X)	→	X	(12)
activate(n__take(X1,X2))	→	take(X1,X2)	(11)
take(X1,X2)	→	n__take(X1,X2)	(9)

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

activate^#(n__take(X1,X2))	→	take^#(X1,X2)	(18)
take^#(s(N),cons(X,XS))	→	activate^#(XS)	(16)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.