:: Quick Sort on SCMPDS
:: by JingChao Chen
::
:: Received June 14, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

registration
let I, J be shiftable Program of SCMPDS;
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 ;
proofend;
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 SCMPDS
for J being shiftable Program of SCMPDS
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
proofend;

set A = NAT ;

set D = SCM-Data-Loc ;

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

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

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 SCMPDS
for a being Int_position
for i being Integer
for m being Element of NAT st I is_closed_on s,P &amp; I is_halting_on s,P &amp; s . (DataLoc ((s . a),i)) > 0 &amp; m = (LifeSpan ((P +* (stop I)),(Initialize s))) + 2 &amp; sm = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),m) holds
( DataPart sm = DataPart (IExec (I,P,(Initialize s))) &amp; Initialize sm = sm )
proofend;

theorem Th3: :: SCPQSORT:3
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS 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
proofend;

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

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 SCMPDS
for a, x, y being Int_position
for i, c being Integer st s . x >= c + (s . (DataLoc ((s . a),i))) &amp; ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c + (t . (DataLoc ((s . a),i))) &amp; t . y = s . y &amp; t . a = s . a &amp; t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a &amp; I is_closed_on t,Q &amp; I is_halting_on t,Q &amp; (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) &amp; (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) &amp; (IExec (I,Q,t)) . y = t . y ) ) holds
( while>0 (a,i,I) is_closed_on s,P &amp; while>0 (a,i,I) is_halting_on s,P &amp; ( 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)))) ) )
proofend;

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 SCMPDS
for a, x, y being Int_position
for i, c being Integer st s . x >= c &amp; ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= c &amp; t . y = s . y &amp; t . a = s . a &amp; t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a &amp; I is_closed_on t,Q &amp; I is_halting_on t,Q &amp; (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) &amp; (IExec (I,Q,t)) . x >= c &amp; (IExec (I,Q,t)) . y = t . y ) ) holds
( while>0 (a,i,I) is_closed_on s,P &amp; while>0 (a,i,I) is_halting_on s,P &amp; ( 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)))) ) )
proofend;

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 SCMPDS
for a, x1, x2, x3, x4 being Int_position
for i, c, md being Integer st s . x4 = ((s . x3) - c) + (s . x1) &amp; md <= (s . x3) - c &amp; ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x4 = ((t . x3) - c) + (t . x1) &amp; md <= (t . x3) - c &amp; t . x2 = s . x2 &amp; t . a = s . a &amp; t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a &amp; I is_closed_on t,Q &amp; I is_halting_on t,Q &amp; (IExec (I,Q,t)) . (DataLoc ((s . a),i)) < t . (DataLoc ((s . a),i)) &amp; (IExec (I,Q,t)) . x4 = (((IExec (I,Q,t)) . x3) - c) + ((IExec (I,Q,t)) . x1) &amp; md <= ((IExec (I,Q,t)) . x3) - c &amp; (IExec (I,Q,t)) . x2 = t . x2 ) ) holds
( while>0 (a,i,I) is_closed_on s,P &amp; while>0 (a,i,I) is_halting_on s,P &amp; ( 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)))) ) )
proofend;

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

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

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

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

begin

:: a "larger" subsequence
:: a5=a7=length a2=mid(x[1]), a3=x[2], a4=x[n], a6=save
definition
func Partition  ->  Program of SCMPDS equals :: SCPQSORT:def 1
((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))) ';' (((intpos 2),0) := (GBP,6));
coherence
 ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))) ';' (((intpos 2),0) := (GBP,6)) is Program of SCMPDS ;
end;

:: deftheorem  defines Partition SCPQSORT:def_1_:_
 Partition = ((((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))) ';' (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))))) ';' ((GBP,6) := ((intpos 4),0))) ';' (((intpos 4),0) := ((intpos 2),0))) ';' (((intpos 2),0) := (GBP,6));

begin

