Certification Problem

Input (TPDB TRS_Standard/Mixed_TRS/hydra)

The rewrite relation of the following TRS is considered.

f(cons(nil,y))	→	y	(1)
f(cons(f(cons(nil,y)),z))	→	copy(n,y,z)	(2)
copy(0,y,z)	→	f(z)	(3)
copy(s(x),y,z)	→	copy(x,y,cons(f(y),z))	(4)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

f^#(cons(f(cons(nil,y)),z))	→	copy^#(n,y,z)	(5)
copy^#(0,y,z)	→	f^#(z)	(6)
copy^#(s(x),y,z)	→	copy^#(x,y,cons(f(y),z))	(7)
copy^#(s(x),y,z)	→	f^#(y)	(8)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair
copy^#(s(x),y,z) → copy^#(x,y,cons(f(y),z)) (7)

1.1.1 Size-Change Termination

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

copy^#(s(x),y,z) → copy^#(x,y,cons(f(y),z)) (7)

1 > 1

2 ≥ 2

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