:: SCPQSORT semantic presentation

Lemma1: for b1 being State of SCMPDS
for b2, b3 being shiftable Program-block
for b4 being Nat holds (b2 ';' (Goto b4)) ';' b3 is shiftable
proof end;

registration
let c1, c2 be shiftable Program-block;
let c3 be Int_position ;
let c4 be Integer;
cluster if>0 a3,a4,a1,a2 -> shiftable ;
correctness
coherence
if>0 c3,c4,c1,c2 is shiftable;
proof end;
end;

theorem Th1: :: SCPQSORT:1
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being shiftable Program-block
for b4, b5 being Int_position
for b6 being Integer st b1 . (DataLoc (b1 . b4),b6) > 0 & b2 is_closed_on b1 & b2 is_halting_on b1 holds
(IExec (if>0 b4,b6,b2,b3),b1) . b5 = (IExec b2,b1) . b5
proof end;

set c1 = the Instruction-Locations of SCMPDS ;

set c2 = SCM-Data-Loc ;

Lemma3: for b1 being Int_position
for b2 being Integer
for b3 being Program-block holds while>0 b1,b2,b3 = (b1,b2 <=0_goto ((card b3) + 2)) ';' (b3 ';' (goto (- ((card b3) + 1))))
proof end;

Lemma4: for b1 being Program-block
for b2 being Int_position
for b3 being Integer holds Shift b1,1 c= while>0 b2,b3,b1
proof end;

theorem Th2: :: SCPQSORT:2
for b1, b2 being State of SCMPDS
for b3 being shiftable No-StopCode Program-block
for b4 being Int_position
for b5 being Integer
for b6 being Nat st card b3 > 0 & b3 is_closed_on b1 & b3 is_halting_on b1 & b1 . (DataLoc (b1 . b4),b5) > 0 & b6 = (LifeSpan (b1 +* (Initialized (stop b3)))) + 2 & b2 = (Computation (b1 +* (Initialized (stop (while>0 b4,b5,b3))))) . b6 holds
( b2 | SCM-Data-Loc = (IExec b3,b1) | SCM-Data-Loc & b2 +* (Initialized (stop (while>0 b4,b5,b3))) = b2 )
proof end;

theorem Th3: :: SCPQSORT:3
for b1 being State of SCMPDS
for b2 being Program-block st ( for b3 being State of SCMPDS st b3 | SCM-Data-Loc = b1 | SCM-Data-Loc holds
b2 is_halting_on b3 ) holds
b2 is_closed_on b1
proof end;

theorem Th4: :: SCPQSORT:4
for b1, b2, b3, b4 being Instruction of SCMPDS holds card (((b1 ';' b2) ';' b3) ';' b4) = 4
proof end;

theorem Th5: :: SCPQSORT:5
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3, b4, b5 being Int_position
for b6, b7 being Integer st card b2 > 0 & b1 . b4 >= b7 + (b1 . (DataLoc (b1 . b3),b6)) & ( for b8 being State of SCMPDS st b8 . b4 >= b7 + (b8 . (DataLoc (b1 . b3),b6)) & b8 . b5 = b1 . b5 & b8 . b3 = b1 . b3 & b8 . (DataLoc (b1 . b3),b6) > 0 holds
( (IExec b2,b8) . b3 = b8 . b3 & b2 is_closed_on b8 & b2 is_halting_on b8 & (IExec b2,b8) . (DataLoc (b1 . b3),b6) < b8 . (DataLoc (b1 . b3),b6) & (IExec b2,b8) . b4 >= b7 + ((IExec b2,b8) . (DataLoc (b1 . b3),b6)) & (IExec b2,b8) . b5 = b8 . b5 ) ) holds
( while>0 b3,b6,b2 is_closed_on b1 & while>0 b3,b6,b2 is_halting_on b1 & ( b1 . (DataLoc (b1 . b3),b6) > 0 implies IExec (while>0 b3,b6,b2),b1 = IExec (while>0 b3,b6,b2),(IExec b2,b1) ) )
proof end;

theorem Th6: :: SCPQSORT:6
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3, b4, b5 being Int_position
for b6, b7 being Integer st card b2 > 0 & b1 . b4 >= b7 & ( for b8 being State of SCMPDS st b8 . b4 >= b7 & b8 . b5 = b1 . b5 & b8 . b3 = b1 . b3 & b8 . (DataLoc (b1 . b3),b6) > 0 holds
( (IExec b2,b8) . b3 = b8 . b3 & b2 is_closed_on b8 & b2 is_halting_on b8 & (IExec b2,b8) . (DataLoc (b1 . b3),b6) < b8 . (DataLoc (b1 . b3),b6) & (IExec b2,b8) . b4 >= b7 & (IExec b2,b8) . b5 = b8 . b5 ) ) holds
( while>0 b3,b6,b2 is_closed_on b1 & while>0 b3,b6,b2 is_halting_on b1 & ( b1 . (DataLoc (b1 . b3),b6) > 0 implies IExec (while>0 b3,b6,b2),b1 = IExec (while>0 b3,b6,b2),(IExec b2,b1) ) )
proof end;

