Certification Problem

Input (TPDB TRS_Standard/Rubio_04/quick)

The rewrite relation of the following TRS is considered.

le(0,Y)	→	true	(1)
le(s(X),0)	→	false	(2)
le(s(X),s(Y))	→	le(X,Y)	(3)
app(nil,Y)	→	Y	(4)
app(cons(N,L),Y)	→	cons(N,app(L,Y))	(5)
low(N,nil)	→	nil	(6)
low(N,cons(M,L))	→	iflow(le(M,N),N,cons(M,L))	(7)
iflow(true,N,cons(M,L))	→	cons(M,low(N,L))	(8)
iflow(false,N,cons(M,L))	→	low(N,L)	(9)
high(N,nil)	→	nil	(10)
high(N,cons(M,L))	→	ifhigh(le(M,N),N,cons(M,L))	(11)
ifhigh(true,N,cons(M,L))	→	high(N,L)	(12)
ifhigh(false,N,cons(M,L))	→	cons(M,high(N,L))	(13)
quicksort(nil)	→	nil	(14)
quicksort(cons(N,L))	→	app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))	(15)

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.

iflow^#(false,N,cons(M,L))	→	low^#(N,L)	(16)
low^#(N,cons(M,L))	→	iflow^#(le(M,N),N,cons(M,L))	(17)
quicksort^#(cons(N,L))	→	low^#(N,L)	(18)
le^#(s(X),s(Y))	→	le^#(X,Y)	(19)
quicksort^#(cons(N,L))	→	app^#(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))	(20)
quicksort^#(cons(N,L))	→	quicksort^#(low(N,L))	(21)
quicksort^#(cons(N,L))	→	quicksort^#(high(N,L))	(22)
low^#(N,cons(M,L))	→	le^#(M,N)	(23)
iflow^#(true,N,cons(M,L))	→	low^#(N,L)	(24)
ifhigh^#(true,N,cons(M,L))	→	high^#(N,L)	(25)
high^#(N,cons(M,L))	→	ifhigh^#(le(M,N),N,cons(M,L))	(26)
ifhigh^#(false,N,cons(M,L))	→	high^#(N,L)	(27)
app^#(cons(N,L),Y)	→	app^#(L,Y)	(28)
quicksort^#(cons(N,L))	→	high^#(N,L)	(29)
high^#(N,cons(M,L))	→	le^#(M,N)	(30)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

