:: Insert Sort on SCM+FSA
:: by JingChao Chen
::
:: Received March 13, 1999
:: Copyright (c) 1999 Association of Mizar Users

registration

let i be good Instruction of SCM+FSA ;
cluster Macro i -> good ;
coherence
Macro i is good

proof end;

end;

registration

let a be read-write Int-Location ;
let b be Int-Location ;
cluster AddTo a,b -> good ;
coherence
AddTo a,b is good

proof end;

end;

theorem :: SCMISORT:1

canceled;

theorem :: SCMISORT:2

for p being preProgram of SCM+FSA
for l being Instruction-Location of SCM+FSA
for ic being Instruction of SCM+FSA st l in dom p & ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds
UsedIntLoc p = UsedIntLoc (p +* (l .--> ic))

proof end;

theorem :: SCMISORT:3

for a being Int-Location
for I being Program of SCM+FSA holds (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto (insloc ((card I) + 4))

proof end;

theorem :: SCMISORT:4

for p being preProgram of SCM+FSA
for l being Instruction-Location of SCM+FSA
for ic being Instruction of SCM+FSA st l in dom p & ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedInt*Loc pc = UsedInt*Loc ic ) holds
UsedInt*Loc p = UsedInt*Loc (p +* (l .--> ic))

proof end;

theorem :: SCMISORT:5

canceled;

theorem Th6: :: SCMISORT:6

for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0 ) = 1 & IC s = insloc 0 holds
s +* I = s +* (Initialized I)

proof end;

theorem Th7: :: SCMISORT:7

for I being Program of SCM+FSA
for a, b being Int-Location st I does_not_destroy b holds
while>0 a,I does_not_destroy b

proof end;

theorem :: SCMISORT:8

canceled;

theorem :: SCMISORT:9

canceled;

theorem Th10: :: SCMISORT:10

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_halting_on Initialize s holds
for a being Int-Location holds (IExec I,s) . a = (Computation ((Initialize s) +* (I +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize s) +* (I +* (Start-At (insloc 0 )))))) . a

proof end;

theorem Th11: :: SCMISORT:11

for s1, s2 being State of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialized I c= s1 & Initialized I c= s2 & s1,s2 equal_outside NAT holds
for k being Element of NAT holds
( Computation s1,k, Computation s2,k equal_outside NAT & CurInstr (Computation s1,k) = CurInstr (Computation s2,k) )

proof end;

theorem Th12: :: SCMISORT:12

for s1, s2 being State of SCM+FSA
for I being InitHalting Program of SCM+FSA st Initialized I c= s1 & Initialized I c= s2 & s1,s2 equal_outside NAT holds
( LifeSpan s1 = LifeSpan s2 & Result s1, Result s2 equal_outside NAT )

proof end;

theorem Th13: :: SCMISORT:13

for I being Program of SCM+FSA
for f being FinSeq-Location holds not f in dom I

proof end;

theorem Th14: :: SCMISORT:14

for I being Program of SCM+FSA
for a being Int-Location holds not a in dom I

proof end;

theorem :: SCMISORT:15

canceled;

theorem Th16: :: SCMISORT:16

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
( while>0 a,I is_halting_onInit s & while>0 a,I is_closed_onInit s )

proof end;

theorem :: SCMISORT:17

for a being Int-Location
for I being Program of SCM+FSA
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_onInit s & I is_halting_onInit s & k < LifeSpan (s +* (Initialized I)) & IC (Computation (s +* (Initialized (while>0 a,I))),(1 + k)) = (IC (Computation (s +* (Initialized I)),k)) + 4 & DataPart (Computation (s +* (Initialized (while>0 a,I))),(1 + k)) = DataPart (Computation (s +* (Initialized I)),k) holds
( IC (Computation (s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = (IC (Computation (s +* (Initialized I)),(k + 1))) + 4 & DataPart (Computation (s +* (Initialized (while>0 a,I))),((1 + k) + 1)) = DataPart (Computation (s +* (Initialized I)),(k + 1)) )

proof end;

theorem :: SCMISORT:18

for a being Int-Location
for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_onInit s & I is_halting_onInit s & IC (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = (IC (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I))))) + 4 holds
CurInstr (Computation (s +* (Initialized (while>0 a,I))),(1 + (LifeSpan (s +* (Initialized I))))) = goto (insloc ((card I) + 4))

proof end;

theorem Th19: :: SCMISORT:19

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I) ) )

