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


definition
let f be FinSequence of INT ;
let s be State of SCMPDS;
let m be Nat;
pred f is_FinSequence_on s,m means :: SCPISORT:def 1
 for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i));
end;

:: deftheorem defines is_FinSequence_on SCPISORT:def 1 :
for f being FinSequence of INT
for s being State of SCMPDS
for m being Nat holds
( f is_FinSequence_on s,m iff for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) );

theorem Th1: :: SCPISORT:1
for s being State of SCMPDS
for n, m being Nat ex f being FinSequence of INT st
( len f = n & ( for i being Nat st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) ) )
proof end;

theorem :: SCPISORT:2
for s being State of SCMPDS
for n, m being Nat ex f being FinSequence of INT st
( len f = n & f is_FinSequence_on s,m )
proof end;

theorem Th3: :: SCPISORT:3
for f, g being FinSequence of INT
for m, n being Nat st 1 <= n & n <= len f & 1 <= m & m <= len f & len f = len g & f . m = g . n & f . n = g . m & ( for k being Nat st k <> m & k <> n & 1 <= k & k <= len f holds
f . k = g . k ) holds
f,g are_fiberwise_equipotent
proof end;

set A = NAT ;

set D = SCM-Data-Loc ;

theorem Th4: :: SCPISORT:4
for s1, s2 being State of SCMPDS st ( for a being Int_position holds s1 . a = s2 . a ) holds
Initialize s1 = Initialize s2
proof end;

theorem Th5: :: SCPISORT:5
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being halt-free Program of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( I ';' j is_closed_on s,P & I ';' j is_halting_on s,P )
proof end;

theorem :: SCPISORT:6
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for a being Int_position st I is_closed_on s,P & I is_halting_on s,P holds
(IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a
proof end;

theorem :: SCPISORT:7
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free parahalting Program of SCMPDS
for J being shiftable Program of SCMPDS
for a being Int_position st J is_closed_on IExec (I,P,s),P & J is_halting_on IExec (I,P,s),P holds
(IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a
proof end;

theorem :: SCPISORT:8
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
proof end;

theorem :: SCPISORT:9
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being parahalting Program of SCMPDS
for J being shiftable Program of SCMPDS st J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
proof end;

theorem :: SCPISORT:10
for P being Instruction-Sequence of SCMPDS
for s being State of SCMPDS
for I being Program of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( I ';' j is_closed_on s,P & I ';' j is_halting_on s,P )
proof end;

Lm1: for a being Int_position
for i being Integer
for n being Nat
for I being Program of SCMPDS holds card (stop (for-down (a,i,n,I))) = (card I) + 4
proof end;

Lm2: for a being Int_position
for i being Integer
for n being Nat
for I being Program of SCMPDS holds for-down (a,i,n,I) = ((a,i) <=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,(- n)))) ';' (goto (- ((card I) + 2))))
proof end;

Lm3: for I being Program of SCMPDS
for a being Int_position
for i being Integer
for n being Nat holds Shift ((I ';' (AddTo (a,i,(- n)))),1) c= for-down (a,i,n,I)
proof end;