quicksort^#(cons(N,L))	→	quicksort^#(high(N,L))	(22)
quicksort^#(cons(N,L))	→	quicksort^#(low(N,L))	(21)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 1
[s(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[quicksort^#(x₁)]	=	x₁ + 0
[high^#(x₁, x₂)]	=	0
[false]	=	3
[quicksort(x₁)]	=	0
[true]	=	2
[iflow^#(x₁, x₂, x₃)]	=	0
[0]	=	1
[high(x₁, x₂)]	=	x₂ + 1
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₂ + 1
[iflow(x₁, x₂, x₃)]	=	x₃ + 1
[ifhigh(x₁, x₂, x₃)]	=	x₃ + 1
[cons(x₁, x₂)]	=	x₂ + 2
[ifhigh^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

together with the usable rules

iflow(true,N,cons(M,L))	→	cons(M,low(N,L))	(8)
high(N,nil)	→	nil	(10)
low(N,cons(M,L))	→	iflow(le(M,N),N,cons(M,L))	(7)
ifhigh(true,N,cons(M,L))	→	high(N,L)	(12)
high(N,cons(M,L))	→	ifhigh(le(M,N),N,cons(M,L))	(11)
iflow(false,N,cons(M,L))	→	low(N,L)	(9)
ifhigh(false,N,cons(M,L))	→	cons(M,high(N,L))	(13)
low(N,nil)	→	nil	(6)

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

quicksort^#(cons(N,L))	→	quicksort^#(high(N,L))	(22)
quicksort^#(cons(N,L))	→	quicksort^#(low(N,L))	(21)

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

app^#(cons(N,L),Y)

→

app^#(L,Y)

(28)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 1
[s(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[quicksort^#(x₁)]	=	x₁ + 0
[high^#(x₁, x₂)]	=	0
[false]	=	17653
[quicksort(x₁)]	=	0
[true]	=	2
[iflow^#(x₁, x₂, x₃)]	=	0
[0]	=	17651
[high(x₁, x₂)]	=	x₂ + 38978
[nil]	=	1
[app^#(x₁, x₂)]	=	x₁ + 0
[low(x₁, x₂)]	=	x₂ + 42736
[iflow(x₁, x₂, x₃)]	=	x₃ + 42736
[ifhigh(x₁, x₂, x₃)]	=	x₃ + 38978
[cons(x₁, x₂)]	=	x₂ + 2
[ifhigh^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

together with the usable rules

iflow(true,N,cons(M,L))	→	cons(M,low(N,L))	(8)
high(N,nil)	→	nil	(10)
low(N,cons(M,L))	→	iflow(le(M,N),N,cons(M,L))	(7)
ifhigh(true,N,cons(M,L))	→	high(N,L)	(12)
high(N,cons(M,L))	→	ifhigh(le(M,N),N,cons(M,L))	(11)
iflow(false,N,cons(M,L))	→	low(N,L)	(9)
ifhigh(false,N,cons(M,L))	→	cons(M,high(N,L))	(13)
low(N,nil)	→	nil	(6)

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

app^#(cons(N,L),Y)

→

app^#(L,Y)

(28)

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

ifhigh^#(false,N,cons(M,L))	→	high^#(N,L)	(27)
high^#(N,cons(M,L))	→	ifhigh^#(le(M,N),N,cons(M,L))	(26)
ifhigh^#(true,N,cons(M,L))	→	high^#(N,L)	(25)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 1
[s(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[quicksort^#(x₁)]	=	0
[high^#(x₁, x₂)]	=	x₂ + 1
[false]	=	1
[quicksort(x₁)]	=	0
[true]	=	1
[iflow^#(x₁, x₂, x₃)]	=	0
[0]	=	50736
[high(x₁, x₂)]	=	x₂ + 11049
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₂ + 31122
[iflow(x₁, x₂, x₃)]	=	x₃ + 31122
[ifhigh(x₁, x₂, x₃)]	=	x₃ + 11049
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[ifhigh^#(x₁, x₂, x₃)]	=	x₃ + 0
[low^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

together with the usable rules

iflow(true,N,cons(M,L))	→	cons(M,low(N,L))	(8)
le(0,Y)	→	true	(1)
le(s(X),s(Y))	→	le(X,Y)	(3)
high(N,nil)	→	nil	(10)
low(N,cons(M,L))	→	iflow(le(M,N),N,cons(M,L))	(7)
iflow(false,N,cons(M,L))	→	low(N,L)	(9)
low(N,nil)	→	nil	(6)
le(s(X),0)	→	false	(2)

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

ifhigh^#(false,N,cons(M,L))	→	high^#(N,L)	(27)
high^#(N,cons(M,L))	→	ifhigh^#(le(M,N),N,cons(M,L))	(26)
ifhigh^#(true,N,cons(M,L))	→	high^#(N,L)	(25)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

low^#(N,cons(M,L))	→	iflow^#(le(M,N),N,cons(M,L))	(17)
iflow^#(true,N,cons(M,L))	→	low^#(N,L)	(24)
iflow^#(false,N,cons(M,L))	→	low^#(N,L)	(16)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 1
[s(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[quicksort^#(x₁)]	=	0
[high^#(x₁, x₂)]	=	1
[false]	=	1
[quicksort(x₁)]	=	0
[true]	=	1
[iflow^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[0]	=	50736
[high(x₁, x₂)]	=	x₂ + 11049
[nil]	=	35495
[app^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₂ + 3
[iflow(x₁, x₂, x₃)]	=	x₃ + 3
[ifhigh(x₁, x₂, x₃)]	=	x₃ + 11049
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[ifhigh^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	x₁ + x₂ + 1
[app(x₁, x₂)]	=	0

together with the usable rules

iflow(true,N,cons(M,L))	→	cons(M,low(N,L))	(8)
le(0,Y)	→	true	(1)
le(s(X),s(Y))	→	le(X,Y)	(3)
high(N,nil)	→	nil	(10)
low(N,cons(M,L))	→	iflow(le(M,N),N,cons(M,L))	(7)
iflow(false,N,cons(M,L))	→	low(N,L)	(9)
low(N,nil)	→	nil	(6)
le(s(X),0)	→	false	(2)

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

low^#(N,cons(M,L))	→	iflow^#(le(M,N),N,cons(M,L))	(17)
iflow^#(true,N,cons(M,L))	→	low^#(N,L)	(24)
iflow^#(false,N,cons(M,L))	→	low^#(N,L)	(16)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

le^#(s(X),s(Y))

→

le^#(X,Y)

(19)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₂ + 1
[s(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	x₁ + 0
[quicksort^#(x₁)]	=	0
[high^#(x₁, x₂)]	=	1
[false]	=	25075
[quicksort(x₁)]	=	0
[true]	=	1
[iflow^#(x₁, x₂, x₃)]	=	0
[0]	=	25074
[high(x₁, x₂)]	=	x₂ + 11049
[nil]	=	35495
[app^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₂ + 3
[iflow(x₁, x₂, x₃)]	=	x₃ + 3
[ifhigh(x₁, x₂, x₃)]	=	x₃ + 11049
[cons(x₁, x₂)]	=	x₁ + x₂ + 2
[ifhigh^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	1
[app(x₁, x₂)]	=	0

together with the usable rules

iflow(true,N,cons(M,L))	→	cons(M,low(N,L))	(8)
le(0,Y)	→	true	(1)
le(s(X),s(Y))	→	le(X,Y)	(3)
high(N,nil)	→	nil	(10)
low(N,cons(M,L))	→	iflow(le(M,N),N,cons(M,L))	(7)
iflow(false,N,cons(M,L))	→	low(N,L)	(9)
low(N,nil)	→	nil	(6)
le(s(X),0)	→	false	(2)

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

le^#(s(X),s(Y))

→

le^#(X,Y)

(19)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.