:: a0=global, a1=stack, a2=stack depth
definition
let n, p0 be Element of NAT ;
func QuickSort (n,p0) ->  Program of SCMPDS equals :: SCPQSORT:def 2
((((GBP := 0) ';' (SBP := 1)) ';' ((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
 ((((GBP := 0) ';' (SBP := 1)) ';' ((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 SCMPDS ;
end;

:: deftheorem  defines QuickSort SCPQSORT:def_2_:_
 for n, p0 being Element of NAT holds QuickSort (n,p0) = ((((GBP := 0) ';' (SBP := 1)) ';' ((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) := ((intpos 4),0);

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

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

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

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

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

set WB1 = (((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),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) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),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) := ((intpos 2),0);

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

set j5 = AddTo (GBP,3,1);

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

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

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

set WB2 = (((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),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) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),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 = AddTo (GBP,3,1);

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

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

set k6 = ((intpos 4),0) := ((intpos 3),0);

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

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

set k9 = AddTo (GBP,3,1);

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

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

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

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

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

set j9 = ((intpos 4),0) := ((intpos 2),0);

set j0 = ((intpos 2),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;

Lm7:  card ((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))) = 9
proofend;

Lm8:  for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, me being Element of NAT st s . (intpos 2) = md &amp; s . (intpos 4) = me &amp; md >= 8 &amp; me >= 8 &amp; s . GBP = 0 holds
( (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . GBP = 0 &amp; (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 1) = s . (intpos 1) &amp; (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 2) = s . (intpos 2) &amp; (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 3) = s . (intpos 3) &amp; ( for i being Element of NAT st i >= 8 holds
(IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) &amp; ( s . (intpos md) < s . (intpos me) implies ( (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 5) = (s . (intpos 5)) - 1 &amp; (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 &amp; (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 7) = (s . (intpos 5)) - 1 ) ) &amp; ( s . (intpos md) >= s . (intpos me) implies ( (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 5) = 0 &amp; (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 4) = s . (intpos 4) &amp; (IExec (((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))),P,s)) . (intpos 7) = s . (intpos 5) ) ) )
proofend;

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

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

Lm11:  card (while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) = 11
proofend;

Lm12:  card ((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))) = 9
proofend;

Lm13:  card (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))))) = 11
proofend;

Lm14:  for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, me being Element of NAT st s . (intpos 2) = md &amp; s . (intpos 3) = me &amp; md >= 8 &amp; me >= 8 &amp; s . GBP = 0 holds
( (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . GBP = 0 &amp; (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 1) = s . (intpos 1) &amp; (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 2) = s . (intpos 2) &amp; (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 4) = s . (intpos 4) &amp; ( for i being Element of NAT st i >= 8 holds
(IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos i) = s . (intpos i) ) &amp; ( s . (intpos md) > s . (intpos me) implies ( (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 7) = (s . (intpos 7)) - 1 &amp; (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 3) = (s . (intpos 3)) + 1 &amp; (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 5) = (s . (intpos 7)) - 1 ) ) &amp; ( s . (intpos md) <= s . (intpos me) implies ( (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 7) = 0 &amp; (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 3) = s . (intpos 3) &amp; (IExec (((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0))))),P,s)) . (intpos 5) = s . (intpos 7) ) ) )
proofend;

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

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

Lm17:  card (((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))) = 29
proofend;

Lm18:  card (while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))) = 31
proofend;

begin

theorem Th12: :: SCPQSORT:9
card Partition = 38
proofend;

Lm19:  for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for m3, m4 being Element of NAT st s . GBP = 0 &amp; s . (intpos 5) > 0 &amp; s . (intpos 3) = m3 &amp; s . (intpos 4) = m4 &amp; m3 > 6 &amp; m4 > 6 holds
( (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . GBP = 0 &amp; (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 1) = s . (intpos 1) &amp; (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 2) = s . (intpos 2) &amp; (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos m3) = s . (intpos m4) &amp; (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos m4) = s . (intpos m3) &amp; (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 3) = (s . (intpos 3)) + 1 &amp; (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 4) = (s . (intpos 4)) - 1 &amp; (IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos 5) = (s . (intpos 5)) - 2 &amp; ( for i being Element of NAT st i >= 8 &amp; i <> m3 &amp; i <> m4 holds
(IExec ((if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
proofend;

Lm20:  for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, m3 being Element of NAT st s . GBP = 0 &amp; s . (intpos 5) > 0 &amp; s . (intpos 4) = m3 + (s . (intpos 5)) &amp; m3 = (s . (intpos 3)) - 1 &amp; s . (intpos 2) = md &amp; md >= 8 &amp; md <= m3 holds
( ((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))) is_closed_on s,P &amp; ((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))) is_halting_on s,P &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . GBP = 0 &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 1) = s . (intpos 1) &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 2) = md &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 3) >= s . (intpos 3) &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 4) <= s . (intpos 4) &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 4) >= m3 &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 5) < s . (intpos 5) &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 5) >= - 1 &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 4) = (((IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 3)) - 1) + ((IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 5)) &amp; ex n1, n2 being Element of NAT st
( n1 = ((IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 3)) - 1 &amp; n2 = ((IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos 4)) + 1 &amp; ( for i being Element of NAT st i >= 8 &amp; i <> n1 &amp; i <> n2 holds
(IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos i) = s . (intpos i) ) &amp; ( ( (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos n1) = s . (intpos n1) &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos n2) = s . (intpos n2) ) or ( n1 >= s . (intpos 3) &amp; n2 <= s . (intpos 4) &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos n1) = s . (intpos n2) &amp; (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos n2) = s . (intpos n1) ) ) &amp; ( for i being Element of NAT st s . (intpos 3) <= i &amp; i <= n1 holds
(IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos md) >= (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos i) ) &amp; ( for i being Element of NAT st n2 <= i &amp; i <= s . (intpos 4) holds
(IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos md) <= (IExec ((((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))),P,s)) . (intpos i) ) ) )
proofend;