theorem Th7: :: SCPQSORT:7
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3, b4, b5, b6, b7 being Int_position
for b8, b9, b10 being Integer st card b2 > 0 & b1 . b7 = ((b1 . b6) - b9) + (b1 . b4) & b10 <= (b1 . b6) - b9 & ( for b11 being State of SCMPDS st b11 . b7 = ((b11 . b6) - b9) + (b11 . b4) & b10 <= (b11 . b6) - b9 & b11 . b5 = b1 . b5 & b11 . b3 = b1 . b3 & b11 . (DataLoc (b1 . b3),b8) > 0 holds
( (IExec b2,b11) . b3 = b11 . b3 & b2 is_closed_on b11 & b2 is_halting_on b11 & (IExec b2,b11) . (DataLoc (b1 . b3),b8) < b11 . (DataLoc (b1 . b3),b8) & (IExec b2,b11) . b7 = (((IExec b2,b11) . b6) - b9) + ((IExec b2,b11) . b4) & b10 <= ((IExec b2,b11) . b6) - b9 & (IExec b2,b11) . b5 = b11 . b5 ) ) holds
( while>0 b3,b8,b2 is_closed_on b1 & while>0 b3,b8,b2 is_halting_on b1 & ( b1 . (DataLoc (b1 . b3),b8) > 0 implies IExec (while>0 b3,b8,b2),b1 = IExec (while>0 b3,b8,b2),(IExec b2,b1) ) )
proof end;

theorem Th8: :: SCPQSORT:8
for b1 being FinSequence of INT
for b2, b3, b4, b5 being Nat st b2 <= b4 & b4 <= b5 & b3 = b4 - 1 & b1 is_non_decreasing_on b2,b3 & b1 is_non_decreasing_on b4 + 1,b5 & ( for b6 being Nat st b2 <= b6 & b6 < b4 holds
b1 . b6 <= b1 . b4 ) & ( for b6 being Nat st b4 < b6 & b6 <= b5 holds
b1 . b4 <= b1 . b6 ) holds
b1 is_non_decreasing_on b2,b5
proof end;

theorem Th9: :: SCPQSORT:9
for b1, b2 being FinSequence
for b3 being set st b3 in dom b2 & b1,b2 are_fiberwise_equipotent holds
ex b4 being set st
( b4 in dom b2 & b1 . b3 = b2 . b4 )
proof end;

theorem Th10: :: SCPQSORT:10
for b1, b2, b3 being FinSequence holds
( b1,b2 are_fiberwise_equipotent iff b3 ^ b1,b3 ^ b2 are_fiberwise_equipotent )
proof end;

theorem Th11: :: SCPQSORT:11
for b1, b2 being FinSequence
for b3, b4, b5 being Nat st b1,b2 are_fiberwise_equipotent & b3 <= b4 & b4 <= len b1 & ( for b6 being Nat st 1 <= b6 & b6 <= b3 holds
b1 . b6 = b2 . b6 ) & ( for b6 being Nat st b4 < b6 & b6 <= len b1 holds
b1 . b6 = b2 . b6 ) & b3 < b5 & b5 <= b4 holds
ex b6 being Nat st
( b3 < b6 & b6 <= b4 & b1 . b5 = b2 . b6 )
proof end;

