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


begin

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

:: deftheorem Def1 defines is_FinSequence_on SCPISORT:def_1_:_
 for f being FinSequence of INT
for s being State of SCMPDS
for m being Element of NAT holds
( f is_FinSequence_on s,m iff for i being Element of NAT st 1 <= i &amp; i <= len f holds
f . i = s . (intpos (m + i)) );

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

theorem :: SCPISORT:2
for s being State of SCMPDS
for n, m being Element of NAT ex f being FinSequence of INT st
( len f = n &amp; f is_FinSequence_on s,m )
proofend;

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

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

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 &amp; I is_halting_on s,P holds
( I ';' j is_closed_on s,P &amp; I ';' j is_halting_on s,P )
proofend;

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 &amp; I is_halting_on s,P holds
(IExec ((I ';' J),P,s)) . a = (IExec (J,P,(Initialize (IExec (I,P,s))))) . a
proofend;

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 &amp; 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
proofend;

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 &amp; I is_halting_on s,P holds
( I ';' J is_closed_on s,P &amp; I ';' J is_halting_on s,P )
proofend;

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 &amp; J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P &amp; I ';' J is_halting_on s,P )
proofend;

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 &amp; I is_halting_on s,P holds
( I ';' j is_closed_on s,P &amp; I ';' j is_halting_on s,P )
proofend;

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

Lm2:  for a being Int_position
for i being Integer
for n being Element of 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))))
proofend;

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

begin

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() ->  Element of NAT } :
 ( for-down (F4(),F5(),F6(),F3()) is_closed_on F1(),F2() &amp; 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] &amp; t . F4() = F1() . F4() &amp; t . (DataLoc ((F1() . F4()),F5())) > 0 holds
( (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4() = t . F4() &amp; (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((F1() . F4()),F5())) = (t . (DataLoc ((F1() . F4()),F5()))) - F6() &amp; F3() is_closed_on t,Q &amp; F3() is_halting_on t,Q &amp; P1[ Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
proofend;

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() ->  Element of 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] &amp; t . F4() = F1() . F4() &amp; t . (DataLoc ((F1() . F4()),F5())) > 0 holds
( (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4() = t . F4() &amp; (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((F1() . F4()),F5())) = (t . (DataLoc ((F1() . F4()),F5()))) - F6() &amp; F3() is_closed_on t,Q &amp; F3() is_halting_on t,Q &amp; P1[ Initialize (IExec ((F3() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
proofend;

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() ->  Element of NAT } :
 ( (IExec ((for-down (F4(),F5(),F6(),F2())),F3(),F1())) . (DataLoc ((F1() . F4()),F5())) <= 0 &amp; 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] &amp; t . F4() = F1() . F4() &amp; t . (DataLoc ((F1() . F4()),F5())) > 0 holds
( (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . F4() = t . F4() &amp; (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t)) . (DataLoc ((F1() . F4()),F5())) = (t . (DataLoc ((F1() . F4()),F5()))) - F6() &amp; F2() is_closed_on t,Q &amp; F2() is_halting_on t,Q &amp; P1[ Initialize (IExec ((F2() ';' (AddTo (F4(),F5(),(- F6())))),Q,t))] )
proofend;

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

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

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 Element of NAT st s . (DataLoc ((s . a),i)) > 0 &amp; n > 0 &amp; a <> DataLoc ((s . a),i) &amp; ( 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 &amp; (IExec (I,Q,t)) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) &amp; I is_closed_on t,Q &amp; I is_halting_on t,Q ) ) holds
( for-down (a,i,n,I) is_closed_on s,P &amp; for-down (a,i,n,I) is_halting_on s,P )
proofend;

begin

:: n -> intpos 2, x1 -> intpos 3
definition
let n, p0 be Element of 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 Element of 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
proofend;

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

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)) &amp; s . GBP = 0 &amp; 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 &amp; (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) )
proofend;

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

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))) &amp; 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 &amp; 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 )
proofend;

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))) &amp; 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 &amp; (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) &amp; (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) &amp; (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) )
proofend;

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 &amp; (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 &amp; (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),P,s)) . (intpos 2) = s . (intpos 2) &amp; (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 &amp; (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 &amp; (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 &amp; ( for i being Element of 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) ) )
proofend;

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 &amp; 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 &amp; (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 &amp; (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 &amp; (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 &amp; ( for i being Element of 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) ) )
proofend;

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

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

begin

theorem :: SCPISORT:14
for n, p0 being Element of NAT holds card (insert-sort (n,p0)) = 23
proofend;

theorem :: SCPISORT:15
for p0, n being Element of NAT st p0 >= 7 holds
insert-sort (n,p0) is parahalting
proofend;

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

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 Element of NAT st s . (intpos 4) >= 7 + (s . (intpos 6)) &amp; s . GBP = 0 &amp; k = s . (intpos 6) &amp; k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 &amp; f is_FinSequence_on s,k0 &amp; 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 &amp; len f = len g &amp; len f > k &amp; f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent &amp; g is_non_decreasing_on 1,k + 1 &amp; ( for i being Element of NAT st i > k + 1 &amp; i <= len f holds
f . i = g . i ) &amp; ( for i being Element of NAT st 1 <= i &amp; i <= k + 1 holds
ex j being Element of NAT st
( 1 <= j &amp; j <= k + 1 &amp; g . i = f . j ) ) )
proofend;

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 Element of NAT st s . GBP = 0 &amp; s . (intpos 2) = n - 1 &amp; s . (intpos 3) = p0 + 1 &amp; s . (intpos 1) = 0 &amp; p0 >= 6 &amp; f is_FinSequence_on s,p0 &amp; 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 &amp; len f = n &amp; len g = n holds
( f,g are_fiberwise_equipotent &amp; g is_non_decreasing_on 1,n )
proofend;

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 Element of NAT st p0 >= 6 &amp; len f = n &amp; len g = n &amp; f is_FinSequence_on s,p0 &amp; g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),P,s),p0 holds
( f,g are_fiberwise_equipotent &amp; g is_non_decreasing_on 1,n )
proofend;