Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex2_Luc03b_Z)

The rewrite relation of the following TRS is considered.

fst(0,Z)	→	nil	(1)
fst(s(X),cons(Y,Z))	→	cons(Y,n__fst(activate(X),activate(Z)))	(2)
from(X)	→	cons(X,n__from(s(X)))	(3)
add(0,X)	→	X	(4)
add(s(X),Y)	→	s(n__add(activate(X),Y))	(5)
len(nil)	→	0	(6)
len(cons(X,Z))	→	s(n__len(activate(Z)))	(7)
fst(X1,X2)	→	n__fst(X1,X2)	(8)
from(X)	→	n__from(X)	(9)
add(X1,X2)	→	n__add(X1,X2)	(10)
len(X)	→	n__len(X)	(11)
activate(n__fst(X1,X2))	→	fst(X1,X2)	(12)
activate(n__from(X))	→	from(X)	(13)
activate(n__add(X1,X2))	→	add(X1,X2)	(14)
activate(n__len(X))	→	len(X)	(15)
activate(X)	→	X	(16)

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.

fst^#(s(X),cons(Y,Z))	→	activate^#(Z)	(17)
len^#(cons(X,Z))	→	activate^#(Z)	(18)
add^#(s(X),Y)	→	activate^#(X)	(19)
activate^#(n__add(X1,X2))	→	add^#(X1,X2)	(20)
activate^#(n__from(X))	→	from^#(X)	(21)
fst^#(s(X),cons(Y,Z))	→	activate^#(X)	(22)
activate^#(n__len(X))	→	len^#(X)	(23)
activate^#(n__fst(X1,X2))	→	fst^#(X1,X2)	(24)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

activate^#(n__fst(X1,X2))	→	fst^#(X1,X2)	(24)
activate^#(n__len(X))	→	len^#(X)	(23)
fst^#(s(X),cons(Y,Z))	→	activate^#(X)	(22)
len^#(cons(X,Z))	→	activate^#(Z)	(18)
activate^#(n__add(X1,X2))	→	add^#(X1,X2)	(20)
add^#(s(X),Y)	→	activate^#(X)	(19)
fst^#(s(X),cons(Y,Z))	→	activate^#(Z)	(17)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[len^#(x₁)]	=	x₁ + 2941
[s(x₁)]	=	x₁ + 1
[activate(x₁)]	=	0
[n__from(x₁)]	=	0
[fst(x₁, x₂)]	=	0
[activate^#(x₁)]	=	x₁ + 0
[n__add(x₁, x₂)]	=	x₁ + 1
[fst^#(x₁, x₂)]	=	x₁ + x₂ + 2437
[0]	=	0
[from(x₁)]	=	0
[nil]	=	0
[n__len(x₁)]	=	x₁ + 2942
[n__fst(x₁, x₂)]	=	x₁ + x₂ + 2438
[from^#(x₁)]	=	0
[cons(x₁, x₂)]	=	x₂ + 5915
[add^#(x₁, x₂)]	=	x₁ + 0
[add(x₁, x₂)]	=	0
[len(x₁)]	=	0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

activate^#(n__fst(X1,X2))	→	fst^#(X1,X2)	(24)
activate^#(n__len(X))	→	len^#(X)	(23)
fst^#(s(X),cons(Y,Z))	→	activate^#(X)	(22)
len^#(cons(X,Z))	→	activate^#(Z)	(18)
activate^#(n__add(X1,X2))	→	add^#(X1,X2)	(20)
add^#(s(X),Y)	→	activate^#(X)	(19)
fst^#(s(X),cons(Y,Z))	→	activate^#(Z)	(17)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.