:: Quick Sort on SCMPDS
:: by JingChao Chen
::
:: Copyright (c) 2000-2021 Association of Mizar Users

registration
let I, J be shiftable Program of ;
let a be Int_position;
let k1 be Integer;
cluster if>0 (a,k1,I,J) -> shiftable ;
correctness
coherence
if>0 (a,k1,I,J) is shiftable
;
proof end;
end;

theorem Th1: :: SCPQSORT:1
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for J being shiftable Program of
for a, b being Int_position
for k1 being Integer st s . (DataLoc ((s . a),k1)) > 0 & I is_closed_on s,P & I is_halting_on s,P holds
(IExec ((if>0 (a,k1,I,J)),P,s)) . b = (IExec (I,P,s)) . b
proof end;

set A = NAT ;

set D = SCM-Data-Loc ;

Lm1: for a being Int_position
for i being Integer
for I being Program of holds while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))

proof end;

Lm2: for I being Program of
for a being Int_position
for i being Integer holds Shift (I,1) c= while>0 (a,i,I)

proof end;

theorem Th2: :: SCPQSORT:2
for P being Instruction-Sequence of SCMPDS
for s, sm being State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for m being Nat st I is_closed_on s,P & I is_halting_on s,P & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((P +* (stop I)),())) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(),m) holds
( DataPart sm = DataPart (IExec (I,P,())) & Initialize sm = sm )
proof end;

theorem Th3: :: SCPQSORT:3
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st DataPart t = DataPart s holds
I is_halting_on t,Q ) holds
I is_closed_on s,P
proof end;

theorem Th4: :: SCPQSORT:4
for i1, i2, i3, i4 being Instruction of SCMPDS holds card (((i1 ';' i2) ';' i3) ';' i4) = 4
proof end;

theorem Th5: :: SCPQSORT:5
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a, x, y being Int_position
for i, c being Integer st s . x >= c + (s . (DataLoc ((s . a),i))) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c + (t . (DataLoc ((s . a),i))) & t . y = s . y & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) & (IExec (I,Q,t)) . y = t . y ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
proof end;

theorem Th6: :: SCPQSORT:6
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a, x, y being Int_position
for i, c being Integer st s . x >= c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c & t . y = s . y & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x >= c & (IExec (I,Q,t)) . y = t . y ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
proof end;

theorem Th7: :: SCPQSORT:7
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) & md <= (s . x3) - c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) & md <= (t . x3) - c & t . x2 = s . x2 & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) & (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) & md <= ((IExec (I,Q,t)) . x3) - c & (IExec (I,Q,t)) . x2 = t . x2 ) ) holds
( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P & ( s . (DataLoc ((s . a),i)) > 0 implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) ) )
proof end;

theorem Th8: :: SCPQSORT:8
for f being FinSequence of INT
for m, k1, k, n being Nat st k1 = k - 1 & f is_non_decreasing_on m,k1 & f is_non_decreasing_on k + 1,n & ( for i being Nat st m <= i & i < k holds
f . i <= f . k ) & ( for i being Nat st k < i & i <= n holds
f . k <= f . i ) holds
f is_non_decreasing_on m,n
proof end;

Lm3: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i, c being Integer
for f, g being FinSequence of INT
for m, n, m1 being Nat st s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m & 1 = s . (DataLoc (c,i)) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Nat st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s,P & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )

proof end;

Lm4: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i, c being Integer
for m, n, m1 being Nat st s . a = c & 1 = s . (DataLoc (c,i)) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Nat st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
while>0 (a,i,I) is_halting_on s,P

proof end;

Lm5: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i, c being Integer
for m, n, m1 being Nat st s . a = c & 1 = s . (DataLoc (c,i)) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Nat st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P )

proof end;

:: a "larger" subsequence
:: a5=a7=length a2=mid(x[1]), a3=x[2], a4=x[n], a6=save
definition
func Partition -> Program of equals :: SCPQSORT:def 1
coherence
;
end;

:: deftheorem defines Partition SCPQSORT:def 1 :

