:: SCPISORT semantic presentation

definition
let c1 be FinSequence of INT ;
let c2 be State of SCMPDS ;
let c3 be Nat;
pred c1 is_FinSequence_on c2,c3 means :Def1: :: SCPISORT:def 1
for b1 being Nat st 1 <= b1 & b1 <= len a1 holds
a1 . b1 = a2 . (intpos (a3 + b1));
end;

:: deftheorem Def1 defines is_FinSequence_on SCPISORT:def 1 :
for b1 being FinSequence of INT
for b2 being State of SCMPDS
for b3 being Nat holds
( b1 is_FinSequence_on b2,b3 iff for b4 being Nat st 1 <= b4 & b4 <= len b1 holds
b1 . b4 = b2 . (intpos (b3 + b4)) );

Lemma2: for b1 being FinSequence of INT
for b2 being Nat holds b1 is_non_decreasing_on b2,b2
proof end;

theorem Th1: :: SCPISORT:1
for b1 being FinSequence of INT
for b2, b3 being Nat st b2 >= b3 holds
b1 is_non_decreasing_on b2,b3
proof end;

theorem Th2: :: SCPISORT:2
for b1 being State of SCMPDS
for b2, b3 being Nat ex b4 being FinSequence of INT st
( len b4 = b2 & ( for b5 being Nat st 1 <= b5 & b5 <= len b4 holds
b4 . b5 = b1 . (intpos (b3 + b5)) ) )
proof end;

theorem Th3: :: SCPISORT:3
for b1 being State of SCMPDS
for b2, b3 being Nat ex b4 being FinSequence of INT st
( len b4 = b2 & b4 is_FinSequence_on b1,b3 )
proof end;

theorem Th4: :: SCPISORT:4
for b1, b2 being FinSequence of INT
for b3, b4 being Nat st 1 <= b4 & b4 <= len b1 & 1 <= b3 & b3 <= len b1 & len b1 = len b2 & b1 . b3 = b2 . b4 & b1 . b4 = b2 . b3 & ( for b5 being Nat st b5 <> b3 & b5 <> b4 & 1 <= b5 & b5 <= len b1 holds
b1 . b5 = b2 . b5 ) holds
b1,b2 are_fiberwise_equipotent
proof end;

set c1 = the Instruction-Locations of SCMPDS ;

set c2 = SCM-Data-Loc ;

theorem Th5: :: SCPISORT:5
for b1, b2 being State of SCMPDS st ( for b3 being Int_position holds b1 . b3 = b2 . b3 ) holds
Dstate b1 = Dstate b2
proof end;

theorem Th6: :: SCPISORT:6
for b1 being State of SCMPDS
for b2 being No-StopCode Program-block
for b3 being shiftable parahalting Instruction of SCMPDS st b2 is_closed_on b1 & b2 is_halting_on b1 holds
( b2 ';' b3 is_closed_on b1 & b2 ';' b3 is_halting_on b1 )
proof end;

theorem Th7: :: SCPISORT:7
for b1 being State of SCMPDS
for b2 being No-StopCode Program-block
for b3 being parahalting shiftable Program-block
for b4 being Int_position st b2 is_closed_on b1 & b2 is_halting_on b1 holds
(IExec (b2 ';' b3),b1) . b4 = (IExec b3,(IExec b2,b1)) . b4
proof end;

theorem Th8: :: SCPISORT:8
for b1 being State of SCMPDS
for b2 being parahalting No-StopCode Program-block
for b3 being shiftable Program-block
for b4 being Int_position st b3 is_closed_on IExec b2,b1 & b3 is_halting_on IExec b2,b1 holds
(IExec (b2 ';' b3),b1) . b4 = (IExec b3,(IExec b2,b1)) . b4
proof end;

theorem Th9: :: SCPISORT:9
for b1 being State of SCMPDS
for b2 being Program-block
for b3 being parahalting shiftable Program-block st b2 is_closed_on b1 & b2 is_halting_on b1 holds
( b2 ';' b3 is_closed_on b1 & b2 ';' b3 is_halting_on b1 )
proof end;