Lemma15: for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4, b5 being Integer
for b6, b7 being FinSequence of INT
for b8, b9, b10 being Nat st card b2 > 0 & b1 . b3 = b5 & len b6 = b9 & len b7 = b9 & b6 is_FinSequence_on b1,b8 & b7 is_FinSequence_on IExec (while>0 b3,b4,b2),b1,b8 & 1 = b1 . (DataLoc b5,b4) & b10 = (b8 + b9) + 1 & b8 + 1 = b1 . (intpos b10) & b8 + b9 = b1 . (intpos (b10 + 1)) & ( for b11 being State of SCMPDS
for b12, b13 being FinSequence of INT
for b14, b15, b16, b17 being Nat st b11 . b3 = b5 & (2 * b14) + 1 = b11 . (DataLoc b5,b4) & b15 = ((b8 + b9) + (2 * b14)) + 1 & b8 + b16 = b11 . (intpos b15) & b8 + b17 = b11 . (intpos (b15 + 1)) & ( ( 1 <= b16 & b17 <= b9 ) or b16 >= b17 ) holds
( b2 is_closed_on b11 & b2 is_halting_on b11 & (IExec b2,b11) . b3 = b11 . b3 & ( for b18 being Nat st 1 <= b18 & b18 < (2 * b14) + 1 holds
(IExec b2,b11) . (intpos ((b8 + b9) + b18)) = b11 . (intpos ((b8 + b9) + b18)) ) & ( b16 >= b17 implies ( (IExec b2,b11) . (DataLoc b5,b4) = (2 * b14) - 1 & ( for b18 being Nat st 1 <= b18 & b18 <= b9 holds
(IExec b2,b11) . (intpos (b8 + b18)) = b11 . (intpos (b8 + b18)) ) ) ) & ( b16 < b17 implies ( (IExec b2,b11) . (DataLoc b5,b4) = (2 * b14) + 3 & ( for b18 being Nat st ( ( 1 <= b18 & b18 < b16 ) or ( b17 < b18 & b18 <= b9 ) ) holds
(IExec b2,b11) . (intpos (b8 + b18)) = b11 . (intpos (b8 + b18)) ) & ex b18 being Nat st
( b16 <= b18 & b18 <= b17 & b8 + b16 = (IExec b2,b11) . (intpos b15) & (b8 + b18) - 1 = (IExec b2,b11) . (intpos (b15 + 1)) & (b8 + b18) + 1 = (IExec b2,b11) . (intpos (b15 + 2)) & b8 + b17 = (IExec b2,b11) . (intpos (b15 + 3)) & ( for b19 being Nat st b16 <= b19 & b19 < b18 holds
(IExec b2,b11) . (intpos (b8 + b19)) <= (IExec b2,b11) . (intpos (b8 + b18)) ) & ( for b19 being Nat st b18 < b19 & b19 <= b17 holds
(IExec b2,b11) . (intpos (b8 + b19)) >= (IExec b2,b11) . (intpos (b8 + b18)) ) ) ) ) & ( b12 is_FinSequence_on b11,b8 & b13 is_FinSequence_on IExec b2,b11,b8 & len b12 = b9 & len b13 = b9 implies b12,b13 are_fiberwise_equipotent ) ) ) holds
( while>0 b3,b4,b2 is_halting_on b1 & b6,b7 are_fiberwise_equipotent & b7 is_non_decreasing_on 1,b9 )
proof end;

Lemma16: for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4, b5 being Integer
for b6, b7, b8 being Nat st card b2 > 0 & b1 . b3 = b5 & 1 = b1 . (DataLoc b5,b4) & b8 = (b6 + b7) + 1 & b6 + 1 = b1 . (intpos b8) & b6 + b7 = b1 . (intpos (b8 + 1)) & ( for b9 being State of SCMPDS
for b10, b11 being FinSequence of INT
for b12, b13, b14, b15 being Nat st b9 . b3 = b5 & (2 * b12) + 1 = b9 . (DataLoc b5,b4) & b13 = ((b6 + b7) + (2 * b12)) + 1 & b6 + b14 = b9 . (intpos b13) & b6 + b15 = b9 . (intpos (b13 + 1)) & ( ( 1 <= b14 & b15 <= b7 ) or b14 >= b15 ) holds
( b2 is_closed_on b9 & b2 is_halting_on b9 & (IExec b2,b9) . b3 = b9 . b3 & ( for b16 being Nat st 1 <= b16 & b16 < (2 * b12) + 1 holds
(IExec b2,b9) . (intpos ((b6 + b7) + b16)) = b9 . (intpos ((b6 + b7) + b16)) ) & ( b14 >= b15 implies ( (IExec b2,b9) . (DataLoc b5,b4) = (2 * b12) - 1 & ( for b16 being Nat st 1 <= b16 & b16 <= b7 holds
(IExec b2,b9) . (intpos (b6 + b16)) = b9 . (intpos (b6 + b16)) ) ) ) & ( b14 < b15 implies ( (IExec b2,b9) . (DataLoc b5,b4) = (2 * b12) + 3 & ( for b16 being Nat st ( ( 1 <= b16 & b16 < b14 ) or ( b15 < b16 & b16 <= b7 ) ) holds
(IExec b2,b9) . (intpos (b6 + b16)) = b9 . (intpos (b6 + b16)) ) & ex b16 being Nat st
( b14 <= b16 & b16 <= b15 & b6 + b14 = (IExec b2,b9) . (intpos b13) & (b6 + b16) - 1 = (IExec b2,b9) . (intpos (b13 + 1)) & (b6 + b16) + 1 = (IExec b2,b9) . (intpos (b13 + 2)) & b6 + b15 = (IExec b2,b9) . (intpos (b13 + 3)) & ( for b17 being Nat st b14 <= b17 & b17 < b16 holds
(IExec b2,b9) . (intpos (b6 + b17)) <= (IExec b2,b9) . (intpos (b6 + b16)) ) & ( for b17 being Nat st b16 < b17 & b17 <= b15 holds
(IExec b2,b9) . (intpos (b6 + b17)) >= (IExec b2,b9) . (intpos (b6 + b16)) ) ) ) ) & ( b10 is_FinSequence_on b9,b6 & b11 is_FinSequence_on IExec b2,b9,b6 & len b10 = b7 & len b11 = b7 implies b10,b11 are_fiberwise_equipotent ) ) ) holds
while>0 b3,b4,b2 is_halting_on b1
proof end;

