Certification Problem

Input (TPDB TRS_Standard/AG01/#3.10)

The rewrite relation of the following TRS is considered.

eq(0,0)	→	true	(1)
eq(0,s(x))	→	false	(2)
eq(s(x),0)	→	false	(3)
eq(s(x),s(y))	→	eq(x,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)
min(add(n,nil))	→	n	(10)
min(add(n,add(m,x)))	→	if_min(le(n,m),add(n,add(m,x)))	(11)
if_min(true,add(n,add(m,x)))	→	min(add(n,x))	(12)
if_min(false,add(n,add(m,x)))	→	min(add(m,x))	(13)
rm(n,nil)	→	nil	(14)
rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
minsort(nil,nil)	→	nil	(18)
minsort(add(n,x),y)	→	if_minsort(eq(n,min(add(n,x))),add(n,x),y)	(19)
if_minsort(true,add(n,x),y)	→	add(n,minsort(app(rm(n,x),y),nil))	(20)
if_minsort(false,add(n,x),y)	→	minsort(x,add(n,y))	(21)

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.

app^#(add(n,x),y)	→	app^#(x,y)	(22)
if_minsort^#(true,add(n,x),y)	→	minsort^#(app(rm(n,x),y),nil)	(23)
minsort^#(add(n,x),y)	→	min^#(add(n,x))	(24)
le^#(s(x),s(y))	→	le^#(x,y)	(25)
minsort^#(add(n,x),y)	→	if_minsort^#(eq(n,min(add(n,x))),add(n,x),y)	(26)
minsort^#(add(n,x),y)	→	eq^#(n,min(add(n,x)))	(27)
if_minsort^#(false,add(n,x),y)	→	minsort^#(x,add(n,y))	(28)
if_minsort^#(true,add(n,x),y)	→	app^#(rm(n,x),y)	(29)
if_rm^#(false,n,add(m,x))	→	rm^#(n,x)	(30)
if_min^#(true,add(n,add(m,x)))	→	min^#(add(n,x))	(31)
rm^#(n,add(m,x))	→	eq^#(n,m)	(32)
rm^#(n,add(m,x))	→	if_rm^#(eq(n,m),n,add(m,x))	(33)
min^#(add(n,add(m,x)))	→	if_min^#(le(n,m),add(n,add(m,x)))	(34)
if_min^#(false,add(n,add(m,x)))	→	min^#(add(m,x))	(35)
if_minsort^#(true,add(n,x),y)	→	rm^#(n,x)	(36)
if_rm^#(true,n,add(m,x))	→	rm^#(n,x)	(37)
min^#(add(n,add(m,x)))	→	le^#(n,m)	(38)
eq^#(s(x),s(y))	→	eq^#(x,y)	(39)

1.1 Dependency Graph Processor

The dependency pairs are split into 6 components.

The 1^st component contains the pair

if_minsort^#(false,add(n,x),y)	→	minsort^#(x,add(n,y))	(28)
minsort^#(add(n,x),y)	→	if_minsort^#(eq(n,min(add(n,x))),add(n,x),y)	(26)
if_minsort^#(true,add(n,x),y)	→	minsort^#(app(rm(n,x),y),nil)	(23)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 1
[if_rm(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[s(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[if_rm^#(x₁, x₂, x₃)]	=	0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	25910
[false]	=	25910
[min^#(x₁)]	=	0
[true]	=	25910
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	47339
[app^#(x₁, x₂)]	=	0
[if_minsort^#(x₁, x₂, x₃)]	=	x₂ + x₃ + 3
[min(x₁)]	=	153629
[minsort^#(x₁, x₂)]	=	x₁ + x₂ + 3
[add(x₁, x₂)]	=	x₁ + x₂ + 76814
[if_min(x₁, x₂)]	=	x₂ + 0
[if_minsort(x₁, x₂, x₃)]	=	0
[minsort(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	x₂ + 25910
[rm^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 3564

together with the usable rules

eq(s(x),s(y))	→	eq(x,y)	(4)
rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
app(nil,y)	→	y	(8)
eq(0,0)	→	true	(1)
eq(s(x),0)	→	false	(3)
if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
rm(n,nil)	→	nil	(14)
app(add(n,x),y)	→	add(n,app(x,y))	(9)
eq(0,s(x))	→	false	(2)

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

if_minsort^#(true,add(n,x),y)

→

minsort^#(app(rm(n,x),y),nil)

(23)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

if_minsort^#(false,add(n,x),y)	→	minsort^#(x,add(n,y))	(28)
minsort^#(add(n,x),y)	→	if_minsort^#(eq(n,min(add(n,x))),add(n,x),y)	(26)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 1
[if_rm(x₁, x₂, x₃)]	=	x₁ + x₃ + 19427
[s(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[if_rm^#(x₁, x₂, x₃)]	=	0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	25070
[false]	=	25070
[min^#(x₁)]	=	0
[true]	=	25068
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[if_minsort^#(x₁, x₂, x₃)]	=	x₂ + 3
[min(x₁)]	=	153629
[minsort^#(x₁, x₂)]	=	x₁ + 4
[add(x₁, x₂)]	=	x₁ + x₂ + 2
[if_min(x₁, x₂)]	=	x₂ + 153624
[if_minsort(x₁, x₂, x₃)]	=	0
[minsort(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	x₂ + 44497
[rm^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 38145

together with the usable rules

eq(s(x),s(y))	→	eq(x,y)	(4)
rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
app(nil,y)	→	y	(8)
eq(0,0)	→	true	(1)
eq(s(x),0)	→	false	(3)
if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
rm(n,nil)	→	nil	(14)
app(add(n,x),y)	→	add(n,app(x,y))	(9)
eq(0,s(x))	→	false	(2)

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

if_minsort^#(false,add(n,x),y)	→	minsort^#(x,add(n,y))	(28)
minsort^#(add(n,x),y)	→	if_minsort^#(eq(n,min(add(n,x))),add(n,x),y)	(26)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

if_min^#(false,add(n,add(m,x)))	→	min^#(add(m,x))	(35)
min^#(add(n,add(m,x)))	→	if_min^#(le(n,m),add(n,add(m,x)))	(34)
if_min^#(true,add(n,add(m,x)))	→	min^#(add(n,x))	(31)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 1
[if_rm(x₁, x₂, x₃)]	=	x₁ + x₃ + 44492
[s(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[if_rm^#(x₁, x₂, x₃)]	=	0
[if_min^#(x₁, x₂)]	=	x₂ + 0
[eq(x₁, x₂)]	=	5
[false]	=	5
[min^#(x₁)]	=	x₁ + 1
[true]	=	3
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[if_minsort^#(x₁, x₂, x₃)]	=	3
[min(x₁)]	=	153629
[minsort^#(x₁, x₂)]	=	x₁ + 4
[add(x₁, x₂)]	=	x₁ + x₂ + 2
[if_min(x₁, x₂)]	=	x₂ + 153624
[if_minsort(x₁, x₂, x₃)]	=	0
[minsort(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	x₂ + 44497
[rm^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 46111

together with the usable rules

eq(s(x),s(y))	→	eq(x,y)	(4)
rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
app(nil,y)	→	y	(8)
eq(0,0)	→	true	(1)
eq(s(x),0)	→	false	(3)
if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
rm(n,nil)	→	nil	(14)
app(add(n,x),y)	→	add(n,app(x,y))	(9)
eq(0,s(x))	→	false	(2)

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

if_min^#(false,add(n,add(m,x)))	→	min^#(add(m,x))	(35)
min^#(add(n,add(m,x)))	→	if_min^#(le(n,m),add(n,add(m,x)))	(34)
if_min^#(true,add(n,add(m,x)))	→	min^#(add(n,x))	(31)

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

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

→

le^#(x,y)

(25)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 29405
[if_rm(x₁, x₂, x₃)]	=	x₁ + x₃ + 44492
[s(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	x₁ + x₂ + 0
[if_rm^#(x₁, x₂, x₃)]	=	0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	29408
[false]	=	29408
[min^#(x₁)]	=	1
[true]	=	29407
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	36668
[app^#(x₁, x₂)]	=	0
[if_minsort^#(x₁, x₂, x₃)]	=	3
[min(x₁)]	=	153629
[minsort^#(x₁, x₂)]	=	x₁ + 4
[add(x₁, x₂)]	=	x₁ + x₂ + 1
[if_min(x₁, x₂)]	=	x₂ + 153626
[if_minsort(x₁, x₂, x₃)]	=	0
[minsort(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	x₂ + 73900
[rm^#(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 25155

together with the usable rules

eq(s(x),s(y))	→	eq(x,y)	(4)
rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
app(nil,y)	→	y	(8)
eq(0,0)	→	true	(1)
eq(s(x),0)	→	false	(3)
if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
rm(n,nil)	→	nil	(14)
app(add(n,x),y)	→	add(n,app(x,y))	(9)
eq(0,s(x))	→	false	(2)

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

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

→

le^#(x,y)

(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

if_rm^#(true,n,add(m,x))	→	rm^#(n,x)	(37)
rm^#(n,add(m,x))	→	if_rm^#(eq(n,m),n,add(m,x))	(33)
if_rm^#(false,n,add(m,x))	→	rm^#(n,x)	(30)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 29405
[if_rm(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[s(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[if_rm^#(x₁, x₂, x₃)]	=	x₁ + x₃ + 0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	29408
[false]	=	29408
[min^#(x₁)]	=	1
[true]	=	29408
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[if_minsort^#(x₁, x₂, x₃)]	=	3
[min(x₁)]	=	153629
[minsort^#(x₁, x₂)]	=	x₁ + 4
[add(x₁, x₂)]	=	x₁ + x₂ + 2
[if_min(x₁, x₂)]	=	x₂ + 153624
[if_minsort(x₁, x₂, x₃)]	=	0
[minsort(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	x₂ + 29408
[rm^#(x₁, x₂)]	=	x₂ + 29409
[app(x₁, x₂)]	=	x₁ + x₂ + 25155

together with the usable rules

eq(s(x),s(y))	→	eq(x,y)	(4)
rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
app(nil,y)	→	y	(8)
eq(0,0)	→	true	(1)
eq(s(x),0)	→	false	(3)
if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
rm(n,nil)	→	nil	(14)
app(add(n,x),y)	→	add(n,app(x,y))	(9)
eq(0,s(x))	→	false	(2)

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

if_rm^#(true,n,add(m,x))	→	rm^#(n,x)	(37)
rm^#(n,add(m,x))	→	if_rm^#(eq(n,m),n,add(m,x))	(33)
if_rm^#(false,n,add(m,x))	→	rm^#(n,x)	(30)

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

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

→

eq^#(x,y)

(39)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 1
[if_rm(x₁, x₂, x₃)]	=	x₁ + x₃ + 1102
[s(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[if_rm^#(x₁, x₂, x₃)]	=	x₁ + 0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	4
[false]	=	4
[min^#(x₁)]	=	1
[true]	=	4
[eq^#(x₁, x₂)]	=	x₁ + x₂ + 0
[0]	=	1
[nil]	=	1
[app^#(x₁, x₂)]	=	0
[if_minsort^#(x₁, x₂, x₃)]	=	3
[min(x₁)]	=	153629
[minsort^#(x₁, x₂)]	=	x₁ + 4
[add(x₁, x₂)]	=	x₁ + x₂ + 2
[if_min(x₁, x₂)]	=	x₂ + 153624
[if_minsort(x₁, x₂, x₃)]	=	0
[minsort(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	x₂ + 1106
[rm^#(x₁, x₂)]	=	29409
[app(x₁, x₂)]	=	x₁ + x₂ + 30057

together with the usable rules

eq(s(x),s(y))	→	eq(x,y)	(4)
rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
app(nil,y)	→	y	(8)
eq(0,0)	→	true	(1)
eq(s(x),0)	→	false	(3)
if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
rm(n,nil)	→	nil	(14)
app(add(n,x),y)	→	add(n,app(x,y))	(9)
eq(0,s(x))	→	false	(2)

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

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

→

eq^#(x,y)

(39)

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

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

→

app^#(x,y)

(22)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	x₁ + x₂ + 1
[if_rm(x₁, x₂, x₃)]	=	x₁ + x₃ + 1102
[s(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[if_rm^#(x₁, x₂, x₃)]	=	x₁ + 0
[if_min^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	27860
[false]	=	27860
[min^#(x₁)]	=	1
[true]	=	27859
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	1
[app^#(x₁, x₂)]	=	x₁ + 0
[if_minsort^#(x₁, x₂, x₃)]	=	3
[min(x₁)]	=	153629
[minsort^#(x₁, x₂)]	=	x₁ + 4
[add(x₁, x₂)]	=	x₁ + x₂ + 1
[if_min(x₁, x₂)]	=	x₂ + 153626
[if_minsort(x₁, x₂, x₃)]	=	0
[minsort(x₁, x₂)]	=	0
[rm(x₁, x₂)]	=	x₂ + 28962
[rm^#(x₁, x₂)]	=	29409
[app(x₁, x₂)]	=	x₁ + x₂ + 30371

together with the usable rules

eq(s(x),s(y))	→	eq(x,y)	(4)
rm(n,add(m,x))	→	if_rm(eq(n,m),n,add(m,x))	(15)
app(nil,y)	→	y	(8)
eq(0,0)	→	true	(1)
eq(s(x),0)	→	false	(3)
if_rm(true,n,add(m,x))	→	rm(n,x)	(16)
if_rm(false,n,add(m,x))	→	add(m,rm(n,x))	(17)
rm(n,nil)	→	nil	(14)
app(add(n,x),y)	→	add(n,app(x,y))	(9)
eq(0,s(x))	→	false	(2)

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

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

→

app^#(x,y)

(22)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.