Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_2_Luc02c_Z)

The rewrite relation of the following TRS is considered.

2nd(cons(X,n__cons(Y,Z)))	→	activate(Y)	(1)
from(X)	→	cons(X,n__from(s(X)))	(2)
cons(X1,X2)	→	n__cons(X1,X2)	(3)
from(X)	→	n__from(X)	(4)
activate(n__cons(X1,X2))	→	cons(X1,X2)	(5)
activate(n__from(X))	→	from(X)	(6)
activate(X)	→	X	(7)

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.

activate^#(n__from(X))	→	from^#(X)	(8)
activate^#(n__cons(X1,X2))	→	cons^#(X1,X2)	(9)
from^#(X)	→	cons^#(X,n__from(s(X)))	(10)
2nd^#(cons(X,n__cons(Y,Z)))	→	activate^#(Y)	(11)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.