Certification Problem

Input (TPDB TRS_Standard/AG01/#3.55)

The rewrite relation of the following TRS is considered.

minus(x,0)	→	x	(1)
minus(s(x),s(y))	→	minus(x,y)	(2)
quot(0,s(y))	→	0	(3)
quot(s(x),s(y))	→	s(quot(minus(x,y),s(y)))	(4)
le(0,y)	→	true	(5)
le(s(x),0)	→	false	(6)
le(s(x),s(y))	→	le(x,y)	(7)
app(nil,y)	→	y	(8)
app(add(n,x),y)	→	add(n,app(x,y))	(9)
low(n,nil)	→	nil	(10)
low(n,add(m,x))	→	if_low(le(m,n),n,add(m,x))	(11)
if_low(true,n,add(m,x))	→	add(m,low(n,x))	(12)
if_low(false,n,add(m,x))	→	low(n,x)	(13)
high(n,nil)	→	nil	(14)
high(n,add(m,x))	→	if_high(le(m,n),n,add(m,x))	(15)
if_high(true,n,add(m,x))	→	high(n,x)	(16)
if_high(false,n,add(m,x))	→	add(m,high(n,x))	(17)
quicksort(nil)	→	nil	(18)
quicksort(add(n,x))	→	app(quicksort(low(n,x)),add(n,quicksort(high(n,x))))	(19)

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.

if_low^#(false,n,add(m,x))	→	low^#(n,x)	(20)
if_low^#(true,n,add(m,x))	→	low^#(n,x)	(21)
quicksort^#(add(n,x))	→	high^#(n,x)	(22)
quicksort^#(add(n,x))	→	app^#(quicksort(low(n,x)),add(n,quicksort(high(n,x))))	(23)
quicksort^#(add(n,x))	→	low^#(n,x)	(24)
quicksort^#(add(n,x))	→	quicksort^#(high(n,x))	(25)
if_high^#(true,n,add(m,x))	→	high^#(n,x)	(26)
le^#(s(x),s(y))	→	le^#(x,y)	(27)
quicksort^#(add(n,x))	→	quicksort^#(low(n,x))	(28)
low^#(n,add(m,x))	→	le^#(m,n)	(29)
quot^#(s(x),s(y))	→	quot^#(minus(x,y),s(y))	(30)
high^#(n,add(m,x))	→	le^#(m,n)	(31)
app^#(add(n,x),y)	→	app^#(x,y)	(32)
minus^#(s(x),s(y))	→	minus^#(x,y)	(33)
if_high^#(false,n,add(m,x))	→	high^#(n,x)	(34)
high^#(n,add(m,x))	→	if_high^#(le(m,n),n,add(m,x))	(35)
low^#(n,add(m,x))	→	if_low^#(le(m,n),n,add(m,x))	(36)
quot^#(s(x),s(y))	→	minus^#(x,y)	(37)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

quot^#(s(x),s(y))

→

quot^#(minus(x,y),s(y))

(30)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 2
[le^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[if_high(x₁, x₂, x₃)]	=	0
[quicksort^#(x₁)]	=	0
[high^#(x₁, x₂)]	=	0
[false]	=	0
[if_high^#(x₁, x₂, x₃)]	=	0
[quicksort(x₁)]	=	0
[true]	=	0
[0]	=	1
[quot(x₁, x₂)]	=	0
[high(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[quot^#(x₁, x₂)]	=	x₁ + 0
[if_low(x₁, x₂, x₃)]	=	0
[if_low^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

together with the usable rules

minus(x,0)	→	x	(1)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

quot^#(s(x),s(y))

→

quot^#(minus(x,y),s(y))

(30)

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

minus^#(s(x),s(y))

→

minus^#(x,y)

(33)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[s(x₁)]	=	x₁ + 2
[le^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[if_high(x₁, x₂, x₃)]	=	0
[quicksort^#(x₁)]	=	0
[high^#(x₁, x₂)]	=	0
[false]	=	0
[if_high^#(x₁, x₂, x₃)]	=	0
[quicksort(x₁)]	=	0
[true]	=	0
[0]	=	1
[quot(x₁, x₂)]	=	0
[high(x₁, x₂)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[low(x₁, x₂)]	=	0
[add(x₁, x₂)]	=	0
[quot^#(x₁, x₂)]	=	x₁ + 0
[if_low(x₁, x₂, x₃)]	=	0
[if_low^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

together with the usable rules

minus(x,0)	→	x	(1)
minus(s(x),s(y))	→	minus(x,y)	(2)

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

minus^#(s(x),s(y))

→

minus^#(x,y)

(33)

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

quicksort^#(add(n,x))	→	quicksort^#(high(n,x))	(25)
quicksort^#(add(n,x))	→	quicksort^#(low(n,x))	(28)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	2
[le^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[if_high(x₁, x₂, x₃)]	=	x₂ + x₃ + 38551
[quicksort^#(x₁)]	=	x₁ + 0
[high^#(x₁, x₂)]	=	0
[false]	=	5
[if_high^#(x₁, x₂, x₃)]	=	0
[quicksort(x₁)]	=	0
[true]	=	3
[0]	=	1
[quot(x₁, x₂)]	=	0
[high(x₁, x₂)]	=	x₁ + x₂ + 38551
[nil]	=	31755
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₁ + x₂ + 282
[add(x₁, x₂)]	=	x₁ + x₂ + 38552
[quot^#(x₁, x₂)]	=	0
[if_low(x₁, x₂, x₃)]	=	x₂ + x₃ + 282
[if_low^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

together with the usable rules

high(n,add(m,x))	→	if_high(le(m,n),n,add(m,x))	(15)
minus(x,0)	→	x	(1)
if_high(true,n,add(m,x))	→	high(n,x)	(16)
if_high(false,n,add(m,x))	→	add(m,high(n,x))	(17)
low(n,nil)	→	nil	(10)
high(n,nil)	→	nil	(14)
if_low(true,n,add(m,x))	→	add(m,low(n,x))	(12)
low(n,add(m,x))	→	if_low(le(m,n),n,add(m,x))	(11)
if_low(false,n,add(m,x))	→	low(n,x)	(13)

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

quicksort^#(add(n,x))	→	quicksort^#(high(n,x))	(25)
quicksort^#(add(n,x))	→	quicksort^#(low(n,x))	(28)

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

app^#(add(n,x),y)

→

app^#(x,y)

(32)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 1
[s(x₁)]	=	2
[le^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[if_high(x₁, x₂, x₃)]	=	x₂ + x₃ + 38551
[quicksort^#(x₁)]	=	x₁ + 0
[high^#(x₁, x₂)]	=	0
[false]	=	5
[if_high^#(x₁, x₂, x₃)]	=	0
[quicksort(x₁)]	=	0
[true]	=	3
[0]	=	1
[quot(x₁, x₂)]	=	0
[high(x₁, x₂)]	=	x₁ + x₂ + 38551
[nil]	=	53547
[app^#(x₁, x₂)]	=	x₁ + 0
[minus^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₁ + x₂ + 1
[add(x₁, x₂)]	=	x₁ + x₂ + 38552
[quot^#(x₁, x₂)]	=	0
[if_low(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[if_low^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

together with the usable rules

high(n,add(m,x))	→	if_high(le(m,n),n,add(m,x))	(15)
minus(x,0)	→	x	(1)
if_high(true,n,add(m,x))	→	high(n,x)	(16)
if_high(false,n,add(m,x))	→	add(m,high(n,x))	(17)
low(n,nil)	→	nil	(10)
high(n,nil)	→	nil	(14)
if_low(true,n,add(m,x))	→	add(m,low(n,x))	(12)
low(n,add(m,x))	→	if_low(le(m,n),n,add(m,x))	(11)
if_low(false,n,add(m,x))	→	low(n,x)	(13)

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

app^#(add(n,x),y)

→

app^#(x,y)

(32)

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

if_high^#(true,n,add(m,x))	→	high^#(n,x)	(26)
high^#(n,add(m,x))	→	if_high^#(le(m,n),n,add(m,x))	(35)
if_high^#(false,n,add(m,x))	→	high^#(n,x)	(34)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	1324
[s(x₁)]	=	0
[le^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[if_high(x₁, x₂, x₃)]	=	x₂ + x₃ + 38607
[quicksort^#(x₁)]	=	x₁ + 0
[high^#(x₁, x₂)]	=	x₁ + x₂ + 1325
[false]	=	1324
[if_high^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[quicksort(x₁)]	=	0
[true]	=	1324
[0]	=	0
[quot(x₁, x₂)]	=	0
[high(x₁, x₂)]	=	x₁ + x₂ + 38607
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₁ + x₂ + 34519
[add(x₁, x₂)]	=	x₂ + 2
[quot^#(x₁, x₂)]	=	0
[if_low(x₁, x₂, x₃)]	=	x₂ + x₃ + 34519
[if_low^#(x₁, x₂, x₃)]	=	0
[low^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

together with the usable rules

high(n,add(m,x))	→	if_high(le(m,n),n,add(m,x))	(15)
minus(x,0)	→	x	(1)
if_high(true,n,add(m,x))	→	high(n,x)	(16)
if_high(false,n,add(m,x))	→	add(m,high(n,x))	(17)
le(0,y)	→	true	(5)
low(n,nil)	→	nil	(10)
le(s(x),s(y))	→	le(x,y)	(7)
high(n,nil)	→	nil	(14)
if_low(true,n,add(m,x))	→	add(m,low(n,x))	(12)
low(n,add(m,x))	→	if_low(le(m,n),n,add(m,x))	(11)
if_low(false,n,add(m,x))	→	low(n,x)	(13)
le(s(x),0)	→	false	(6)

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

if_high^#(true,n,add(m,x))	→	high^#(n,x)	(26)
high^#(n,add(m,x))	→	if_high^#(le(m,n),n,add(m,x))	(35)
if_high^#(false,n,add(m,x))	→	high^#(n,x)	(34)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

low^#(n,add(m,x))	→	if_low^#(le(m,n),n,add(m,x))	(36)
if_low^#(true,n,add(m,x))	→	low^#(n,x)	(21)
if_low^#(false,n,add(m,x))	→	low^#(n,x)	(20)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	23612
[s(x₁)]	=	0
[le^#(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	x₁ + 1
[if_high(x₁, x₂, x₃)]	=	x₂ + x₃ + 25074
[quicksort^#(x₁)]	=	x₁ + 0
[high^#(x₁, x₂)]	=	1325
[false]	=	23612
[if_high^#(x₁, x₂, x₃)]	=	x₁ + 0
[quicksort(x₁)]	=	0
[true]	=	23612
[0]	=	0
[quot(x₁, x₂)]	=	0
[high(x₁, x₂)]	=	x₁ + x₂ + 25074
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₁ + x₂ + 1
[add(x₁, x₂)]	=	x₂ + 2
[quot^#(x₁, x₂)]	=	0
[if_low(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[if_low^#(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[low^#(x₁, x₂)]	=	x₁ + x₂ + 23613
[app(x₁, x₂)]	=	0

together with the usable rules

high(n,add(m,x))	→	if_high(le(m,n),n,add(m,x))	(15)
minus(x,0)	→	x	(1)
if_high(true,n,add(m,x))	→	high(n,x)	(16)
if_high(false,n,add(m,x))	→	add(m,high(n,x))	(17)
le(0,y)	→	true	(5)
low(n,nil)	→	nil	(10)
le(s(x),s(y))	→	le(x,y)	(7)
high(n,nil)	→	nil	(14)
if_low(true,n,add(m,x))	→	add(m,low(n,x))	(12)
low(n,add(m,x))	→	if_low(le(m,n),n,add(m,x))	(11)
if_low(false,n,add(m,x))	→	low(n,x)	(13)
le(s(x),0)	→	false	(6)

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

low^#(n,add(m,x))	→	if_low^#(le(m,n),n,add(m,x))	(36)
if_low^#(true,n,add(m,x))	→	low^#(n,x)	(21)
if_low^#(false,n,add(m,x))	→	low^#(n,x)	(20)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

le^#(s(x),s(y))

→

le^#(x,y)

(27)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	23612
[s(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	x₂ + 0
[minus(x₁, x₂)]	=	x₁ + 1
[if_high(x₁, x₂, x₃)]	=	x₂ + x₃ + 40436
[quicksort^#(x₁)]	=	x₁ + 0
[high^#(x₁, x₂)]	=	1325
[false]	=	1
[if_high^#(x₁, x₂, x₃)]	=	x₁ + 0
[quicksort(x₁)]	=	0
[true]	=	23612
[0]	=	0
[quot(x₁, x₂)]	=	0
[high(x₁, x₂)]	=	x₁ + x₂ + 40436
[nil]	=	48999
[app^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[low(x₁, x₂)]	=	x₁ + x₂ + 1
[add(x₁, x₂)]	=	x₂ + 52182
[quot^#(x₁, x₂)]	=	0
[if_low(x₁, x₂, x₃)]	=	x₂ + x₃ + 1
[if_low^#(x₁, x₂, x₃)]	=	x₁ + 0
[low^#(x₁, x₂)]	=	23613
[app(x₁, x₂)]	=	0

together with the usable rules

high(n,add(m,x))	→	if_high(le(m,n),n,add(m,x))	(15)
minus(x,0)	→	x	(1)
if_high(true,n,add(m,x))	→	high(n,x)	(16)
if_high(false,n,add(m,x))	→	add(m,high(n,x))	(17)
le(0,y)	→	true	(5)
low(n,nil)	→	nil	(10)
le(s(x),s(y))	→	le(x,y)	(7)
high(n,nil)	→	nil	(14)
if_low(true,n,add(m,x))	→	add(m,low(n,x))	(12)
low(n,add(m,x))	→	if_low(le(m,n),n,add(m,x))	(11)
if_low(false,n,add(m,x))	→	low(n,x)	(13)
le(s(x),0)	→	false	(6)

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

le^#(s(x),s(y))

→

le^#(x,y)

(27)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.