Certification Problem

Input (TPDB TRS_Standard/SK90/4.60)

The rewrite relation of the following TRS is considered.

msort(nil)	→	nil	(1)
msort(.(x,y))	→	.(min(x,y),msort(del(min(x,y),.(x,y))))	(2)
min(x,nil)	→	x	(3)
min(x,.(y,z))	→	if(<=(x,y),min(x,z),min(y,z))	(4)
del(x,nil)	→	nil	(5)
del(x,.(y,z))	→	if(=(x,y),z,.(y,del(x,z)))	(6)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

msort^#(.(x,y))	→	del^#(min(x,y),.(x,y))	(7)
msort^#(.(x,y))	→	msort^#(del(min(x,y),.(x,y)))	(8)
msort^#(.(x,y))	→	min^#(x,y)	(9)
min^#(x,.(y,z))	→	min^#(y,z)	(10)
min^#(x,.(y,z))	→	min^#(x,z)	(11)
del^#(x,.(y,z))	→	del^#(x,z)	(12)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair
del^#(x,.(y,z)) → del^#(x,z) (12)

1.1.1 Size-Change Termination

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

del^#(x,.(y,z)) → del^#(x,z) (12)

2 > 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 2^nd component contains the pair

min^#(x,.(y,z)) → min^#(y,z) (10)

min^#(x,.(y,z)) → min^#(x,z) (11)

1.1.2 Size-Change Termination

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

min^#(x,.(y,z)) → min^#(y,z) (10)

2 > 2

2 > 1

min^#(x,.(y,z)) → min^#(x,z) (11)

2 > 2

1 ≥ 1

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