Certification Problem

Input (TPDB TRS_Standard/SK90/4.29)

The rewrite relation of the following TRS is considered.

merge(x,nil)	→	x	(1)
merge(nil,y)	→	y	(2)
merge(++(x,y),++(u,v))	→	++(x,merge(y,++(u,v)))	(3)
merge(++(x,y),++(u,v))	→	++(u,merge(++(x,y),v))	(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.

merge^#(++(x,y),++(u,v))	→	merge^#(++(x,y),v)	(5)
merge^#(++(x,y),++(u,v))	→	merge^#(y,++(u,v))	(6)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair
merge^#(++(x,y),++(u,v)) → merge^#(y,++(u,v)) (6)

1.1.1 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation

[merge(x₁, x₂)] = 0

[v] = 0

[u] = 0

[++(x₁, x₂)] = x₂ + 1

[merge^#(x₁, x₂)] = x₁ + 0

[nil] = 0

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pair
merge^#(++(x,y),++(u,v)) → merge^#(y,++(u,v)) (6)
could be deleted.
1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.