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

begin

definition

let f be FinSequence of INT ;
let s be State of SCMPDS ;
let m be Element of NAT ;
pred f is_FinSequence_on s,m means :Def1: :: SCPISORT:def 1
for i being Element of NAT st 1 <= i & 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 & i <= len f holds
f . i = s . (intpos (m + i)) );

Lm1: for f being FinSequence of INT
for k being Element of NAT holds f is_non_decreasing_on k,k

proof end;

theorem Th1: :: SCPISORT:1

for f being FinSequence of INT
for m, n being Element of NAT st m >= n holds
f is_non_decreasing_on m,n

proof end;

theorem Th2: :: 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 & ( for i being Element of NAT st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) ) )

proof end;

theorem :: SCPISORT:3

for s being State of SCMPDS
for n, m being Element of NAT ex f being FinSequence of INT st
( len f = n & f is_FinSequence_on s,m )

proof end;

theorem Th4: :: SCPISORT:4

for f, g being FinSequence of INT
for m, n being Element of 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 Element of 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 Th5: :: SCPISORT:5

for s1, s2 being State of SCMPDS st ( for a being Int_position holds s1 . a = s2 . a ) holds
Dstate s1 = Dstate s2

proof end;

theorem Th6: :: SCPISORT:6

for s being State of SCMPDS
for I being No-StopCode Program of SCMPDS
for j being shiftable parahalting Instruction of SCMPDS st I is_closed_on s & I is_halting_on s holds
( I ';' j is_closed_on s & I ';' j is_halting_on s )

proof end;

theorem :: SCPISORT:7

for s being State of SCMPDS
for I being No-StopCode Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS
for a being Int_position st I is_closed_on s & I is_halting_on s holds
(IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a

proof end;

theorem :: SCPISORT:8

for s being State of SCMPDS
for I being parahalting No-StopCode Program of SCMPDS
for J being shiftable Program of SCMPDS
for a being Int_position st J is_closed_on IExec I,s & J is_halting_on IExec I,s holds
(IExec (I ';' J),s) . a = (IExec J,(IExec I,s)) . a

proof end;

theorem :: SCPISORT:9

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

proof end;

theorem :: SCPISORT:10

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

proof end;

theorem :: SCPISORT:11

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

proof end;

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

proof end;

Lm3: 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))))

proof end;

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

proof end;

begin

scheme :: SCPISORT:sch 1
ForDownHalt{ P₁[ set ], F₁() -> State of SCMPDS , F₂() -> shiftable No-StopCode Program of SCMPDS , F₃() -> Int_position , F₄() -> Integer, F₅() -> Element of NAT } :

( ( P₁[F₁()] or not P₁[F₁()] ) & for-down F₃(),F₄(),F₅(),F₂() is_closed_on F₁() & for-down F₃(),F₄(),F₅(),F₂() is_halting_on F₁() )

provided

A1: F₅() > 0 and
A2: P₁[ Dstate F₁()] and
A3: for t being State of SCMPDS st P₁[ Dstate t] & t . F₃() = F₁() . F₃() & t . (DataLoc (F₁() . F₃()),F₄()) > 0 holds
( (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t) . F₃() = t . F₃() & (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t) . (DataLoc (F₁() . F₃()),F₄()) = (t . (DataLoc (F₁() . F₃()),F₄())) - F₅() & F₂() is_closed_on t & F₂() is_halting_on t & P₁[ Dstate (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t)] )

proof end;

scheme :: SCPISORT:sch 2
ForDownExec{ P₁[ set ], F₁() -> State of SCMPDS , F₂() -> shiftable No-StopCode Program of SCMPDS , F₃() -> Int_position , F₄() -> Integer, F₅() -> Element of NAT } :

( ( P₁[F₁()] or not P₁[F₁()] ) & IExec (for-down F₃(),F₄(),F₅(),F₂()),F₁() = IExec (for-down F₃(),F₄(),F₅(),F₂()),(IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),F₁()) )

provided

A1: F₅() > 0 and
A2: F₁() . (DataLoc (F₁() . F₃()),F₄()) > 0 and
A3: P₁[ Dstate F₁()] and
A4: for t being State of SCMPDS st P₁[ Dstate t] & t . F₃() = F₁() . F₃() & t . (DataLoc (F₁() . F₃()),F₄()) > 0 holds
( (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t) . F₃() = t . F₃() & (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t) . (DataLoc (F₁() . F₃()),F₄()) = (t . (DataLoc (F₁() . F₃()),F₄())) - F₅() & F₂() is_closed_on t & F₂() is_halting_on t & P₁[ Dstate (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t)] )

proof end;

