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.