Lm21:  for i being Integer st i >= - 1 &amp; i <= 0 &amp; not i = - 1 holds
i = 0
proofend;

Lm22:  for i1, i2 being Integer
for n1, n2, i being Element of NAT st i1 >= - 1 &amp; i1 <= 0 &amp; n2 = i2 + 1 &amp; i2 = n1 + i1 &amp; i < n2 holds
i <= n1
proofend;

Lm23:  for i1, i2 being Integer
for n1, n2 being Element of NAT st i1 >= - 1 &amp; n2 = i2 + 1 &amp; i2 = n1 + i1 holds
n1 <= n2
proofend;

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

Lm25:  for s, s1 being State of SCMPDS
for n0, n1, n2 being Element of NAT
for c1, c2 being Integer st ( for i being Element of NAT st i >= n0 &amp; i <> n1 &amp; i <> n2 holds
s1 . (intpos i) = s . (intpos i) ) &amp; n1 <= n2 &amp; ( ( s1 . (intpos n1) = s . (intpos n1) &amp; s1 . (intpos n2) = s . (intpos n2) ) or ( c1 <= n1 &amp; n2 <= c2 &amp; s1 . (intpos n1) = s . (intpos n2) &amp; s1 . (intpos n2) = s . (intpos n1) ) ) holds
for i being Element of NAT st i >= n0 &amp; ( i < c1 or i > c2 ) holds
s1 . (intpos i) = s . (intpos i)
proofend;