theorem Th10: :: SCPISORT:10
for b1 being State of SCMPDS
for b2 being parahalting Program-block
for b3 being shiftable Program-block st b3 is_closed_on IExec b2,b1 & b3 is_halting_on IExec b2,b1 holds
( b2 ';' b3 is_closed_on b1 & b2 ';' b3 is_halting_on b1 )
proof end;

theorem Th11: :: SCPISORT:11
for b1 being State of SCMPDS
for b2 being Program-block
for b3 being shiftable parahalting Instruction of SCMPDS st b2 is_closed_on b1 & b2 is_halting_on b1 holds
( b2 ';' b3 is_closed_on b1 & b2 ';' b3 is_halting_on b1 )
proof end;

Lemma8: for b1 being Int_position
for b2 being Integer
for b3 being Nat
for b4 being Program-block holds card (stop (for-down b1,b2,b3,b4)) = (card b4) + 4
proof end;

Lemma9: for b1 being Int_position
for b2 being Integer
for b3 being Nat
for b4 being Program-block holds for-down b1,b2,b3,b4 = (b1,b2 <=0_goto ((card b4) + 3)) ';' ((b4 ';' (AddTo b1,b2,(- b3))) ';' (goto (- ((card b4) + 2))))
proof end;

Lemma10: for b1 being Program-block
for b2 being Int_position
for b3 being Integer
for b4 being Nat holds Shift (b1 ';' (AddTo b2,b3,(- b4))),1 c= for-down b2,b3,b4,b1
proof end;

scheme :: SCPISORT:sch 1
s1{ P1[ set ], F1() -> State of SCMPDS , F2() -> shiftable No-StopCode Program-block, F3() -> Int_position , F4() -> Integer, F5() -> Nat } :
( ( P1[F1()] or not P1[F1()] ) & for-down F3(),F4(),F5(),F2() is_closed_on F1() & for-down F3(),F4(),F5(),F2() is_halting_on F1() )
provided
E11: F5() > 0 and
E12: P1[ Dstate F1()] and
E13: for b1 being State of SCMPDS st P1[ Dstate b1] & b1 . F3() = F1() . F3() & b1 . (DataLoc (F1() . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1) . F3() = b1 . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1) . (DataLoc (F1() . F3()),F4()) = (b1 . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on b1 & F2() is_halting_on b1 & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1)] )
proof end;

scheme :: SCPISORT:sch 2
s2{ P1[ set ], F1() -> State of SCMPDS , F2() -> shiftable No-StopCode Program-block, F3() -> Int_position , F4() -> Integer, F5() -> Nat } :
( ( P1[F1()] or not P1[F1()] ) & IExec (for-down F3(),F4(),F5(),F2()),F1() = IExec (for-down F3(),F4(),F5(),F2()),(IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),F1()) )
provided
E11: F5() > 0 and
E12: F1() . (DataLoc (F1() . F3()),F4()) > 0 and
E13: P1[ Dstate F1()] and
E14: for b1 being State of SCMPDS st P1[ Dstate b1] & b1 . F3() = F1() . F3() & b1 . (DataLoc (F1() . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1) . F3() = b1 . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1) . (DataLoc (F1() . F3()),F4()) = (b1 . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on b1 & F2() is_halting_on b1 & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1)] )
proof end;

scheme :: SCPISORT:sch 3
s3{ P1[ set ], F1() -> State of SCMPDS , F2() -> shiftable No-StopCode Program-block, F3() -> Int_position , F4() -> Integer, F5() -> Nat } :
( ( P1[F1()] or not P1[F1()] ) & (IExec (for-down F3(),F4(),F5(),F2()),F1()) . (DataLoc (F1() . F3()),F4()) <= 0 & P1[ Dstate (IExec (for-down F3(),F4(),F5(),F2()),F1())] )
provided
E11: F5() > 0 and
E12: P1[ Dstate F1()] and
E13: for b1 being State of SCMPDS st P1[ Dstate b1] & b1 . F3() = F1() . F3() & b1 . (DataLoc (F1() . F3()),F4()) > 0 holds
( (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1) . F3() = b1 . F3() & (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1) . (DataLoc (F1() . F3()),F4()) = (b1 . (DataLoc (F1() . F3()),F4())) - F5() & F2() is_closed_on b1 & F2() is_halting_on b1 & P1[ Dstate (IExec (F2() ';' (AddTo F3(),F4(),(- F5()))),b1)] )
proof end;

