Certification Problem

Input (TPDB TRS_Standard/Rubio_04/selsort)

The rewrite relation of the following TRS is considered.

eq(0,0)	→	true	(1)
eq(0,s(Y))	→	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)
min(cons(0,nil))	→	0	(8)
min(cons(s(N),nil))	→	s(N)	(9)
min(cons(N,cons(M,L)))	→	ifmin(le(N,M),cons(N,cons(M,L)))	(10)
ifmin(true,cons(N,cons(M,L)))	→	min(cons(N,L))	(11)
ifmin(false,cons(N,cons(M,L)))	→	min(cons(M,L))	(12)
replace(N,M,nil)	→	nil	(13)
replace(N,M,cons(K,L))	→	ifrepl(eq(N,K),N,M,cons(K,L))	(14)
ifrepl(true,N,M,cons(K,L))	→	cons(M,L)	(15)
ifrepl(false,N,M,cons(K,L))	→	cons(K,replace(N,M,L))	(16)
selsort(nil)	→	nil	(17)
selsort(cons(N,L))	→	ifselsort(eq(N,min(cons(N,L))),cons(N,L))	(18)
ifselsort(true,cons(N,L))	→	cons(N,selsort(L))	(19)
ifselsort(false,cons(N,L))	→	cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L)))	(20)

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.

ifmin^#(false,cons(N,cons(M,L)))	→	min^#(cons(M,L))	(21)
ifselsort^#(false,cons(N,L))	→	selsort^#(replace(min(cons(N,L)),N,L))	(22)
ifrepl^#(false,N,M,cons(K,L))	→	replace^#(N,M,L)	(23)
le^#(s(X),s(Y))	→	le^#(X,Y)	(24)
min^#(cons(N,cons(M,L)))	→	le^#(N,M)	(25)
ifselsort^#(true,cons(N,L))	→	selsort^#(L)	(26)
eq^#(s(X),s(Y))	→	eq^#(X,Y)	(27)
ifselsort^#(false,cons(N,L))	→	replace^#(min(cons(N,L)),N,L)	(28)
min^#(cons(N,cons(M,L)))	→	ifmin^#(le(N,M),cons(N,cons(M,L)))	(29)
ifselsort^#(false,cons(N,L))	→	min^#(cons(N,L))	(30)
selsort^#(cons(N,L))	→	min^#(cons(N,L))	(31)
selsort^#(cons(N,L))	→	eq^#(N,min(cons(N,L)))	(32)
replace^#(N,M,cons(K,L))	→	ifrepl^#(eq(N,K),N,M,cons(K,L))	(33)
ifmin^#(true,cons(N,cons(M,L)))	→	min^#(cons(N,L))	(34)
ifselsort^#(false,cons(N,L))	→	min^#(cons(N,L))	(30)
selsort^#(cons(N,L))	→	ifselsort^#(eq(N,min(cons(N,L))),cons(N,L))	(35)
replace^#(N,M,cons(K,L))	→	eq^#(N,K)	(36)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