proof end;

theorem :: SCMISORT:20

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
for k being Element of NAT st k <= (LifeSpan (s +* (Initialized I))) + 3 holds
IC (Computation (s +* (Initialized (while>0 a,I))),k) in dom (while>0 a,I)

proof end;

theorem Th21: :: SCMISORT:21

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st I is_closed_onInit s & I is_halting_onInit s & s . a > 0 holds
( IC (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = insloc 0 & DataPart (Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)) = DataPart (Computation (s +* (Initialized I)),(LifeSpan (s +* (Initialized I)))) )

proof end;

theorem :: SCMISORT:22

for s being State of SCM+FSA
for I being InitHalting Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialized (while>0 a,I)) & k = (LifeSpan (s +* (Initialized I))) + 3 & IC (Computation s2,k) = insloc 0 & ( for b being Int-Location holds (Computation s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,s) . f ) )

proof end;

definition

let s be State of SCM+FSA ;
let I be Program of SCM+FSA ;
let a be read-write Int-Location ;
deffunc H₁( Nat, Element of product the Object-Kind of SCM+FSA ) -> Element of product the Object-Kind of SCM+FSA = Computation ($2 +* (Initialized (while>0 a,I))),((LifeSpan ($2 +* (Initialized I))) + 3);
func StepWhile>0 a,s,I -> Function of NAT ,(product the Object-Kind of SCM+FSA ) means :Def1: :: SCMISORT:def 1
( it . 0 = s & ( for i being Nat holds it . (i + 1) = Computation ((it . i) +* (Initialized (while>0 a,I))),((LifeSpan ((it . i) +* (Initialized I))) + 3) ) );
existence
ex b₁ being Function of NAT ,(product the Object-Kind of SCM+FSA ) st
( b₁ . 0 = s & ( for i being Nat holds b₁ . (i + 1) = Computation ((b₁ . i) +* (Initialized (while>0 a,I))),((LifeSpan ((b₁ . i) +* (Initialized I))) + 3) ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT ,(product the Object-Kind of SCM+FSA ) st b₁ . 0 = s & ( for i being Nat holds b₁ . (i + 1) = Computation ((b₁ . i) +* (Initialized (while>0 a,I))),((LifeSpan ((b₁ . i) +* (Initialized I))) + 3) ) & b₂ . 0 = s & ( for i being Nat holds b₂ . (i + 1) = Computation ((b₂ . i) +* (Initialized (while>0 a,I))),((LifeSpan ((b₂ . i) +* (Initialized I))) + 3) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines StepWhile>0 SCMISORT:def 1 :

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location
for b₄ being Function of NAT ,(product the Object-Kind of SCM+FSA ) holds
( b₄ = StepWhile>0 a,s,I iff ( b₄ . 0 = s & ( for i being Nat holds b₄ . (i + 1) = Computation ((b₄ . i) +* (Initialized (while>0 a,I))),((LifeSpan ((b₄ . i) +* (Initialized I))) + 3) ) ) );

theorem :: SCMISORT:23

canceled;

theorem :: SCMISORT:24

canceled;

theorem :: SCMISORT:25

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location
for k being Element of NAT holds (StepWhile>0 a,s,I) . (k + 1) = (StepWhile>0 a,((StepWhile>0 a,s,I) . k),I) . 1

proof end;

theorem Th26: :: SCMISORT:26

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA holds (StepWhile>0 a,s,I) . (0 + 1) = Computation (s +* (Initialized (while>0 a,I))),((LifeSpan (s +* (Initialized I))) + 3)

proof end;

theorem Th27: :: SCMISORT:27

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA
for k, n being Element of NAT st IC ((StepWhile>0 a,s,I) . k) = insloc 0 & (StepWhile>0 a,s,I) . k = Computation (s +* (Initialized (while>0 a,I))),n & ((StepWhile>0 a,s,I) . k) . (intloc 0 ) = 1 holds
( (StepWhile>0 a,s,I) . k = ((StepWhile>0 a,s,I) . k) +* (Initialized (while>0 a,I)) & (StepWhile>0 a,s,I) . (k + 1) = Computation (s +* (Initialized (while>0 a,I))),(n + ((LifeSpan (((StepWhile>0 a,s,I) . k) +* (Initialized I))) + 3)) )

proof end;

theorem :: SCMISORT:28

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Element of NAT holds
( ( f . ((StepWhile>0 a,s,I) . k) <> 0 implies ( f . ((StepWhile>0 a,s,I) . (k + 1)) < f . ((StepWhile>0 a,s,I) . k) & I is_closed_onInit (StepWhile>0 a,s,I) . k & I is_halting_onInit (StepWhile>0 a,s,I) . k ) ) & ((StepWhile>0 a,s,I) . (k + 1)) . (intloc 0 ) = 1 & ( f . ((StepWhile>0 a,s,I) . k) = 0 implies ((StepWhile>0 a,s,I) . k) . a <= 0 ) & ( ((StepWhile>0 a,s,I) . k) . a <= 0 implies f . ((StepWhile>0 a,s,I) . k) = 0 ) ) holds
( while>0 a,I is_halting_onInit s & while>0 a,I is_closed_onInit s )

proof end;

theorem Th29: :: SCMISORT:29

for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st ( for s being State of SCM+FSA st s . a > 0 holds
(IExec I,s) . a < s . a ) holds
while>0 a,I is InitHalting

proof end;

theorem Th30: :: SCMISORT:30

for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st ( for s being State of SCM+FSA holds
( (IExec I,s) . a < s . a or (IExec I,s) . a <= 0 ) ) holds
while>0 a,I is InitHalting

proof end;

theorem :: SCMISORT:31

for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st ex f being Function of (product the Object-Kind of SCM+FSA ),INT st
for s, t being State of SCM+FSA holds
( ( f . s > 0 implies f . (IExec I,s) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) holds
while>0 a,I is InitHalting

proof end;

theorem Th32: :: SCMISORT:32

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec (while>0 a,I),s) = DataPart (Initialize s)

proof end;

theorem Th33: :: SCMISORT:33

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & while>0 a,I is InitHalting holds
DataPart (IExec (while>0 a,I),s) = DataPart (IExec (while>0 a,I),(IExec I,s))

proof end;

theorem Th34: :: SCMISORT:34

for s being State of SCM+FSA
for I being Program of SCM+FSA
for f being FinSeq-Location
for a being read-write Int-Location st s . a <= 0 holds
(IExec (while>0 a,I),s) . f = s . f

proof end;

theorem Th35: :: SCMISORT:35

for s being State of SCM+FSA
for I being Program of SCM+FSA
for b being Int-Location
for a being read-write Int-Location st s . a <= 0 holds
(IExec (while>0 a,I),s) . b = (Initialize s) . b

proof end;

theorem Th36: :: SCMISORT:36

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for f being FinSeq-Location
for a being read-write Int-Location st s . a > 0 & while>0 a,I is InitHalting holds
(IExec (while>0 a,I),s) . f = (IExec (while>0 a,I),(IExec I,s)) . f

proof end;

theorem Th37: :: SCMISORT:37

for s being State of SCM+FSA
for I being good InitHalting Program of SCM+FSA
for b being Int-Location
for a being read-write Int-Location st s . a > 0 & while>0 a,I is InitHalting holds
(IExec (while>0 a,I),s) . b = (IExec (while>0 a,I),(IExec I,s)) . b

proof end;

set a0 = intloc 0 ;

set a1 = intloc 1;

set a2 = intloc 2;

set a3 = intloc 3;

set a4 = intloc 4;

set a5 = intloc 5;

set a6 = intloc 6;

set initializeWorkMem = (((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ));

definition

let f be FinSeq-Location ;
func insert-sort f -> Program of SCM+FSA equals :: SCMISORT:def 2
((((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f)) ';' (SubFrom (intloc 1),(intloc 0 ))) ';' (Times (intloc 1),(((((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))))) ';' (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5))))));
coherence
((((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f)) ';' (SubFrom (intloc 1),(intloc 0 ))) ';' (Times (intloc 1),(((((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))))) ';' (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5)))))) is Program of SCM+FSA ;