Lemma17: for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4, b5 being Integer
for b6, b7, b8 being Nat st card b2 > 0 & b1 . b3 = b5 & 1 = b1 . (DataLoc b5,b4) & b8 = (b6 + b7) + 1 & b6 + 1 = b1 . (intpos b8) & b6 + b7 = b1 . (intpos (b8 + 1)) & ( for b9 being State of SCMPDS
for b10, b11 being FinSequence of INT
for b12, b13, b14, b15 being Nat st b9 . b3 = b5 & (2 * b12) + 1 = b9 . (DataLoc b5,b4) & b13 = ((b6 + b7) + (2 * b12)) + 1 & b6 + b14 = b9 . (intpos b13) & b6 + b15 = b9 . (intpos (b13 + 1)) & ( ( 1 <= b14 & b15 <= b7 ) or b14 >= b15 ) holds
( b2 is_closed_on b9 & b2 is_halting_on b9 & (IExec b2,b9) . b3 = b9 . b3 & ( for b16 being Nat st 1 <= b16 & b16 < (2 * b12) + 1 holds
(IExec b2,b9) . (intpos ((b6 + b7) + b16)) = b9 . (intpos ((b6 + b7) + b16)) ) & ( b14 >= b15 implies ( (IExec b2,b9) . (DataLoc b5,b4) = (2 * b12) - 1 & ( for b16 being Nat st 1 <= b16 & b16 <= b7 holds
(IExec b2,b9) . (intpos (b6 + b16)) = b9 . (intpos (b6 + b16)) ) ) ) & ( b14 < b15 implies ( (IExec b2,b9) . (DataLoc b5,b4) = (2 * b12) + 3 & ( for b16 being Nat st ( ( 1 <= b16 & b16 < b14 ) or ( b15 < b16 & b16 <= b7 ) ) holds
(IExec b2,b9) . (intpos (b6 + b16)) = b9 . (intpos (b6 + b16)) ) & ex b16 being Nat st
( b14 <= b16 & b16 <= b15 & b6 + b14 = (IExec b2,b9) . (intpos b13) & (b6 + b16) - 1 = (IExec b2,b9) . (intpos (b13 + 1)) & (b6 + b16) + 1 = (IExec b2,b9) . (intpos (b13 + 2)) & b6 + b15 = (IExec b2,b9) . (intpos (b13 + 3)) & ( for b17 being Nat st b14 <= b17 & b17 < b16 holds
(IExec b2,b9) . (intpos (b6 + b17)) <= (IExec b2,b9) . (intpos (b6 + b16)) ) & ( for b17 being Nat st b16 < b17 & b17 <= b15 holds
(IExec b2,b9) . (intpos (b6 + b17)) >= (IExec b2,b9) . (intpos (b6 + b16)) ) ) ) ) & ( b10 is_FinSequence_on b9,b6 & b11 is_FinSequence_on IExec b2,b9,b6 & len b10 = b7 & len b11 = b7 implies b10,b11 are_fiberwise_equipotent ) ) ) holds
( while>0 b3,b4,b2 is_halting_on b1 & while>0 b3,b4,b2 is_closed_on b1 )
proof end;

definition
func Partition -> Program-block 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-block ;
end;

:: deftheorem Def1 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);

definition
let c3, c4 be Nat;
set c5 = c4 + c3;
func QuickSort c1,c2 -> Program-block equals :: SCPQSORT:def 2
((((GBP := 0) ';' (SBP := 1)) ';' (SBP ,(a2 + a1) := (a2 + 1))) ';' (SBP ,((a2 + a1) + 1) := (a2 + a1))) ';' (while>0 GBP ,1,(((GBP ,2 := SBP ,((a2 + a1) + 1)) ';' (SubFrom GBP ,2,SBP ,(a2 + a1))) ';' (if>0 GBP ,2,((((GBP ,2 := SBP ,(a2 + a1)) ';' (GBP ,4 := SBP ,((a2 + a1) + 1))) ';' Partition ) ';' ((((((SBP ,((a2 + a1) + 3) := SBP ,((a2 + a1) + 1)) ';' (SBP ,((a2 + a1) + 1) := GBP ,4)) ';' (SBP ,((a2 + a1) + 2) := GBP ,4)) ';' (AddTo SBP ,((a2 + a1) + 1),(- 1))) ';' (AddTo SBP ,((a2 + a1) + 2),1)) ';' (AddTo GBP ,1,2))),(Load (AddTo GBP ,1,(- 2))))));
coherence
((((GBP := 0) ';' (SBP := 1)) ';' (SBP ,(c4 + c3) := (c4 + 1))) ';' (SBP ,((c4 + c3) + 1) := (c4 + c3))) ';' (while>0 GBP ,1,(((GBP ,2 := SBP ,((c4 + c3) + 1)) ';' (SubFrom GBP ,2,SBP ,(c4 + c3))) ';' (if>0 GBP ,2,((((GBP ,2 := SBP ,(c4 + c3)) ';' (GBP ,4 := SBP ,((c4 + c3) + 1))) ';' Partition ) ';' ((((((SBP ,((c4 + c3) + 3) := SBP ,((c4 + c3) + 1)) ';' (SBP ,((c4 + c3) + 1) := GBP ,4)) ';' (SBP ,((c4 + c3) + 2) := GBP ,4)) ';' (AddTo SBP ,((c4 + c3) + 1),(- 1))) ';' (AddTo SBP ,((c4 + c3) + 2),1)) ';' (AddTo GBP ,1,2))),(Load (AddTo GBP ,1,(- 2)))))) is Program-block ;
end;

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