theorem Th12: :: SCPISORT:12
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
for b8 being Nat st b8 > 0 & b1 . b4 >= (b1 . b5) + b7 & ( for b9 being State of SCMPDS st b9 . b4 >= (b9 . b5) + b7 & b9 . b3 = b1 . b3 & b9 . (DataLoc (b1 . b3),b6) > 0 holds
( (IExec (b2 ';' (AddTo b3,b6,(- b8))),b9) . b3 = b9 . b3 & (IExec (b2 ';' (AddTo b3,b6,(- b8))),b9) . (DataLoc (b1 . b3),b6) = (b9 . (DataLoc (b1 . b3),b6)) - b8 & b2 is_closed_on b9 & b2 is_halting_on b9 & (IExec (b2 ';' (AddTo b3,b6,(- b8))),b9) . b4 >= ((IExec (b2 ';' (AddTo b3,b6,(- b8))),b9) . b5) + b7 ) ) holds
( for-down b3,b6,b8,b2 is_closed_on b1 & for-down b3,b6,b8,b2 is_halting_on b1 )
proof end;

theorem Th13: :: SCPISORT:13
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
for b8 being Nat st b8 > 0 & b1 . b4 >= (b1 . b5) + b7 & b1 . (DataLoc (b1 . b3),b6) > 0 & ( for b9 being State of SCMPDS st b9 . b4 >= (b9 . b5) + b7 & b9 . b3 = b1 . b3 & b9 . (DataLoc (b1 . b3),b6) > 0 holds
( (IExec (b2 ';' (AddTo b3,b6,(- b8))),b9) . b3 = b9 . b3 & (IExec (b2 ';' (AddTo b3,b6,(- b8))),b9) . (DataLoc (b1 . b3),b6) = (b9 . (DataLoc (b1 . b3),b6)) - b8 & b2 is_closed_on b9 & b2 is_halting_on b9 & (IExec (b2 ';' (AddTo b3,b6,(- b8))),b9) . b4 >= ((IExec (b2 ';' (AddTo b3,b6,(- b8))),b9) . b5) + b7 ) ) holds
IExec (for-down b3,b6,b8,b2),b1 = IExec (for-down b3,b6,b8,b2),(IExec (b2 ';' (AddTo b3,b6,(- b8))),b1)
proof end;

theorem Th14: :: SCPISORT:14
for b1 being State of SCMPDS
for b2 being shiftable No-StopCode Program-block
for b3 being Int_position
for b4 being Integer
for b5 being Nat st b1 . (DataLoc (b1 . b3),b4) > 0 & b5 > 0 & card b2 > 0 & b3 <> DataLoc (b1 . b3),b4 & ( for b6 being State of SCMPDS st b6 . b3 = b1 . b3 holds
( (IExec b2,b6) . b3 = b6 . b3 & (IExec b2,b6) . (DataLoc (b1 . b3),b4) = b6 . (DataLoc (b1 . b3),b4) & b2 is_closed_on b6 & b2 is_halting_on b6 ) ) holds
( for-down b3,b4,b5,b2 is_closed_on b1 & for-down b3,b4,b5,b2 is_halting_on b1 )
proof end;

definition
let c3, c4 be Nat;
func insert-sort c1,c2 -> Program-block equals :: SCPISORT:def 2
((((GBP := 0) ';' (GBP ,1 := 0)) ';' (GBP ,2 := (a1 - 1))) ';' (GBP ,3 := a2)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))));
coherence
((((GBP := 0) ';' (GBP ,1 := 0)) ';' (GBP ,2 := (c3 - 1))) ';' (GBP ,3 := c4)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))))) is Program-block ;
end;