end;

:: deftheorem defines insert-sort SCMISORT:def 2 :

for f being FinSeq-Location holds insert-sort f = ((((((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ))) ';' ((intloc 1) :=len f)) ';' (SubFrom (intloc 1),(intloc 0 ))) ';' (Times (intloc 1),(((((((((intloc 2) :=len f) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0 ))) ';' ((intloc 6) := f,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := f,(intloc 2)) ';' (SubFrom (intloc 5),(intloc 6))) ';' (if>0 (intloc 5),(Macro (SubFrom (intloc 2),(intloc 2))),((AddTo (intloc 4),(intloc 0 )) ';' (SubFrom (intloc 2),(intloc 0 ))))))) ';' (Times (intloc 4),(((((((intloc 2) := (intloc 3)) ';' (SubFrom (intloc 3),(intloc 0 ))) ';' ((intloc 5) := f,(intloc 2))) ';' ((intloc 6) := f,(intloc 3))) ';' (f,(intloc 2) := (intloc 6))) ';' (f,(intloc 3) := (intloc 5))))));

definition

func Insert-Sort-Algorithm -> Program of SCM+FSA equals :: SCMISORT:def 3
insert-sort (fsloc 0 );
coherence
insert-sort (fsloc 0 ) is Program of SCM+FSA ;