scheme :: SCPISORT:sch 3
ForDownEnd{ P₁[ set ], F₁() -> State of SCMPDS , F₂() -> shiftable No-StopCode Program of SCMPDS , F₃() -> Int_position , F₄() -> Integer, F₅() -> Element of NAT } :

( ( P₁[F₁()] or not P₁[F₁()] ) & (IExec (for-down F₃(),F₄(),F₅(),F₂()),F₁()) . (DataLoc (F₁() . F₃()),F₄()) <= 0 & P₁[ Dstate (IExec (for-down F₃(),F₄(),F₅(),F₂()),F₁())] )

provided

A1: F₅() > 0 and
A2: P₁[ Dstate F₁()] and
A3: for t being State of SCMPDS st P₁[ Dstate t] & t . F₃() = F₁() . F₃() & t . (DataLoc (F₁() . F₃()),F₄()) > 0 holds
( (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t) . F₃() = t . F₃() & (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t) . (DataLoc (F₁() . F₃()),F₄()) = (t . (DataLoc (F₁() . F₃()),F₄())) - F₅() & F₂() is_closed_on t & F₂() is_halting_on t & P₁[ Dstate (IExec (F₂() ';' (AddTo F₃(),F₄(),(- F₅()))),t)] )

proof end;

theorem Th12: :: SCPISORT:12

for s being State of SCMPDS
for I being shiftable No-StopCode Program of SCMPDS
for a, x, y being Int_position
for i, c being Integer
for n being Element of NAT st n > 0 & s . x >= (s . y) + c & ( for t being State 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))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )

proof end;

theorem Th13: :: SCPISORT:13

for s being State of SCMPDS
for I being shiftable No-StopCode Program of SCMPDS
for a, x, y being Int_position
for i, c being Integer
for n being Element of NAT st n > 0 & s . x >= (s . y) + c & s . (DataLoc (s . a),i) > 0 & ( for t being State 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))),t) . a = t . a & (IExec (I ';' (AddTo a,i,(- n))),t) . (DataLoc (s . a),i) = (t . (DataLoc (s . a),i)) - n & I is_closed_on t & I is_halting_on t & (IExec (I ';' (AddTo a,i,(- n))),t) . x >= ((IExec (I ';' (AddTo a,i,(- n))),t) . y) + c ) ) holds
IExec (for-down a,i,n,I),s = IExec (for-down a,i,n,I),(IExec (I ';' (AddTo a,i,(- n))),s)

proof end;

theorem :: SCPISORT:14

for s being State of SCMPDS
for I being shiftable No-StopCode 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 & n > 0 & card I > 0 & a <> DataLoc (s . a),i & ( for t being State of SCMPDS st t . a = s . a holds
( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) = t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t ) ) holds
( for-down a,i,n,I is_closed_on s & for-down a,i,n,I is_halting_on s )

proof end;

begin

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

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

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

Lm7: for s being 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 )))),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 )))),s) . (intpos 1) = s . (intpos 1) )

proof end;

Lm8: for s being 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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),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 )))),s) . (intpos 6) = 0 ) ) )

proof end;

Lm9: for s being 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 & 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 )

proof end;

Lm10: for s being 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 ))))),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 ))))),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 ))))),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 ))))),s) . (intpos 3) = s . (intpos 3) )

proof end;

Lm11: for s being 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)),s) . GBP = 0 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 1) = (s . (intpos 1)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 2) = s . (intpos 2) & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 3) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 4) = (s . (intpos 3)) + 1 & (IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s) . (intpos 6) = (s . (intpos 1)) + 1 & ( 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)),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));

Lm12: for s being 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))),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))),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))),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))),s) . (intpos 1) = (s . (intpos 1)) + 1 & ( 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))),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 ))))),(IExec ((((AddTo GBP ,3,1) ';' (GBP ,4 := GBP ,3)) ';' (AddTo GBP ,1,1)) ';' (GBP ,6 := GBP ,1)),s)) . (intpos i) ) )

proof end;

Lm13: for s being 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 & 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 )

proof end;

Lm14: for s being 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 ))))))),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 ))))))),(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))),s)

proof end;

begin

theorem :: SCPISORT:15

for n, p0 being Element of NAT holds card (insert-sort n,p0) = 23

proof end;

theorem :: SCPISORT:16

for p0, n being Element of NAT st p0 >= 7 holds
insert-sort n,p0 is parahalting

proof end;

Lm15: for s being 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 ))))),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 ))))),(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 )))),s)

proof end;

theorem Th17: :: SCPISORT:17

for s being 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)) & 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 ))))),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 Element of NAT st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= k + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )

proof end;

Lm16: for s being State of SCMPDS
for f, g being FinSequence of INT
for p0, n being Element of 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 ))))))),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:18

for s being State of SCMPDS
for f, g being FinSequence of INT
for p0, n being Element of 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)),s,p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )

proof end;