set c3 = GBP ,7 := GBP ,5;

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

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

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

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

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

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

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

set c11 = ((((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 c12 = 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 c13 = GBP ,5 := GBP ,7;

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

set c15 = GBP ,6 := (intpos 2),0;

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

set c17 = AddTo GBP ,3,1;

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

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

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

set c21 = ((((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 c22 = 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 c23 = GBP ,5 := GBP ,4;

set c24 = SubFrom GBP ,5,GBP ,2;

set c25 = GBP ,3 := GBP ,2;

set c26 = AddTo GBP ,3,1;

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

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

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

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

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

set c32 = AddTo GBP ,3,1;

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

set c34 = 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 c35 = ((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 c36 = 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 c37 = GBP ,6 := (intpos 4),0;

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

set c39 = (intpos 2),0 := GBP ,6;

set c40 = intpos 1;

set c41 = intpos 2;

set c42 = intpos 3;

set c43 = intpos 4;

set c44 = intpos 5;

set c45 = intpos 6;

set c46 = intpos 7;

Lemma18: 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;

Lemma19: for b1 being State of SCMPDS
for b2, b3 being Nat st b1 . (intpos 2) = b2 & b1 . (intpos 4) = b3 & b2 >= 8 & b3 >= 8 & b1 . GBP = 0 & b1 . (intpos 5) > 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)))),b1) . 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)))),b1) . (intpos 1) = b1 . (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)))),b1) . (intpos 2) = b1 . (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)))),b1) . (intpos 3) = b1 . (intpos 3) & ( for b4 being Nat st b4 >= 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)))),b1) . (intpos b4) = b1 . (intpos b4) ) & ( b1 . (intpos b2) < b1 . (intpos b3) 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)))),b1) . (intpos 5) = (b1 . (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)))),b1) . (intpos 4) = (b1 . (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)))),b1) . (intpos 7) = (b1 . (intpos 5)) - 1 ) ) & ( b1 . (intpos b2) >= b1 . (intpos b3) 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)))),b1) . (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)))),b1) . (intpos 4) = b1 . (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)))),b1) . (intpos 7) = b1 . (intpos 5) ) ) )
proof end;

Lemma20: for b1 being State of SCMPDS
for b2, b3 being Nat st b1 . GBP = 0 & b1 . (intpos 5) > 0 & b1 . (intpos 4) = b2 + (b1 . (intpos 5)) & b2 >= 8 & b1 . (intpos 2) = b3 & b3 >= 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))))),b1) . GBP = 0 & (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))))),b1) . (intpos 1) = b1 . (intpos 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))))),b1) . (intpos 5) = 0 & (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))))),b1) . (intpos 2) = b1 . (intpos 2) & (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))))),b1) . (intpos 3) = b1 . (intpos 3) & ( for b4 being Nat st b4 >= 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))))),b1) . (intpos b4) = b1 . (intpos b4) ) & ex b4 being Nat st
( b4 = (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))))),b1) . (intpos 7) & (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))))),b1) . (intpos 4) = b2 + b4 & b4 <= b1 . (intpos 5) & ( for b5 being Nat st b2 + b4 < b5 & b5 <= b1 . (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))))),b1) . (intpos b3) < (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))))),b1) . (intpos b5) ) & ( b4 = 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))))),b1) . (intpos b3) >= (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))))),b1) . (intpos (b2 + b4)) ) ) )
proof end;

Lemma21: for b1 being State of SCMPDS
for b2, b3 being Nat st b1 . GBP = 0 & b1 . (intpos 5) > 0 & b1 . (intpos 4) = b2 + (b1 . (intpos 5)) & b2 >= 8 & b1 . (intpos 2) = b3 & b3 >= 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 b1 & 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 b1 )
proof end;

Lemma22: 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
proof end;

Lemma23: 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
proof end;

Lemma24: 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
proof end;