end;

:: deftheorem defines Insert-Sort-Algorithm SCMISORT:def 3 :

Insert-Sort-Algorithm = insert-sort (fsloc 0 );

theorem Th38: :: SCMISORT:38

for f being FinSeq-Location holds UsedIntLoc (insert-sort f) = {(intloc 0 ),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}

proof end;

theorem Th39: :: SCMISORT:39

for f being FinSeq-Location holds UsedInt*Loc (insert-sort f) = {f}

proof end;

theorem Th40: :: SCMISORT:40

for k1, k2, k3, k4 being Instruction of SCM+FSA holds card (((k1 ';' k2) ';' k3) ';' k4) = 8

proof end;

theorem Th41: :: SCMISORT:41

for k1, k2, k3, k4, k5 being Instruction of SCM+FSA holds card ((((k1 ';' k2) ';' k3) ';' k4) ';' k5) = 10

proof end;

theorem Th42: :: SCMISORT:42

for f being FinSeq-Location holds card (insert-sort f) = 82

proof end;

theorem Th43: :: SCMISORT:43

for f being FinSeq-Location
for k being Element of NAT st k < 82 holds
insloc k in dom (insert-sort f)

proof end;

Lm1: for s being State of SCM+FSA st Insert-Sort-Algorithm c= s holds
( s . (insloc 0 ) = (intloc 2) := (intloc 0 ) & s . (insloc 1) = goto (insloc 2) & s . (insloc 2) = (intloc 3) := (intloc 0 ) & s . (insloc 3) = goto (insloc 4) & s . (insloc 4) = (intloc 4) := (intloc 0 ) & s . (insloc 5) = goto (insloc 6) & s . (insloc 6) = (intloc 5) := (intloc 0 ) & s . (insloc 7) = goto (insloc 8) & s . (insloc 8) = (intloc 6) := (intloc 0 ) & s . (insloc 9) = goto (insloc 10) & s . (insloc 10) = (intloc 1) :=len (fsloc 0 ) & s . (insloc 11) = goto (insloc 12) )

proof end;

set f0 = fsloc 0 ;

set b1 = intloc (0 + 1);

set b2 = intloc (1 + 1);

set b3 = intloc (2 + 1);

set b4 = intloc (3 + 1);

set b5 = intloc (4 + 1);

set b6 = intloc (5 + 1);

set i1 = (intloc (1 + 1)) := (intloc (2 + 1));

set i2 = SubFrom (intloc (2 + 1)),(intloc 0 );

set i3 = (intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1));

set i4 = (intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1));

set i5 = (fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1));

set i6 = (fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1));

set body3 = ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1)));

set w2 = (intloc (1 + 1)) := (intloc 0 );

set w3 = (intloc (2 + 1)) := (intloc 0 );

set w4 = (intloc (3 + 1)) := (intloc 0 );

set w5 = (intloc (4 + 1)) := (intloc 0 );

set w6 = (intloc (5 + 1)) := (intloc 0 );

set T3 = Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))));

set m0 = SubFrom (intloc (1 + 1)),(intloc (1 + 1));

set m1 = Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)));

set m2 = AddTo (intloc (3 + 1)),(intloc 0 );

set m3 = SubFrom (intloc (1 + 1)),(intloc 0 );

set IF = if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )));

set n1 = (intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1));

set n2 = SubFrom (intloc (4 + 1)),(intloc (5 + 1));

set body2 = (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))));

set t1 = (intloc (1 + 1)) :=len (fsloc 0 );

set t2 = SubFrom (intloc (1 + 1)),(intloc (0 + 1));

set t3 = (intloc (2 + 1)) := (intloc (1 + 1));

set t4 = AddTo (intloc (2 + 1)),(intloc 0 );

set t5 = (intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1));

