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 NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

copy^#(0,y,z)	→	f^#(z)	(5)
copy^#(s(x),y,z)	→	copy^#(x,y,cons(f(y),z))	(6)
f^#(cons(f(cons(nil,y)),z))	→	copy^#(n,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))

(6)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 28959
[n]	=	28961
[copy^#(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[f(x₁)]	=	x₁ + 2
[0]	=	1
[nil]	=	1
[f^#(x₁)]	=	0
[cons(x₁, x₂)]	=	28958
[copy(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0

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

copy^#(s(x),y,z)

→

copy^#(x,y,cons(f(y),z))

(6)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.