Lemma25: for b1 being State of SCMPDS
for b2, b3 being Nat st b1 . (intpos 2) = b2 & b1 . (intpos 3) = b3 & b2 >= 8 & b3 >= 8 & b1 . GBP = 0 & b1 . (intpos 7) > 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)))),b1) . GBP = 0 & (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)))),b1) . (intpos 1) = b1 . (intpos 1) & (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)))),b1) . (intpos 2) = b1 . (intpos 2) & (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)))),b1) . (intpos 4) = b1 . (intpos 4) & ( for b4 being Nat st b4 >= 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)))),b1) . (intpos b4) = b1 . (intpos b4) ) & ( b1 . (intpos b2) > b1 . (intpos b3) 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)))),b1) . (intpos 7) = (b1 . (intpos 7)) - 1 & (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)))),b1) . (intpos 3) = (b1 . (intpos 3)) + 1 & (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)))),b1) . (intpos 5) = (b1 . (intpos 7)) - 1 ) ) & ( b1 . (intpos b2) <= b1 . (intpos b3) 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)))),b1) . (intpos 7) = 0 & (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)))),b1) . (intpos 3) = b1 . (intpos 3) & (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)))),b1) . (intpos 5) = b1 . (intpos 7) ) ) )
proof end;

Lemma26: for b1 being State of SCMPDS
for b2, b3 being Nat st b1 . GBP = 0 & b1 . (intpos 7) > 0 & (b1 . (intpos 3)) + (b1 . (intpos 7)) = b2 & b1 . (intpos 3) >= 8 & b1 . (intpos 2) = b3 & b3 >= 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))))),b1) . GBP = 0 & (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))))),b1) . (intpos 1) = b1 . (intpos 1) & (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))))),b1) . (intpos 7) = 0 & (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))))),b1) . (intpos 2) = b1 . (intpos 2) & (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))))),b1) . (intpos 4) = b1 . (intpos 4) & ( for b4 being Nat st b4 >= 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))))),b1) . (intpos b4) = b1 . (intpos b4) ) & ex b4, b5 being Nat st
( b4 = (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))))),b1) . (intpos 5) & (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))))),b1) . (intpos 3) = b5 & b5 + b4 = b2 & b4 <= b1 . (intpos 7) & ( for b6 being Nat st b1 . (intpos 3) <= b6 & b6 < b5 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))))),b1) . (intpos b3) > (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))))),b1) . (intpos b6) ) & ( b4 = 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))))),b1) . (intpos b3) <= (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))))),b1) . (intpos b5) ) ) )
proof end;

Lemma27: for b1 being State of SCMPDS
for b2 being Nat st b1 . GBP = 0 & b1 . (intpos 7) > 0 & b1 . (intpos 3) >= 8 & b1 . (intpos 2) = b2 & b2 >= 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 b1 & 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 b1 )
proof end;

Lemma28: 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
proof end;

Lemma29: 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
proof end;

theorem Th12: :: SCPQSORT:12
card Partition = 38
proof end;

Lemma31: for b1 being State of SCMPDS
for b2, b3 being Nat st b1 . GBP = 0 & b1 . (intpos 5) > 0 & b1 . (intpos 3) = b2 & b1 . (intpos 4) = b3 & b2 > 6 & b3 > 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)))),b1) . GBP = 0 & (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)))),b1) . (intpos 1) = b1 . (intpos 1) & (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)))),b1) . (intpos 2) = b1 . (intpos 2) & (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)))),b1) . (intpos b2) = b1 . (intpos b3) & (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)))),b1) . (intpos b3) = b1 . (intpos b2) & (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)))),b1) . (intpos 3) = (b1 . (intpos 3)) + 1 & (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)))),b1) . (intpos 4) = (b1 . (intpos 4)) - 1 & (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)))),b1) . (intpos 5) = (b1 . (intpos 5)) - 2 & ( for b4 being Nat st b4 >= 8 & b4 <> b2 & b4 <> b3 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)))),b1) . (intpos b4) = b1 . (intpos b4) ) )
proof end;

Lemma32: for b1 being State of SCMPDS
for b2, b3 being Nat st b1 . GBP = 0 & b1 . (intpos 5) > 0 & b1 . (intpos 4) = b3 + (b1 . (intpos 5)) & b3 = (b1 . (intpos 3)) - 1 & b1 . (intpos 2) = b2 & b2 >= 8 & b2 <= b3 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 b1 & ((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 b1 & (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))))),b1) . GBP = 0 & (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))))),b1) . (intpos 1) = b1 . (intpos 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))))),b1) . (intpos 2) = b2 & (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))))),b1) . (intpos 3) >= b1 . (intpos 3) & (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))))),b1) . (intpos 4) <= b1 . (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))))),b1) . (intpos 4) >= b3 & (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))))),b1) . (intpos 5) < b1 . (intpos 5) & (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))))),b1) . (intpos 5) >= - 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))))),b1) . (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))))),b1) . (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))))),b1) . (intpos 5)) & ex b4, b5 being Nat st
( b4 = ((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))))),b1) . (intpos 3)) - 1 & b5 = ((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))))),b1) . (intpos 4)) + 1 & ( for b6 being Nat st b6 >= 8 & b6 <> b4 & b6 <> b5 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))))),b1) . (intpos b6) = b1 . (intpos b6) ) & ( ( (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))))),b1) . (intpos b4) = b1 . (intpos b4) & (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))))),b1) . (intpos b5) = b1 . (intpos b5) ) or ( b4 >= b1 . (intpos 3) & b5 <= b1 . (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))))),b1) . (intpos b4) = b1 . (intpos b5) & (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))))),b1) . (intpos b5) = b1 . (intpos b4) ) ) & ( for b6 being Nat st b1 . (intpos 3) <= b6 & b6 <= b4 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))))),b1) . (intpos b2) >= (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))))),b1) . (intpos b6) ) & ( for b6 being Nat st b5 <= b6 & b6 <= b1 . (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))))),b1) . (intpos b2) <= (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))))),b1) . (intpos b6) ) ) )
proof end;