set t6 = SubFrom (intloc (3 + 1)),(intloc (3 + 1));

set Wg = while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))));

set t16 = ((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)));

set body1 = ((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1)))));

set WM = (((((intloc 2) := (intloc 0 )) ';' ((intloc 3) := (intloc 0 ))) ';' ((intloc 4) := (intloc 0 ))) ';' ((intloc 5) := (intloc 0 ))) ';' ((intloc 6) := (intloc 0 ));

set j1 = (intloc (0 + 1)) :=len (fsloc 0 );

set j2 = SubFrom (intloc (0 + 1)),(intloc 0 );

Lm2: for s being State of SCM+FSA st Insert-Sort-Algorithm c= s & s starts_at 0 holds
( ( for k being Element of NAT st k > 0 & k < 12 holds
( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) ) & (Computation s,11) . (intloc 1) = len (s . (fsloc 0 )) & (Computation s,11) . (intloc 2) = s . (intloc 0 ) & (Computation s,11) . (intloc 3) = s . (intloc 0 ) & (Computation s,11) . (intloc 4) = s . (intloc 0 ) & (Computation s,11) . (intloc 5) = s . (intloc 0 ) & (Computation s,11) . (intloc 6) = s . (intloc 0 ) )

proof end;

Lm3: for s being State of SCM+FSA holds
( ( s . (intloc (4 + 1)) > 0 implies (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (intloc (1 + 1)) = 0 ) & ( s . (intloc (4 + 1)) <= 0 implies (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 ) )

proof end;

Lm4: for s being State of SCM+FSA holds
( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) < s . (intloc (1 + 1)) or (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),s) . (intloc (1 + 1)) <= 0 )

proof end;

then Lm5: while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))) is good InitHalting Program of SCM+FSA
by Th30;

Lm6: ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))) does_not_destroy intloc (3 + 1)

proof end;

Lm7: ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))) does_not_destroy intloc (0 + 1)

proof end;

Lm8: (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))) does_not_destroy intloc (0 + 1)

proof end;

Lm9: ((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))) does_not_destroy intloc (0 + 1)

proof end;

Lm10: Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1)))) is good InitHalting Program of SCM+FSA

proof end;

Lm11: ((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))) is good InitHalting Program of SCM+FSA

proof end;

Lm12: Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1)))))) is good InitHalting Program of SCM+FSA

proof end;

theorem Th44: :: SCMISORT:44

( insert-sort (fsloc 0 ) is keepInt0_1 & insert-sort (fsloc 0 ) is InitHalting ) by Lm12;

Lm13: for s being State of SCM+FSA holds (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (fsloc 0 ) = s . (fsloc 0 )

proof end;

Lm14: for s being State of SCM+FSA holds
( ( s . (intloc (4 + 1)) > 0 implies (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) & ( s . (intloc (4 + 1)) <= 0 implies (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) )

proof end;

Lm15: for a being read-write Int-Location
for s being State of SCM+FSA st a <> intloc (3 + 1) & a <> intloc (1 + 1) holds
(IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . a = s . a

proof end;

Lm16: for t being State of SCM+FSA st t . (intloc (1 + 1)) >= 1 & t . (intloc (1 + 1)) <= len (t . (fsloc 0 )) holds
( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),t) . (intloc (2 + 1)) = t . (intloc (2 + 1)) & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),t) . (intloc (5 + 1)) = t . (intloc (5 + 1)) & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),t) . (fsloc 0 ) = t . (fsloc 0 ) & ex x1 being Integer st
( x1 = (t . (fsloc 0 )) . (t . (intloc (1 + 1))) & ( x1 - (t . (intloc (5 + 1))) > 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),t) . (intloc (1 + 1)) = 0 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),t) . (intloc (3 + 1)) = t . (intloc (3 + 1)) ) ) & ( x1 - (t . (intloc (5 + 1))) <= 0 implies ( (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),t) . (intloc (1 + 1)) = (t . (intloc (1 + 1))) - 1 & (IExec ((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))),t) . (intloc (3 + 1)) = (t . (intloc (3 + 1))) + 1 ) ) ) )

proof end;