:: deftheorem Def2 defines insert-sort SCPISORT:def 2 :
for b1, b2 being Nat holds insert-sort b1,b2 = ((((GBP := 0) ';' (GBP ,1 := 0)) ';' (GBP ,2 := (b1 - 1))) ';' (GBP ,3 := b2)) ';' (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))));

set c3 = AddTo GBP ,3,1;

set c4 = GBP ,4 := GBP ,3;

set c5 = AddTo GBP ,1,1;

set c6 = GBP ,6 := GBP ,1;

set c7 = GBP ,5 := (intpos 4),(- 1);

set c8 = SubFrom GBP ,5,(intpos 4),0;

set c9 = GBP ,5 := (intpos 4),(- 1);

set c10 = (intpos 4),(- 1) := (intpos 4),0;

set c11 = (intpos 4),0 := GBP ,5;

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

set c13 = AddTo GBP ,6,(- 1);

set c14 = Load (GBP ,6 := 0);

set c15 = ((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1));

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

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

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

set c19 = (((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1);

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

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

Lemma13: card (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))) = 10
proof end;

Lemma14: card (((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) = 16
proof end;

set c22 = intpos 1;

set c23 = intpos 2;

set c24 = intpos 3;

set c25 = intpos 4;

set c26 = intpos 5;

set c27 = intpos 6;

Lemma15: for b1 being State of SCMPDS st b1 . (intpos 4) >= 7 + (b1 . (intpos 6)) & b1 . GBP = 0 & b1 . (intpos 6) > 0 holds
( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . GBP = 0 & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 1) = b1 . (intpos 1) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 2) = b1 . (intpos 2) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 3) = b1 . (intpos 3) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 6) < b1 . (intpos 6) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 4) >= 7 + ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 6)) & ( for b2 being Nat st b2 >= 7 & b2 <> (b1 . (intpos 4)) - 1 & b2 <> b1 . (intpos 4) holds
(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos b2) = b1 . (intpos b2) ) & ( b1 . (DataLoc (b1 . (intpos 4)),(- 1)) > b1 . (DataLoc (b1 . (intpos 4)),0) implies ( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (DataLoc (b1 . (intpos 4)),(- 1)) = b1 . (DataLoc (b1 . (intpos 4)),0) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (DataLoc (b1 . (intpos 4)),0) = b1 . (DataLoc (b1 . (intpos 4)),(- 1)) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 6) = (b1 . (intpos 6)) - 1 & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 4) = (b1 . (intpos 4)) - 1 ) ) & ( b1 . (DataLoc (b1 . (intpos 4)),(- 1)) <= b1 . (DataLoc (b1 . (intpos 4)),0) implies ( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (DataLoc (b1 . (intpos 4)),(- 1)) = b1 . (DataLoc (b1 . (intpos 4)),(- 1)) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (DataLoc (b1 . (intpos 4)),0) = b1 . (DataLoc (b1 . (intpos 4)),0) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1) . (intpos 6) = 0 ) ) )
proof end;

Lemma16: for b1 being State of SCMPDS st b1 . (intpos 4) >= 7 + (b1 . (DataLoc (b1 . GBP ),6)) & b1 . GBP = 0 holds
( while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))) is_closed_on b1 & while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))) is_halting_on b1 )
proof end;

Lemma17: for b1 being State of SCMPDS st b1 . (intpos 4) >= 7 + (b1 . (DataLoc (b1 . GBP ),6)) & b1 . GBP = 0 holds
( (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),b1) . GBP = 0 & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),b1) . (intpos 1) = b1 . (intpos 1) & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),b1) . (intpos 2) = b1 . (intpos 2) & (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),b1) . (intpos 3) = b1 . (intpos 3) )
proof end;

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

set c28 = AddTo GBP ,2,(- 1);

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

