Certification Problem

Input (TPDB TRS_Standard/Rubio_04/enno)

The rewrite relation of the following TRS is considered.

lt(0,s(X))	→	true	(1)
lt(s(X),0)	→	false	(2)
lt(s(X),s(Y))	→	lt(X,Y)	(3)
append(nil,Y)	→	Y	(4)
append(add(N,X),Y)	→	add(N,append(X,Y))	(5)
split(N,nil)	→	pair(nil,nil)	(6)
split(N,add(M,Y))	→	f_1(split(N,Y),N,M,Y)	(7)
f_1(pair(X,Z),N,M,Y)	→	f_2(lt(N,M),N,M,Y,X,Z)	(8)
f_2(true,N,M,Y,X,Z)	→	pair(X,add(M,Z))	(9)
f_2(false,N,M,Y,X,Z)	→	pair(add(M,X),Z)	(10)
qsort(nil)	→	nil	(11)
qsort(add(N,X))	→	f_3(split(N,X),N,X)	(12)
f_3(pair(Y,Z),N,X)	→	append(qsort(Y),add(X,qsort(Z)))	(13)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

lt^#(s(X),s(Y))	→	lt^#(X,Y)	(14)
append^#(add(N,X),Y)	→	append^#(X,Y)	(15)
split^#(N,add(M,Y))	→	split^#(N,Y)	(16)
split^#(N,add(M,Y))	→	f_1^#(split(N,Y),N,M,Y)	(17)
f_1^#(pair(X,Z),N,M,Y)	→	lt^#(N,M)	(18)
f_1^#(pair(X,Z),N,M,Y)	→	f_2^#(lt(N,M),N,M,Y,X,Z)	(19)
qsort^#(add(N,X))	→	split^#(N,X)	(20)
qsort^#(add(N,X))	→	f_3^#(split(N,X),N,X)	(21)
f_3^#(pair(Y,Z),N,X)	→	qsort^#(Z)	(22)
f_3^#(pair(Y,Z),N,X)	→	qsort^#(Y)	(23)
f_3^#(pair(Y,Z),N,X)	→	append^#(qsort(Y),add(X,qsort(Z)))	(24)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

f_3^#(pair(Y,Z),N,X)	→	qsort^#(Z)	(22)
qsort^#(add(N,X))	→	f_3^#(split(N,X),N,X)	(21)
f_3^#(pair(Y,Z),N,X)	→	qsort^#(Y)	(23)

1.1.1 Subterm Criterion Processor

We use the projection to multisets

π(f_3^#)	=	{ 1, 1, 1 }
π(qsort^#)	=	{ 1, 1 }
π(f_2)	=	{ 3, 3, 5, 5, 5, 6, 6, 6 }
π(f_1)	=	{ 1, 1, 1, 3, 3 }
π(pair)	=	{ 1, 2 }
π(split)	=	{ 2, 2 }
π(add)	=	{ 1, 1, 2, 2, 2 }

to remove the pairs:

f_3^#(pair(Y,Z),N,X)	→	qsort^#(Z)	(22)
qsort^#(add(N,X))	→	f_3^#(split(N,X),N,X)	(21)
f_3^#(pair(Y,Z),N,X)	→	qsort^#(Y)	(23)

1.1.1.1 P is empty

There are no pairs anymore.

The 2^nd component contains the pair
append^#(add(N,X),Y) → append^#(X,Y) (15)

1.1.2 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

append^#(add(N,X),Y) → append^#(X,Y) (15)

2 ≥ 2

1 > 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 3^rd component contains the pair
split^#(N,add(M,Y)) → split^#(N,Y) (16)

1.1.3 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

split^#(N,add(M,Y)) → split^#(N,Y) (16)

2 > 2

1 ≥ 1

As there is no critical graph in the transitive closure, there are no infinite chains.
The 4^th component contains the pair
lt^#(s(X),s(Y)) → lt^#(X,Y) (14)

1.1.4 Subterm Criterion Processor
We use the projection
π(lt^#) = 1
and remove the pairs:
lt^#(s(X),s(Y)) → lt^#(X,Y) (14)

1.1.4.1 P is empty

There are no pairs anymore.