:: Quick Sort on SCMPDS
:: by JingChao Chen
::
:: Received June 14, 2000
:: Copyright (c) 2000-2019 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)),(Initialize s))) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),m) holds
( DataPart sm = DataPart (IExec (I,P,(Initialize s))) & 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
((((((((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 ;

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));

:: a0=global, a1=stack, a2=stack depth

definition

let n, p0 be Nat;

func QuickSort (n,p0) -> Program of 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 ;

end;

:: deftheorem defines QuickSort SCPQSORT:def 2 :
for n, p0 being 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;

Lm6: 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

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 . (intpos 2) = md & s . (intpos 4) = me & md >= 8 & me >= 8 & 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 & (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) & (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) & (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) & ( for i being 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) ) & ( 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 & (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 & (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 ) ) & ( 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 & (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) & (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) ) ) )

proof end;