Lm26:  for n being Element of NAT
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, m3, n0 being Element of NAT
for f, f1 being FinSequence of INT st s . GBP = 0 &amp; s . (intpos 5) > 0 &amp; s . (intpos 4) = m3 + (s . (intpos 5)) &amp; m3 = (s . (intpos 3)) - 1 &amp; s . (intpos 2) = md &amp; md >= n0 + 1 &amp; md <= m3 &amp; n0 + 1 <= s . (intpos 3) &amp; s . (intpos 4) <= n0 + n &amp; f is_FinSequence_on s,n0 &amp; f1 is_FinSequence_on IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s),n0 &amp; n0 >= 7 &amp; len f = n &amp; len f1 = n holds
( (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . GBP = 0 &amp; (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos 1) = s . (intpos 1) &amp; (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos 2) = md &amp; (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos 4) >= md &amp; (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos 4) <= s . (intpos 4) &amp; f,f1 are_fiberwise_equipotent &amp; ( for i being Element of NAT st s . (intpos 3) <= i &amp; i <= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos 4) holds
(IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos md) >= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos i) ) &amp; ( for i being Element of NAT st (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos 4) < i &amp; i <= s . (intpos 4) holds
(IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos md) <= (IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos i) ) &amp; ( for i being Element of NAT st i >= n0 + 1 &amp; ( i < s . (intpos 3) or i > s . (intpos 4) ) holds
(IExec ((while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1))))))))),P,s)) . (intpos i) = s . (intpos i) ) )
proofend;

Lm27:  for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, m3, n0 being Element of NAT st s . GBP = 0 &amp; s . (intpos 4) = m3 + (s . (intpos 5)) &amp; m3 = (s . (intpos 3)) - 1 &amp; s . (intpos 2) = md &amp; md >= n0 + 1 &amp; md <= m3 &amp; n0 >= 7 holds
( while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_closed_on s,P &amp; while>0 (GBP,5,(((while>0 (GBP,5,((((((GBP,7) := (GBP,5)) ';' (AddTo (GBP,5,(- 1)))) ';' ((GBP,6) := ((intpos 4),0))) ';' (SubFrom (GBP,6,(intpos 2),0))) ';' (if>0 (GBP,6,((AddTo (GBP,4,(- 1))) ';' (AddTo (GBP,7,(- 1)))),(Load ((GBP,5) := 0))))))) ';' (while>0 (GBP,7,((((((GBP,5) := (GBP,7)) ';' (AddTo (GBP,7,(- 1)))) ';' ((GBP,6) := ((intpos 2),0))) ';' (SubFrom (GBP,6,(intpos 3),0))) ';' (if>0 (GBP,6,((AddTo (GBP,3,1)) ';' (AddTo (GBP,5,(- 1)))),(Load ((GBP,7) := 0)))))))) ';' (if>0 (GBP,5,(((((((GBP,6) := ((intpos 4),0)) ';' (((intpos 4),0) := ((intpos 3),0))) ';' (((intpos 3),0) := (GBP,6))) ';' (AddTo (GBP,5,(- 2)))) ';' (AddTo (GBP,3,1))) ';' (AddTo (GBP,4,(- 1)))))))) is_halting_on s,P )
proofend;

Lm28:  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,(Initialize s))) . GBP = 0 &amp; (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 1) = s . (intpos 1) &amp; (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 2) = s . (intpos 2) &amp; (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 3) = (s . (intpos 2)) + 1 &amp; (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 4) = s . (intpos 4) &amp; (IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos 5) = (s . (intpos 4)) - (s . (intpos 2)) &amp; ( for i being Element of NAT st i >= 8 holds
(IExec ((((((GBP,5) := (GBP,4)) ';' (SubFrom (GBP,5,GBP,2))) ';' ((GBP,3) := (GBP,2))) ';' (AddTo (GBP,3,1))),P,(Initialize s))) . (intpos i) = s . (intpos i) ) )
proofend;

theorem Th13: :: SCPQSORT:10
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, p0 being Element of NAT st s . GBP = 0 &amp; s . (intpos 2) = md &amp; md >= p0 + 1 &amp; p0 >= 7 holds
( Partition is_closed_on s,P &amp; Partition is_halting_on s,P )
proofend;

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

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

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

begin

theorem :: SCPQSORT:13
for n, p0 being Element of NAT holds card (QuickSort (n,p0)) = 57 by Lm29;

theorem :: SCPQSORT:14
for p0, n being Element of NAT st p0 >= 7 holds
QuickSort (n,p0) is parahalting
proofend;

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