Certification Problem

Input (TPDB TRS_Standard/SK90/4.59)

The rewrite relation of the following TRS is considered.

qsort(nil)	→	nil	(1)
qsort(.(x,y))	→	++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y))))	(2)
lowers(x,nil)	→	nil	(3)
lowers(x,.(y,z))	→	if(<=(y,x),.(y,lowers(x,z)),lowers(x,z))	(4)
greaters(x,nil)	→	nil	(5)
greaters(x,.(y,z))	→	if(<=(y,x),greaters(x,z),.(y,greaters(x,z)))	(6)

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.

qsort^#(.(x,y))	→	lowers^#(x,y)	(7)
greaters^#(x,.(y,z))	→	greaters^#(x,z)	(8)
lowers^#(x,.(y,z))	→	lowers^#(x,z)	(9)
greaters^#(x,.(y,z))	→	greaters^#(x,z)	(8)
qsort^#(.(x,y))	→	qsort^#(greaters(x,y))	(10)
qsort^#(.(x,y))	→	qsort^#(lowers(x,y))	(11)
lowers^#(x,.(y,z))	→	lowers^#(x,z)	(9)
qsort^#(.(x,y))	→	greaters^#(x,y)	(12)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

qsort^#(.(x,y))	→	qsort^#(lowers(x,y))	(11)
qsort^#(.(x,y))	→	qsort^#(greaters(x,y))	(10)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[lowers(x₁, x₂)]	=	x₂ + 1
[greaters(x₁, x₂)]	=	x₂ + 1
[<=(x₁, x₂)]	=	1
[++(x₁, x₂)]	=	0
[qsort(x₁)]	=	0
[qsort^#(x₁)]	=	x₁ + 0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[lowers^#(x₁, x₂)]	=	0
[nil]	=	1
[greaters^#(x₁, x₂)]	=	0
[.(x₁, x₂)]	=	x₂ + 2

together with the usable rules

lowers(x,.(y,z))	→	if(<=(y,x),.(y,lowers(x,z)),lowers(x,z))	(4)
lowers(x,nil)	→	nil	(3)
greaters(x,nil)	→	nil	(5)
greaters(x,.(y,z))	→	if(<=(y,x),greaters(x,z),.(y,greaters(x,z)))	(6)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

qsort^#(.(x,y))	→	qsort^#(lowers(x,y))	(11)
qsort^#(.(x,y))	→	qsort^#(greaters(x,y))	(10)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

greaters^#(x,.(y,z))	→	greaters^#(x,z)	(8)
greaters^#(x,.(y,z))	→	greaters^#(x,z)	(8)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[lowers(x₁, x₂)]	=	x₂ + 1
[greaters(x₁, x₂)]	=	x₂ + 40651
[<=(x₁, x₂)]	=	1
[++(x₁, x₂)]	=	0
[qsort(x₁)]	=	0
[qsort^#(x₁)]	=	x₁ + 0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[lowers^#(x₁, x₂)]	=	0
[nil]	=	1
[greaters^#(x₁, x₂)]	=	x₂ + 0
[.(x₁, x₂)]	=	x₂ + 1

together with the usable rules

lowers(x,.(y,z))	→	if(<=(y,x),.(y,lowers(x,z)),lowers(x,z))	(4)
lowers(x,nil)	→	nil	(3)
greaters(x,nil)	→	nil	(5)
greaters(x,.(y,z))	→	if(<=(y,x),greaters(x,z),.(y,greaters(x,z)))	(6)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

greaters^#(x,.(y,z))	→	greaters^#(x,z)	(8)
greaters^#(x,.(y,z))	→	greaters^#(x,z)	(8)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

lowers^#(x,.(y,z))	→	lowers^#(x,z)	(9)
lowers^#(x,.(y,z))	→	lowers^#(x,z)	(9)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[lowers(x₁, x₂)]	=	x₂ + 1
[greaters(x₁, x₂)]	=	x₂ + 1424
[<=(x₁, x₂)]	=	1
[++(x₁, x₂)]	=	0
[qsort(x₁)]	=	0
[qsort^#(x₁)]	=	x₁ + 0
[if(x₁, x₂, x₃)]	=	x₂ + 0
[lowers^#(x₁, x₂)]	=	x₂ + 0
[nil]	=	1
[greaters^#(x₁, x₂)]	=	0
[.(x₁, x₂)]	=	x₂ + 1

together with the usable rules

lowers(x,.(y,z))	→	if(<=(y,x),.(y,lowers(x,z)),lowers(x,z))	(4)
lowers(x,nil)	→	nil	(3)
greaters(x,nil)	→	nil	(5)
greaters(x,.(y,z))	→	if(<=(y,x),greaters(x,z),.(y,greaters(x,z)))	(6)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

lowers^#(x,.(y,z))	→	lowers^#(x,z)	(9)
lowers^#(x,.(y,z))	→	lowers^#(x,z)	(9)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.