Lm17: for k being Element of NAT
for s being State of SCM+FSA st s . (intloc (1 + 1)) = k & s . (intloc (1 + 1)) <= len (s . (fsloc 0 )) holds
( s . (fsloc 0 ) = (IExec (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))))),s) . (fsloc 0 ) & s . (intloc (5 + 1)) = (IExec (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))))),s) . (intloc (5 + 1)) & s . (intloc (2 + 1)) = (IExec (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))))),s) . (intloc (2 + 1)) & ( k = 0 or ex n being Element of NAT ex x1 being Integer st
( n = ((IExec (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))))),s) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k & ( k - n >= 1 implies ( x1 = (s . (fsloc 0 )) . (k - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Element of NAT st i > k - n & i < k + 1 holds
ex x2 being Integer st
( x2 = (s . (fsloc 0 )) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )

proof end;

Lm18: for s being State of SCM+FSA holds
( (IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1)))),s) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 & (IExec (((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1)))),s) . (fsloc 0 ) = ((s . (fsloc 0 )) +* (abs (s . (intloc (2 + 1)))),((s . (fsloc 0 )) /. (abs ((s . (intloc (2 + 1))) - 1)))) +* (abs ((s . (intloc (2 + 1))) - 1)),((s . (fsloc 0 )) /. (abs (s . (intloc (2 + 1))))) )

proof end;

Lm19: for k being Element of NAT
for s being State of SCM+FSA st s . (intloc (3 + 1)) = k & k < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . (fsloc 0 )) holds
( s . (fsloc 0 ),(IExec (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))),s) . (fsloc 0 ) are_fiberwise_equipotent & (IExec (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))),s) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - k & ((IExec (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))),s) . (fsloc 0 )) . ((s . (intloc (2 + 1))) - k) = (s . (fsloc 0 )) . (s . (intloc (2 + 1))) & ( for i being Element of NAT st (s . (intloc (2 + 1))) - k < i & i <= s . (intloc (2 + 1)) holds
((IExec (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))),s) . (fsloc 0 )) . i = (s . (fsloc 0 )) . (i - 1) ) & ( for i being Element of NAT st s . (intloc (2 + 1)) < i & i <= len (s . (fsloc 0 )) holds
((IExec (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))),s) . (fsloc 0 )) . i = (s . (fsloc 0 )) . i ) & ( for i being Element of NAT st 1 <= i & i < (s . (intloc (2 + 1))) - k holds
((IExec (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))),s) . (fsloc 0 )) . i = (s . (fsloc 0 )) . i ) )

proof end;

Lm20: for s being State of SCM+FSA holds
( (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (1 + 1)) = (len (s . (fsloc 0 ))) - (s . (intloc (0 + 1))) & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (2 + 1)) = ((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1 & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (fsloc 0 ) = s . (fsloc 0 ) & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (3 + 1)) = 0 & (IExec (((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))),s) . (intloc (5 + 1)) = (s . (fsloc 0 )) /. (abs (((len (s . (fsloc 0 ))) - (s . (intloc (0 + 1)))) + 1)) )

proof end;

set T1 = Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))));

Lm21: for s being State of SCM+FSA st s . (intloc (0 + 1)) = (len (s . (fsloc 0 ))) - 1 holds
( s . (fsloc 0 ),(IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))))),s) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))))),s) . (fsloc 0 )) . i & x2 = ((IExec (Times (intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len (fsloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc (0 + 1)))) ';' ((intloc (2 + 1)) := (intloc (1 + 1)))) ';' (AddTo (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' (SubFrom (intloc (3 + 1)),(intloc (3 + 1)))) ';' (while>0 (intloc (1 + 1)),((((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))))))) ';' (Times (intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))))))),s) . (fsloc 0 )) . j holds
x1 >= x2 ) )

proof end;

theorem Th45: :: SCMISORT:45

for s being State of SCM+FSA holds
( s . (fsloc 0 ),(IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . i & x2 = ((IExec (insert-sort (fsloc 0 )),s) . (fsloc 0 )) . j holds
x1 >= x2 ) )

proof end;

theorem Th46: :: SCMISORT:46

for i being Element of NAT
for s being State of SCM+FSA
for w being FinSequence of INT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) c= s holds
IC (Computation s,i) in dom Insert-Sort-Algorithm

proof end;

theorem Th47: :: SCMISORT:47

for s being State of SCM+FSA
for t being FinSequence of INT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> t) c= s holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result s) . (fsloc 0 ) = u )

proof end;

theorem Th48: :: SCMISORT:48

for w being FinSequence of INT holds (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0 ) .--> w) is autonomic

proof end;

theorem :: SCMISORT:49

Initialized Insert-Sort-Algorithm computes Sorting-Function

proof end;