selsort^#(cons(N,L))	→	ifselsort^#(eq(N,min(cons(N,L))),cons(N,L))	(35)
ifselsort^#(true,cons(N,L))	→	selsort^#(L)	(26)
ifselsort^#(false,cons(N,L))	→	selsort^#(replace(min(cons(N,L)),N,L))	(22)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[ifselsort(x₁, x₂)]	=	0
[le(x₁, x₂)]	=	x₂ + 4
[s(x₁)]	=	x₁ + 43374
[le^#(x₁, x₂)]	=	0
[ifmin(x₁, x₂)]	=	x₁ + x₂ + 0
[eq(x₁, x₂)]	=	20543
[false]	=	6
[min^#(x₁)]	=	0
[true]	=	2
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	28382
[ifrepl(x₁,...,x₄)]	=	x₄ + 1146
[selsort(x₁)]	=	0
[ifrepl^#(x₁,...,x₄)]	=	0
[selsort^#(x₁)]	=	x₁ + 20544
[replace^#(x₁, x₂, x₃)]	=	0
[ifselsort^#(x₁, x₂)]	=	x₁ + x₂ + 0
[min(x₁)]	=	43373
[cons(x₁, x₂)]	=	x₂ + 21685
[ifmin^#(x₁, x₂)]	=	0
[replace(x₁, x₂, x₃)]	=	x₃ + 1146

together with the usable rules

eq(s(X),s(Y))	→	eq(X,Y)	(4)
ifrepl(true,N,M,cons(K,L))	→	cons(M,L)	(15)
eq(0,0)	→	true	(1)
eq(s(X),0)	→	false	(3)
ifrepl(false,N,M,cons(K,L))	→	cons(K,replace(N,M,L))	(16)
replace(N,M,cons(K,L))	→	ifrepl(eq(N,K),N,M,cons(K,L))	(14)
replace(N,M,nil)	→	nil	(13)
eq(0,s(Y))	→	false	(2)

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

selsort^#(cons(N,L))	→	ifselsort^#(eq(N,min(cons(N,L))),cons(N,L))	(35)
ifselsort^#(true,cons(N,L))	→	selsort^#(L)	(26)
ifselsort^#(false,cons(N,L))	→	selsort^#(replace(min(cons(N,L)),N,L))	(22)

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

replace^#(N,M,cons(K,L))	→	ifrepl^#(eq(N,K),N,M,cons(K,L))	(33)
ifrepl^#(false,N,M,cons(K,L))	→	replace^#(N,M,L)	(23)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[ifselsort(x₁, x₂)]	=	0
[le(x₁, x₂)]	=	x₂ + 4
[s(x₁)]	=	x₁ + 43374
[le^#(x₁, x₂)]	=	0
[ifmin(x₁, x₂)]	=	x₁ + x₂ + 0
[eq(x₁, x₂)]	=	6
[false]	=	6
[min^#(x₁)]	=	0
[true]	=	2
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	35231
[ifrepl(x₁,...,x₄)]	=	x₄ + 1146
[selsort(x₁)]	=	0
[ifrepl^#(x₁,...,x₄)]	=	x₁ + x₄ + 0
[selsort^#(x₁)]	=	x₁ + 20544
[replace^#(x₁, x₂, x₃)]	=	x₃ + 7
[ifselsort^#(x₁, x₂)]	=	x₁ + 0
[min(x₁)]	=	7
[cons(x₁, x₂)]	=	x₂ + 2
[ifmin^#(x₁, x₂)]	=	0
[replace(x₁, x₂, x₃)]	=	x₃ + 1146

together with the usable rules

eq(s(X),s(Y))	→	eq(X,Y)	(4)
ifrepl(true,N,M,cons(K,L))	→	cons(M,L)	(15)
eq(0,0)	→	true	(1)
eq(s(X),0)	→	false	(3)
ifrepl(false,N,M,cons(K,L))	→	cons(K,replace(N,M,L))	(16)
replace(N,M,cons(K,L))	→	ifrepl(eq(N,K),N,M,cons(K,L))	(14)
replace(N,M,nil)	→	nil	(13)
eq(0,s(Y))	→	false	(2)

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

replace^#(N,M,cons(K,L))	→	ifrepl^#(eq(N,K),N,M,cons(K,L))	(33)
ifrepl^#(false,N,M,cons(K,L))	→	replace^#(N,M,L)	(23)

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

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

→

eq^#(X,Y)

(27)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[ifselsort(x₁, x₂)]	=	0
[le(x₁, x₂)]	=	x₂ + 3
[s(x₁)]	=	x₁ + 43371
[le^#(x₁, x₂)]	=	0
[ifmin(x₁, x₂)]	=	x₁ + x₂ + 0
[eq(x₁, x₂)]	=	5
[false]	=	5
[min^#(x₁)]	=	0
[true]	=	1
[eq^#(x₁, x₂)]	=	x₂ + 0
[0]	=	1
[nil]	=	54788
[ifrepl(x₁,...,x₄)]	=	x₄ + 19781
[selsort(x₁)]	=	0
[ifrepl^#(x₁,...,x₄)]	=	x₁ + 0
[selsort^#(x₁)]	=	x₁ + 20544
[replace^#(x₁, x₂, x₃)]	=	7
[ifselsort^#(x₁, x₂)]	=	x₁ + 0
[min(x₁)]	=	4
[cons(x₁, x₂)]	=	x₂ + 1
[ifmin^#(x₁, x₂)]	=	0
[replace(x₁, x₂, x₃)]	=	x₃ + 19781

together with the usable rules

eq(s(X),s(Y))	→	eq(X,Y)	(4)
ifrepl(true,N,M,cons(K,L))	→	cons(M,L)	(15)
eq(0,0)	→	true	(1)
eq(s(X),0)	→	false	(3)
ifrepl(false,N,M,cons(K,L))	→	cons(K,replace(N,M,L))	(16)
replace(N,M,cons(K,L))	→	ifrepl(eq(N,K),N,M,cons(K,L))	(14)
replace(N,M,nil)	→	nil	(13)
eq(0,s(Y))	→	false	(2)

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

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

→

eq^#(X,Y)

(27)

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

ifmin^#(true,cons(N,cons(M,L)))	→	min^#(cons(N,L))	(34)
min^#(cons(N,cons(M,L)))	→	ifmin^#(le(N,M),cons(N,cons(M,L)))	(29)
ifmin^#(false,cons(N,cons(M,L)))	→	min^#(cons(M,L))	(21)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[ifselsort(x₁, x₂)]	=	0
[le(x₁, x₂)]	=	x₂ + 3
[s(x₁)]	=	x₁ + 43373
[le^#(x₁, x₂)]	=	0
[ifmin(x₁, x₂)]	=	x₁ + x₂ + 0
[eq(x₁, x₂)]	=	1
[false]	=	0
[min^#(x₁)]	=	x₁ + 1
[true]	=	1
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	54788
[ifrepl(x₁,...,x₄)]	=	x₄ + 19781
[selsort(x₁)]	=	0
[ifrepl^#(x₁,...,x₄)]	=	x₁ + 0
[selsort^#(x₁)]	=	x₁ + 20544
[replace^#(x₁, x₂, x₃)]	=	7
[ifselsort^#(x₁, x₂)]	=	x₁ + 0
[min(x₁)]	=	6
[cons(x₁, x₂)]	=	x₂ + 2
[ifmin^#(x₁, x₂)]	=	x₂ + 0
[replace(x₁, x₂, x₃)]	=	x₃ + 19781

together with the usable rules

eq(s(X),s(Y))	→	eq(X,Y)	(4)
ifrepl(true,N,M,cons(K,L))	→	cons(M,L)	(15)
eq(0,0)	→	true	(1)
eq(s(X),0)	→	false	(3)
ifrepl(false,N,M,cons(K,L))	→	cons(K,replace(N,M,L))	(16)
le(0,Y)	→	true	(5)
le(s(X),s(Y))	→	le(X,Y)	(7)
replace(N,M,cons(K,L))	→	ifrepl(eq(N,K),N,M,cons(K,L))	(14)
replace(N,M,nil)	→	nil	(13)
le(s(X),0)	→	false	(6)
eq(0,s(Y))	→	false	(2)

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

ifmin^#(true,cons(N,cons(M,L)))	→	min^#(cons(N,L))	(34)
min^#(cons(N,cons(M,L)))	→	ifmin^#(le(N,M),cons(N,cons(M,L)))	(29)
ifmin^#(false,cons(N,cons(M,L)))	→	min^#(cons(M,L))	(21)

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)

(24)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[ifselsort(x₁, x₂)]	=	0
[le(x₁, x₂)]	=	x₂ + 3
[s(x₁)]	=	x₁ + 43371
[le^#(x₁, x₂)]	=	x₂ + 0
[ifmin(x₁, x₂)]	=	x₁ + x₂ + 0
[eq(x₁, x₂)]	=	1
[false]	=	0
[min^#(x₁)]	=	1
[true]	=	1
[eq^#(x₁, x₂)]	=	0
[0]	=	1
[nil]	=	33694
[ifrepl(x₁,...,x₄)]	=	x₄ + 36229
[selsort(x₁)]	=	0
[ifrepl^#(x₁,...,x₄)]	=	x₁ + 0
[selsort^#(x₁)]	=	x₁ + 20544
[replace^#(x₁, x₂, x₃)]	=	7
[ifselsort^#(x₁, x₂)]	=	x₁ + 0
[min(x₁)]	=	4
[cons(x₁, x₂)]	=	x₂ + 1
[ifmin^#(x₁, x₂)]	=	0
[replace(x₁, x₂, x₃)]	=	x₃ + 36229

together with the usable rules

eq(s(X),s(Y))	→	eq(X,Y)	(4)
ifrepl(true,N,M,cons(K,L))	→	cons(M,L)	(15)
eq(0,0)	→	true	(1)
eq(s(X),0)	→	false	(3)
ifrepl(false,N,M,cons(K,L))	→	cons(K,replace(N,M,L))	(16)
le(0,Y)	→	true	(5)
le(s(X),s(Y))	→	le(X,Y)	(7)
replace(N,M,cons(K,L))	→	ifrepl(eq(N,K),N,M,cons(K,L))	(14)
replace(N,M,nil)	→	nil	(13)
le(s(X),0)	→	false	(6)
eq(0,s(Y))	→	false	(2)

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

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

→

le^#(X,Y)

(24)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.