scheme :: SCPISORT:sch 1
ForDownHalt{ P1[ set ], F1() -> 0 -started State of SCMPDS, F2() -> Instruction-Sequence of SCMPDS, F3() -> halt-free shiftable Program of SCMPDS, F4() -> Int_position, F5() -> Integer, F6() -> Nat } :
( for-down (F4(),F5(),F6(),F3()) is_closed_on F1(),F2() & for-down (F4(),F5(),F6(),F3()) is_halting_on F1(),F2() )
provided
A1: F6() > 0 and
A2: P1[F1()] and
A3: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F4() = F1() . F4() & t . (DataLoc ((F1() . F4()),F5())) > 0 holds
( (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4() = t . F4() & (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((F1() . F4()),F5())) = (t . (DataLoc ((F1() . F4()),F5()))) - F6() & F3() is_closed_on t,Q & F3() is_halting_on t,Q & P1[ Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
proof end;

scheme :: SCPISORT:sch 2
ForDownExec{ P1[ set ], F1() -> 0 -started State of SCMPDS, F2() -> Instruction-Sequence of SCMPDS, F3() -> halt-free shiftable Program of SCMPDS, F4() -> Int_position, F5() -> Integer, F6() -> Nat } :
IExec ((for-down (F4(),F5(),F6(),F3())),F2(),F1()) = IExec ((for-down (F4(),F5(),F6(),F3())),F2(),(Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),F2(),F1()))))
provided
A1: F6() > 0 and
A2: F1() . (DataLoc ((F1() . F4()),F5())) > 0 and
A3: P1[F1()] and
A4: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st P1[t] & t . F4() = F1() . F4() & t . (DataLoc ((F1() . F4()),F5())) > 0 holds
( (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4() = t . F4() & (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((F1() . F4()),F5())) = (t . (DataLoc ((F1() . F4()),F5()))) - F6() & F3() is_closed_on t,Q & F3() is_halting_on t,Q & P1[ Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
proof end;

scheme :: SCPISORT:sch 3
ForDownEnd{ P1[ set ], F1() -> 0 -started State of SCMPDS, F2() -> halt-free shiftable Program of SCMPDS, F3() -> Instruction-Sequence of SCMPDS, F4() -> Int_position, F5() -> Integer, F6() -> Nat } :
( (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1())) . (DataLoc ((F1() . F4()),F5())) <= 0 & P1[ Initialize (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1()))] )
provided
A1: F6() > 0 and
A2: P1[F1()] and
A3: for Q being Instruction-Sequence of SCMPDS
for t being 0 -started State of SCMPDS st P1[t] & t . F4() = F1() . F4() & t . (DataLoc ((F1() . F4()),F5())) > 0 holds
( (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4() = t . F4() & (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((F1() . F4()),F5())) = (t . (DataLoc ((F1() . F4()),F5()))) - F6() & F2() is_closed_on t,Q & F2() is_halting_on t,Q & P1[ Initialize (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
proof end;

theorem Th11: :: SCPISORT:11
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a, x, y being Int_position
for i, c being Integer
for n being Nat st n > 0 & s . x >= (s . y) + c & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
proof end;

theorem Th12: :: SCPISORT:12
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a, x, y being Int_position
for i, c being Integer
for n being Nat st n > 0 & s . x >= (s . y) + c & s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . x >= (t . y) + c & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . a = t . a & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . (DataLoc ((s . a),i)) = (t . (DataLoc ((s . a),i))) - n & I is_closed_on t,Q & I is_halting_on t,Q & (IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . x >= ((IExec ((I ';' (AddTo (a,i,(- n)))),Q,t)) . y) + c ) ) holds
IExec ((for-down (a,i,n,I)),P,s) = IExec ((for-down (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,(- n)))),P,s))))
proof end;

theorem :: SCPISORT:13
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for n being Nat st s . (DataLoc ((s . a),i)) > 0 & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st t . a = s . a holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q ) ) holds
( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P )
proof end;

:: n -> intpos 2, x1 -> intpos 3
definition
let n, p0 be Nat;
func insert-sort (n,p0) -> Program of SCMPDS equals :: SCPISORT:def 2
((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)) ';' (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) := (n - 1))) ';' ((GBP,3) := p0)) ';' (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 of SCMPDS ;
end;

:: deftheorem defines insert-sort SCPISORT:def 2 :
for n, p0 being Nat holds insert-sort (n,p0) = ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := p0)) ';' (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 j1 = AddTo (GBP,3,1);

set j2 = (GBP,4) := (GBP,3);

set j3 = AddTo (GBP,1,1);

set j4 = (GBP,6) := (GBP,1);

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

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

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

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

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

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

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

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

set TR = (((((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 IF = 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 B1 = (((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 WH = 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 J4 = (((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1));

set B2 = ((((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 FR = 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)))))))));

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

Lm5: 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 a1 = intpos 1;

set a2 = intpos 2;

set a3 = intpos 3;

set a4 = intpos 4;

set a5 = intpos 5;

set a6 = intpos 6;

Lm6: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (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))))),P,s)) . 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))))),P,s)) . (intpos 1) = s . (intpos 1) )
proof end;