:: a0=global, a1=stack, a2=stack depth
definition
let n, p0 be Nat;
func QuickSort (n,p0) -> Program of equals :: SCPQSORT:def 2
(((() ';' ()) ';' ((SBP,(p0 + n)) := (p0 + 1))) ';' ((SBP,((p0 + n) + 1)) := (p0 + n))) ';' (while>0 (GBP,1,((((GBP,2) := (SBP,((p0 + n) + 1))) ';' (SubFrom (GBP,2,SBP,(p0 + n)))) ';' (if>0 (GBP,2,(((((GBP,2) := (SBP,(p0 + n))) ';' ((GBP,4) := (SBP,((p0 + n) + 1)))) ';' Partition) ';' (((((((SBP,((p0 + n) + 3)) := (SBP,((p0 + n) + 1))) ';' ((SBP,((p0 + n) + 1)) := (GBP,4))) ';' ((SBP,((p0 + n) + 2)) := (GBP,4))) ';' (AddTo (SBP,((p0 + n) + 1),(- 1)))) ';' (AddTo (SBP,((p0 + n) + 2),1))) ';' (AddTo (GBP,1,2)))),(Load (AddTo (GBP,1,(- 2)))))))));
coherence
(((() ';' ()) ';' ((SBP,(p0 + n)) := (p0 + 1))) ';' ((SBP,((p0 + n) + 1)) := (p0 + n))) ';' (while>0 (GBP,1,((((GBP,2) := (SBP,((p0 + n) + 1))) ';' (SubFrom (GBP,2,SBP,(p0 + n)))) ';' (if>0 (GBP,2,(((((GBP,2) := (SBP,(p0 + n))) ';' ((GBP,4) := (SBP,((p0 + n) + 1)))) ';' Partition) ';' (((((((SBP,((p0 + n) + 3)) := (SBP,((p0 + n) + 1))) ';' ((SBP,((p0 + n) + 1)) := (GBP,4))) ';' ((SBP,((p0 + n) + 2)) := (GBP,4))) ';' (AddTo (SBP,((p0 + n) + 1),(- 1)))) ';' (AddTo (SBP,((p0 + n) + 2),1))) ';' (AddTo (GBP,1,2)))),(Load (AddTo (GBP,1,(- 2))))))))) is Program of
;
end;

:: deftheorem defines QuickSort SCPQSORT:def 2 :
for n, p0 being Nat holds QuickSort (n,p0) = (((() ';' ()) ';' ((SBP,(p0 + n)) := (p0 + 1))) ';' ((SBP,((p0 + n) + 1)) := (p0 + n))) ';' (while>0 (GBP,1,((((GBP,2) := (SBP,((p0 + n) + 1))) ';' (SubFrom (GBP,2,SBP,(p0 + n)))) ';' (if>0 (GBP,2,(((((GBP,2) := (SBP,(p0 + n))) ';' ((GBP,4) := (SBP,((p0 + n) + 1)))) ';' Partition) ';' (((((((SBP,((p0 + n) + 3)) := (SBP,((p0 + n) + 1))) ';' ((SBP,((p0 + n) + 1)) := (GBP,4))) ';' ((SBP,((p0 + n) + 2)) := (GBP,4))) ';' (AddTo (SBP,((p0 + n) + 1),(- 1)))) ';' (AddTo (SBP,((p0 + n) + 2),1))) ';' (AddTo (GBP,1,2)))),(Load (AddTo (GBP,1,(- 2)))))))));

set i1 = (GBP,7) := (GBP,5);

set i2 = AddTo (GBP,5,(- 1));

set i3 = (GBP,6) := ((),0);

set i4 = SubFrom (GBP,6,(),0);

set i5 = AddTo (GBP,4,(- 1));

set i6 = AddTo (GBP,7,(- 1));

set i7 = Load ((GBP,5) := 0);

set WB1 = (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))));

set WH1 = while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))));

set j1 = (GBP,5) := (GBP,7);

set j2 = AddTo (GBP,7,(- 1));

set j3 = (GBP,6) := ((),0);