Lemma33: for b1 being Integer st b1 >= - 1 & b1 <= 0 & not b1 = - 1 holds
b1 = 0
proof end;

Lemma34: for b1, b2 being Integer
for b3, b4, b5 being Nat st b1 >= - 1 & b1 <= 0 & b4 = b2 + 1 & b2 = b3 + b1 & b5 < b4 holds
b5 <= b3
proof end;

Lemma35: for b1, b2 being Integer
for b3, b4 being Nat st b1 >= - 1 & b4 = b2 + 1 & b2 = b3 + b1 holds
b3 <= b4
proof end;

Lemma36: for b1, b2 being State of SCMPDS
for b3, b4, b5, b6 being Nat
for b7, b8 being FinSequence of INT st b7 is_FinSequence_on b1,b3 & b8 is_FinSequence_on b2,b3 & len b7 = b6 & len b8 = b6 & ( for b9 being Nat st b9 >= b3 + 1 & b9 <> b4 & b9 <> b5 holds
b2 . (intpos b9) = b1 . (intpos b9) ) & ( ( b2 . (intpos b4) = b1 . (intpos b4) & b2 . (intpos b5) = b1 . (intpos b5) ) or ( b4 >= b3 + 1 & b5 >= b3 + 1 & b4 <= b3 + b6 & b5 <= b3 + b6 & b2 . (intpos b4) = b1 . (intpos b5) & b2 . (intpos b5) = b1 . (intpos b4) ) ) holds
b7,b8 are_fiberwise_equipotent
proof end;

Lemma37: for b1, b2 being State of SCMPDS
for b3, b4, b5 being Nat
for b6, b7 being Integer st ( for b8 being Nat st b8 >= b3 & b8 <> b4 & b8 <> b5 holds
b2 . (intpos b8) = b1 . (intpos b8) ) & b4 <= b5 & ( ( b2 . (intpos b4) = b1 . (intpos b4) & b2 . (intpos b5) = b1 . (intpos b5) ) or ( b6 <= b4 & b5 <= b7 & b2 . (intpos b4) = b1 . (intpos b5) & b2 . (intpos b5) = b1 . (intpos b4) ) ) holds
for b8 being Nat st b8 >= b3 & ( b8 < b6 or b8 > b7 ) holds
b2 . (intpos b8) = b1 . (intpos b8)
proof end;

Lemma38: for b1 being Nat
for b2 being State of SCMPDS
for b3, b4, b5 being Nat
for b6, b7 being FinSequence of INT st b2 . GBP = 0 & b2 . (intpos 5) > 0 & b2 . (intpos 4) = b4 + (b2 . (intpos 5)) & b4 = (b2 . (intpos 3)) - 1 & b2 . (intpos 2) = b3 & b3 >= b5 + 1 & b3 <= b4 & b5 + 1 <= b2 . (intpos 3) & b2 . (intpos 4) <= b5 + b1 & b6 is_FinSequence_on b2,b5 & b7 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)))))),b2,b5 & b5 >= 7 & len b6 = b1 & len b7 = b1 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)))))),b2) . GBP = 0 & (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)))))),b2) . (intpos 1) = b2 . (intpos 1) & (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)))))),b2) . (intpos 2) = b3 & (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)))))),b2) . (intpos 4) >= b3 & (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)))))),b2) . (intpos 4) <= b2 . (intpos 4) & b6,b7 are_fiberwise_equipotent & ( for b8 being Nat st b2 . (intpos 3) <= b8 & b8 <= (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)))))),b2) . (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)))))),b2) . (intpos b3) >= (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)))))),b2) . (intpos b8) ) & ( for b8 being 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)))))),b2) . (intpos 4) < b8 & b8 <= b2 . (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)))))),b2) . (intpos b3) <= (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)))))),b2) . (intpos b8) ) & ( for b8 being Nat st b8 >= b5 + 1 & ( b8 < b2 . (intpos 3) or b8 > b2 . (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)))))),b2) . (intpos b8) = b2 . (intpos b8) ) )
proof end;