Lm7: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (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))))),P,s)) . (intpos 2) = s . (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))))),P,s)) . (intpos 3) = s . (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))))),P,s)) . (intpos 6) < s . (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))))),P,s)) . (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))))),P,s)) . (intpos 6)) & ( for i being Nat st i >= 7 & i <> (s . (intpos 4)) - 1 & i <> s . (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))))),P,s)) . (intpos i) = s . (intpos i) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) > s . (DataLoc ((s . (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))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (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))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (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))))),P,s)) . (intpos 6) = (s . (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))))),P,s)) . (intpos 4) = (s . (intpos 4)) - 1 ) ) & ( s . (DataLoc ((s . (intpos 4)),(- 1))) <= s . (DataLoc ((s . (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))))),P,s)) . (DataLoc ((s . (intpos 4)),(- 1))) = s . (DataLoc ((s . (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))))),P,s)) . (DataLoc ((s . (intpos 4)),0)) = s . (DataLoc ((s . (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))))),P,s)) . (intpos 6) = 0 ) ) )
proof end;

Lm8: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . (intpos 4) >= 7 + (s . (DataLoc ((s . GBP),6))) & s . 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 s,P & 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 s,P )
proof end;

Lm9: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . (intpos 4) >= 7 + (s . (DataLoc ((s . GBP),6))) & s . 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))))))),P,s)) . 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))))))),P,s)) . (intpos 1) = s . (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))))))),P,s)) . (intpos 2) = s . (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))))))),P,s)) . (intpos 3) = s . (intpos 3) )
proof end;

Lm10: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . GBP = 0 holds
( (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . GBP = 0 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 2) = s . (intpos 2) & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 6) = (s . (intpos 1)) + 1 & ( for i being Nat st i >= 7 holds
(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos i) = s . (intpos i) ) )
proof end;

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

set B3 = (((((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)));

Lm11: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . 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)))),P,s)) . 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)))),P,s)) . (intpos 2) = (s . (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)))),P,s)) . (intpos 3) = (s . (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)))),P,s)) . (intpos 1) = (s . (intpos 1)) + 1 & ( for i being Nat st i <> 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)))),P,s)) . (intpos i) = (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))))))),P,(Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s))))) . (intpos i) ) )
proof end;

Lm12: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . 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 s,P & 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 s,P )
proof end;

Lm13: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . (intpos 3) >= (s . (intpos 1)) + 7 & s . GBP = 0 & s . (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)))))))))),P,s) = 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)))))))))),P,(Initialize (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)))),P,s))))
proof end;

theorem :: SCPISORT:14
for n, p0 being Nat holds card (insert-sort (n,p0)) = 23
proof end;

theorem :: SCPISORT:15
for n, p0 being Nat st p0 >= 7 holds
insert-sort (n,p0) is parahalting
proof end;

Lm14: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & s . (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))))))),P,s) = 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))))))),P,(Initialize (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))))),P,s))))
proof end;

theorem Th16: :: SCPISORT:16
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for f, g being FinSequence of INT
for k0, k being Nat st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & k = s . (intpos 6) & k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,k0 & g 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))))))),P,s),k0 & len f = len g & len f > k & f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k + 1 & ( for i being Nat st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Nat st 1 <= i & i <= k + 1 holds
ex j being Nat st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
proof end;

Lm15: for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for f, g being FinSequence of INT
for p0, n being Nat st s . GBP = 0 & s . (intpos 2) = n - 1 & s . (intpos 3) = p0 + 1 & s . (intpos 1) = 0 & p0 >= 6 & f is_FinSequence_on s,p0 & g 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)))))))))),P,s),p0 & len f = n & len g = n holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
proof end;

theorem :: SCPISORT:17
for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for f, g being FinSequence of INT
for p0, n being Nat st p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),P,s),p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
proof end;