set j4 = SubFrom (GBP,6,(),0);

set j6 = AddTo (GBP,5,(- 1));

set j7 = Load ((GBP,7) := 0);

set WB2 = (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))));

set WH2 = while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))));

set k1 = (GBP,5) := (GBP,4);

set k2 = SubFrom (GBP,5,GBP,2);

set k3 = (GBP,3) := (GBP,2);

set K4 = ((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1));

set k5 = (GBP,6) := ((),0);

set k6 = ((),0) := ((),0);

set k7 = ((),0) := (GBP,6);

set k8 = AddTo (GBP,5,(- 2));

set k0 = AddTo (GBP,4,(- 1));

set IF3 = if>0 (GBP,5,(((((((GBP,6) := ((),0)) ';' (((),0) := ((),0))) ';' (((),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))));

set j8 = (GBP,6) := ((),0);

set j9 = ((),0) := ((),0);

set j0 = ((),0) := (GBP,6);

set a1 = intpos 1;

set a2 = intpos 2;

set a3 = intpos 3;

set a4 = intpos 4;

set a5 = intpos 5;

set a6 = intpos 6;

set a7 = intpos 7;

Lm6: card ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))) = 9
proof end;

Lm7: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, me being Nat st s . () = md & s . () = me & md >= 8 & me >= 8 & s . GBP = 0 holds

proof end;

Lm8: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for m4, md being Nat st s . GBP = 0 & s . () > 0 & s . () = m4 + (s . ()) & m4 >= 8 & s . () = md & md >= 8 holds
(IExec ((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))),P,s)) . () = s . () ) & ex mE being Nat st
( mE = (IExec ((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))),P,s)) . () & (IExec ((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))),P,s)) . () = m4 + mE & mE <= s . () & ( for i being Nat st m4 + mE < i & i <= s . () holds

proof end;

Lm9: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for m4, md being Nat st s . GBP = 0 & s . () = m4 + (s . ()) & m4 >= 8 & s . () = md & md >= 8 holds
( while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))))) is_closed_on s,P & while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0)))))) is_halting_on s,P )

proof end;

Lm10: card (while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) = 11
proof end;

Lm11: card ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))) = 9
proof end;

Lm12: card (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))))) = 11
proof end;

Lm13: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, me being Nat st s . () = md & s . () = me & md >= 8 & me >= 8 & s . GBP = 0 holds

proof end;

Lm14: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for m3, md being Nat st s . GBP = 0 & s . () > 0 & (s . ()) + (s . ()) = m3 & s . () >= 8 & s . () = md & md >= 8 holds
(IExec ((while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))))),P,s)) . () = s . () ) & ex m5, mE3 being Nat st
( m5 = (IExec ((while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))))),P,s)) . () & (IExec ((while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))))),P,s)) . () = mE3 & mE3 + m5 = m3 & m5 <= s . () & ( for i being Nat st s . () <= i & i < mE3 holds

proof end;

Lm15: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md being Nat st s . GBP = 0 & s . () >= 8 & s . () = md & md >= 8 holds
( while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))) is_closed_on s,P & while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((),0))) ';' (SubFrom (GBP,6,(),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))) is_halting_on s,P )

proof end;

proof end;

proof end;

theorem Th9: :: SCPQSORT:9
proof end;