Lemma19: for b1 being State of SCMPDS st b1 . (intpos 3) >= (b1 . (intpos 1)) + 7 & b1 . GBP = 0 holds
( (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),b1) . GBP = 0 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),b1) . (intpos 2) = (b1 . (intpos 2)) - 1 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),b1) . (intpos 3) = (b1 . (intpos 3)) + 1 & (IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),b1) . (intpos 1) = (b1 . (intpos 1)) + 1 & ( for b2 being Nat st b2 <> 2 holds
(IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),b1) . (intpos b2) = (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),b1)) . (intpos b2) ) )
proof end;

Lemma20: for b1 being State of SCMPDS st b1 . (intpos 3) >= (b1 . (intpos 1)) + 7 & b1 . GBP = 0 holds
( for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) is_closed_on b1 & for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) is_halting_on b1 )
proof end;

Lemma21: for b1 being State of SCMPDS st b1 . (intpos 3) >= (b1 . (intpos 1)) + 7 & b1 . GBP = 0 & b1 . (intpos 2) > 0 holds
IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))))),b1 = IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))))),(IExec ((((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))))) ';' (AddTo GBP ,2,(- 1))),b1)
proof end;

theorem Th15: :: SCPISORT:15
for b1, b2 being Nat holds card (insert-sort b1,b2) = 23
proof end;

theorem Th16: :: SCPISORT:16
for b1, b2 being Nat st b1 >= 7 holds
insert-sort b2,b1 is parahalting
proof end;

Lemma22: for b1 being State of SCMPDS st b1 . (intpos 4) >= 7 + (b1 . (intpos 6)) & b1 . GBP = 0 & b1 . (intpos 6) > 0 holds
IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),b1 = IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0)))),b1)
proof end;

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

theorem Th17: :: SCPISORT:17
for b1 being State of SCMPDS
for b2, b3 being FinSequence of INT
for b4, b5 being Nat st b1 . (intpos 4) >= 7 + (b1 . (intpos 6)) & b1 . GBP = 0 & b5 = b1 . (intpos 6) & b4 = ((b1 . (intpos 4)) - (b1 . (intpos 6))) - 1 & b2 is_FinSequence_on b1,b4 & b3 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))),b1,b4 & len b2 = len b3 & len b2 > b5 & b2 is_non_decreasing_on 1,b5 holds
( b2,b3 are_fiberwise_equipotent & b3 is_non_decreasing_on 1,b5 + 1 & ( for b6 being Nat st b6 > b5 + 1 & b6 <= len b2 holds
b2 . b6 = b3 . b6 ) & ( for b6 being Nat st 1 <= b6 & b6 <= b5 + 1 holds
ex b7 being Nat st
( 1 <= b7 & b7 <= b5 + 1 & b3 . b6 = b2 . b7 ) ) )
proof end;

Lemma24: for b1 being State of SCMPDS
for b2, b3 being FinSequence of INT
for b4, b5 being Nat st b1 . GBP = 0 & b1 . (intpos 2) = b5 - 1 & b1 . (intpos 3) = b4 + 1 & b1 . (intpos 1) = 0 & b4 >= 6 & b2 is_FinSequence_on b1,b4 & b3 is_FinSequence_on IExec (for-down GBP ,2,1,(((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)) ';' (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0)) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0)) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0))))))),b1,b4 & len b2 = b5 & len b3 = b5 holds
( b2,b3 are_fiberwise_equipotent & b3 is_non_decreasing_on 1,b5 )
proof end;

theorem Th18: :: SCPISORT:18
for b1 being State of SCMPDS
for b2, b3 being FinSequence of INT
for b4, b5 being Nat st b4 >= 6 & len b2 = b5 & len b3 = b5 & b2 is_FinSequence_on b1,b4 & b3 is_FinSequence_on IExec (insert-sort b5,(b4 + 1)),b1,b4 holds
( b2,b3 are_fiberwise_equipotent & b3 is_non_decreasing_on 1,b5 )
proof end;