Lemma39: for b1 being State of SCMPDS
for b2, b3, b4 being Nat st b1 . GBP = 0 & b1 . (intpos 5) > 0 & b1 . (intpos 4) = b3 + (b1 . (intpos 5)) & b3 = (b1 . (intpos 3)) - 1 & b1 . (intpos 2) = b2 & b2 >= b4 + 1 & b2 <= b3 & b4 >= 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 b1 & 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 b1 )
proof end;

Lemma40: for b1 being State of SCMPDS st b1 . GBP = 0 holds
( (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),b1) . GBP = 0 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),b1) . (intpos 1) = b1 . (intpos 1) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),b1) . (intpos 2) = b1 . (intpos 2) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),b1) . (intpos 3) = (b1 . (intpos 2)) + 1 & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),b1) . (intpos 4) = b1 . (intpos 4) & (IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),b1) . (intpos 5) = (b1 . (intpos 4)) - (b1 . (intpos 2)) & ( for b2 being Nat st b2 >= 8 holds
(IExec ((((GBP ,5 := GBP ,4) ';' (SubFrom GBP ,5,GBP ,2)) ';' (GBP ,3 := GBP ,2)) ';' (AddTo GBP ,3,1)),b1) . (intpos b2) = b1 . (intpos b2) ) )
proof end;

theorem Th13: :: SCPQSORT:13
for b1 being State of SCMPDS
for b2, b3 being Nat st b1 . GBP = 0 & (b1 . (intpos 4)) - (b1 . (intpos 2)) > 0 & b1 . (intpos 2) = b2 & b2 >= b3 + 1 & b3 >= 7 holds
( Partition is_closed_on b1 & Partition is_halting_on b1 )
proof end;

theorem Th14: :: SCPQSORT:14
for b1 being State of SCMPDS
for b2, b3, b4 being Nat
for b5, b6 being FinSequence of INT st b1 . GBP = 0 & (b1 . (intpos 4)) - (b1 . (intpos 2)) > 0 & b1 . (intpos 2) = b2 & b2 >= b3 + 1 & b1 . (intpos 4) <= b3 + b4 & b3 >= 7 & b5 is_FinSequence_on b1,b3 & len b5 = b4 & b6 is_FinSequence_on IExec Partition ,b1,b3 & len b6 = b4 holds
( (IExec Partition ,b1) . GBP = 0 & (IExec Partition ,b1) . (intpos 1) = b1 . (intpos 1) & b5,b6 are_fiberwise_equipotent & ex b7 being Nat st
( b7 = (IExec Partition ,b1) . (intpos 4) & b2 <= b7 & b7 <= b1 . (intpos 4) & ( for b8 being Nat st b2 <= b8 & b8 < b7 holds
(IExec Partition ,b1) . (intpos b7) >= (IExec Partition ,b1) . (intpos b8) ) & ( for b8 being Nat st b7 < b8 & b8 <= b1 . (intpos 4) holds
(IExec Partition ,b1) . (intpos b7) <= (IExec Partition ,b1) . (intpos b8) ) & ( for b8 being Nat st b8 >= b3 + 1 & ( b8 < b1 . (intpos 2) or b8 > b1 . (intpos 4) ) holds
(IExec Partition ,b1) . (intpos b8) = b1 . (intpos b8) ) ) )
proof end;

theorem Th15: :: SCPQSORT:15
( Partition is No-StopCode & Partition is shiftable ) ;

Lemma43: for b1 being State of SCMPDS
for b2, b3 being Nat holds
( card (QuickSort b3,b2) = 57 & ( b2 >= 7 implies ( QuickSort b3,b2 is_halting_on b1 & ex b4, b5 being FinSequence of INT st
( len b4 = b3 & b4 is_FinSequence_on b1,b2 & len b5 = b3 & b5 is_FinSequence_on IExec (QuickSort b3,b2),b1,b2 & b4,b5 are_fiberwise_equipotent & b5 is_non_decreasing_on 1,b3 ) ) ) )
proof end;

theorem Th16: :: SCPQSORT:16
for b1, b2 being Nat holds card (QuickSort b1,b2) = 57 by Lemma43;

theorem Th17: :: SCPQSORT:17
for b1, b2 being Nat st b1 >= 7 holds
QuickSort b2,b1 is parahalting
proof end;

theorem Th18: :: SCPQSORT:18
for b1 being State of SCMPDS
for b2, b3 being Nat st b2 >= 7 holds
ex b4, b5 being FinSequence of INT st
( len b4 = b3 & b4 is_FinSequence_on b1,b2 & len b5 = b3 & b5 is_FinSequence_on IExec (QuickSort b3,b2),b1,b2 & b4,b5 are_fiberwise_equipotent & b5 is_non_decreasing_on 1,b3 ) by Lemma43;