Lm18: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for m3, m4 being Nat st s . GBP = 0 & s . () > 0 & s . () = m3 & s . () = m4 & m3 > 6 & m4 > 6 holds
(IExec ((if>0 (GBP,5,(((((((GBP,6) := ((),0)) ';' (((),0) := ((),0))) ';' (((),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,())) . () = s . () ) )

proof end;

Lm19: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, m3 being Nat st s . GBP = 0 & s . () > 0 & s . () = m3 + (s . ()) & m3 = (s . ()) - 1 & s . () = md & md >= 8 & md <= m3 holds

proof end;

Lm20: for i being Integer st i >= - 1 & i <= 0 & not i = - 1 holds
i = 0

proof end;

Lm21: for i1, i2 being Integer
for n1, n2, i being Nat st i1 >= - 1 & i1 <= 0 & n2 = i2 + 1 & i2 = n1 + i1 & i < n2 holds
i <= n1

proof end;

Lm22: for i1, i2 being Integer
for n1, n2 being Nat st i1 >= - 1 & n2 = i2 + 1 & i2 = n1 + i1 holds
n1 <= n2

proof end;

Lm23: for s, s1 being State of SCMPDS
for n0, n1, n2, n being Nat
for f, f1 being FinSequence of INT st f is_FinSequence_on s,n0 & f1 is_FinSequence_on s1,n0 & len f = n & len f1 = n & ( for i being Nat st i >= n0 + 1 & i <> n1 & i <> n2 holds
s1 . () = s . () ) & ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) holds
f,f1 are_fiberwise_equipotent

proof end;

Lm24: for s, s1 being State of SCMPDS
for n0, n1, n2 being Nat
for c1, c2 being Integer st ( for i being Nat st i >= n0 & i <> n1 & i <> n2 holds
s1 . () = s . () ) & n1 <= n2 & ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( c1 <= n1 & n2 <= c2 & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) holds
for i being Nat st i >= n0 & ( i < c1 or i > c2 ) holds
s1 . () = s . ()

proof end;

Lm25: for n being Nat
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, m3, n0 being Nat

proof end;

Lm26: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, m3, n0 being Nat st s . GBP = 0 & s . () = m3 + (s . ()) & m3 = (s . ()) - 1 & s . () = md & md >= n0 + 1 & md <= m3 & n0 >= 7 holds

proof end;

Lm27: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . GBP = 0 holds
( (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,())) . GBP = 0 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,())) . () = s . () & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,())) . () = s . () & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,())) . () = (s . ()) + 1 & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,())) . () = s . () & (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,())) . () = (s . ()) - (s . ()) & ( for i being Nat st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,())) . () = s . () ) )

proof end;

theorem Th10: :: SCPQSORT:10
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, p0 being Nat st s . GBP = 0 & s . () = md & md >= p0 + 1 & p0 >= 7 holds
( Partition is_closed_on s,P & Partition is_halting_on s,P )
proof end;

theorem Th11: :: SCPQSORT:11
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, p0, n being Nat
for f, f1 being FinSequence of INT st s . GBP = 0 & (s . ()) - (s . ()) > 0 & s . () = md & md >= p0 + 1 & s . () <= p0 + n & p0 >= 7 & f is_FinSequence_on s,p0 & len f = n & f1 is_FinSequence_on IExec (Partition,P,s),p0 & len f1 = n holds
( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . () = s . () & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . () & md <= m4 & m4 <= s . () & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . () ) & ( for i being Nat st m4 < i & i <= s . () holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . () ) & ( for i being Nat st i >= p0 + 1 & ( i < s . () or i > s . () ) holds
(IExec (Partition,P,s)) . () = s . () ) ) )
proof end;

theorem :: SCPQSORT:12
( Partition is halt-free & Partition is shiftable ) ;

Lm28: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for p0, n being Nat holds
( card (QuickSort (n,p0)) = 57 & ( p0 >= 7 implies ( QuickSort (n,p0) is_halting_on s,P & ex f, g being FinSequence of INT st
( len f = n & f is_FinSequence_on s,p0 & len g = n & g is_FinSequence_on IExec ((QuickSort (n,p0)),P,s),p0 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) ) ) )

proof end;

theorem :: SCPQSORT:13
for n, p0 being Nat holds card (QuickSort (n,p0)) = 57 by Lm28;

theorem :: SCPQSORT:14
for p0, n being Nat st p0 >= 7 holds
QuickSort (n,p0) is parahalting
proof end;

theorem :: SCPQSORT:15
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for p0, n being Nat st p0 >= 7 holds
ex f, g being FinSequence of INT st
( len f = n & f is_FinSequence_on s,p0 & len g = n & g is_FinSequence_on IExec ((QuickSort (n,p0)),P,s),p0 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) by Lm28;