:: SCMISORT semantic presentation

registration
let c1 be good Instruction of SCM+FSA ;
cluster Macro a1 -> good ;
coherence
Macro c1 is good
proof end;
end;

registration
let c1 be read-write Int-Location ;
let c2 be Int-Location ;
cluster AddTo a1,a2 -> good ;
coherence
AddTo c1,c2 is good
proof end;
end;

theorem Th1: :: SCMISORT:1
for b1 being Function
for b2, b3 being set st b2 in dom b1 holds
dom b1 = dom (b1 +* (b2 .--> b3))
proof end;

theorem Th2: :: SCMISORT:2
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA
for b3 being Instruction of SCM+FSA st b2 in dom b1 & ex b4 being Instruction of SCM+FSA st
( b4 = b1 . b2 & UsedIntLoc b4 = UsedIntLoc b3 ) holds
UsedIntLoc b1 = UsedIntLoc (b1 +* (b2 .--> b3))
proof end;

theorem Th3: :: SCMISORT:3
for b1 being Int-Location
for b2 being Macro-Instruction holds (if>0 b1,(b2 ';' (Goto (insloc 0))),SCM+FSA-Stop ) . (insloc ((card b2) + 4)) = goto (insloc ((card b2) + 4))
proof end;

theorem Th4: :: SCMISORT:4
for b1 being programmed FinPartState of SCM+FSA
for b2 being Instruction-Location of SCM+FSA
for b3 being Instruction of SCM+FSA st b2 in dom b1 & ex b4 being Instruction of SCM+FSA st
( b4 = b1 . b2 & UsedInt*Loc b4 = UsedInt*Loc b3 ) holds
UsedInt*Loc b1 = UsedInt*Loc (b1 +* (b2 .--> b3))
proof end;

theorem Th5: :: SCMISORT:5
canceled;

theorem Th6: :: SCMISORT:6
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b1 . (intloc 0) = 1 & IC b1 = insloc 0 holds
b1 +* b2 = b1 +* (Initialized b2)
proof end;

theorem Th7: :: SCMISORT:7
for b1 being Macro-Instruction
for b2, b3 being Int-Location st b1 does_not_destroy b3 holds
while>0 b2,b1 does_not_destroy b3
proof end;

theorem Th8: :: SCMISORT:8
for b1 being Nat holds
( not b1 <= 11 or b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 or b1 = 5 or b1 = 6 or b1 = 7 or b1 = 8 or b1 = 9 or b1 = 10 or b1 = 11 )
proof end;

theorem Th9: :: SCMISORT:9
for b1, b2 being FinSequence of INT
for b3, b4 being Nat st 1 <= b4 & b4 <= len b1 & 1 <= b3 & b3 <= len b1 & b2 = (b1 +* b3,(b1 /. b4)) +* b4,(b1 /. b3) holds
( b1 . b3 = b2 . b4 & b1 . b4 = b2 . b3 & ( for b5 being set st b5 <> b3 & b5 <> b4 & b5 in dom b1 holds
b1 . b5 = b2 . b5 ) & b1,b2 are_fiberwise_equipotent )
proof end;

theorem Th10: :: SCMISORT:10
for b1 being State of SCM+FSA
for b2 being Macro-Instruction st b2 is_halting_on Initialize b1 holds
for b3 being Int-Location holds (IExec b2,b1) . b3 = ((Computation ((Initialize b1) +* (b2 +* (Start-At (insloc 0))))) . (LifeSpan ((Initialize b1) +* (b2 +* (Start-At (insloc 0)))))) . b3
proof end;

theorem Th11: :: SCMISORT:11
for b1, b2 being State of SCM+FSA
for b3 being InitHalting Macro-Instruction st Initialized b3 c= b1 & Initialized b3 c= b2 & b1,b2 equal_outside the Instruction-Locations of SCM+FSA holds
for b4 being Nat holds
( (Computation b1) . b4,(Computation b2) . b4 equal_outside the Instruction-Locations of SCM+FSA & CurInstr ((Computation b1) . b4) = CurInstr ((Computation b2) . b4) )
proof end;

theorem Th12: :: SCMISORT:12
for b1, b2 being State of SCM+FSA
for b3 being InitHalting Macro-Instruction st Initialized b3 c= b1 & Initialized b3 c= b2 & b1,b2 equal_outside the Instruction-Locations of SCM+FSA holds
( LifeSpan b1 = LifeSpan b2 & Result b1, Result b2 equal_outside the Instruction-Locations of SCM+FSA )
proof end;

theorem Th13: :: SCMISORT:13
for b1 being Macro-Instruction
for b2 being FinSeq-Location holds not b2 in dom b1
proof end;

theorem Th14: :: SCMISORT:14
for b1 being Macro-Instruction
for b2 being Int-Location holds not b2 in dom b1
proof end;

theorem Th15: :: SCMISORT:15
for b1 being Nat
for b2 being non empty with_non-empty_elements set
for b3 being non empty non void halting IC-Ins-separated definite AMI-Struct of b2
for b4 being State of b3 st LifeSpan b4 <= b1 & b4 is halting holds
(Computation b4) . b1 = (Computation b4) . (LifeSpan b4)
proof end;

theorem Th16: :: SCMISORT:16
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being read-write Int-Location st b1 . b3 <= 0 holds
( while>0 b3,b2 is_halting_onInit b1 & while>0 b3,b2 is_closed_onInit b1 )
proof end;

theorem Th17: :: SCMISORT:17
for b1 being Int-Location
for b2 being Macro-Instruction
for b3 being State of SCM+FSA
for b4 being Nat st b2 is_closed_onInit b3 & b2 is_halting_onInit b3 & b4 < LifeSpan (b3 +* (Initialized b2)) & IC ((Computation (b3 +* (Initialized (while>0 b1,b2)))) . (1 + b4)) = (IC ((Computation (b3 +* (Initialized b2))) . b4)) + 4 & ((Computation (b3 +* (Initialized (while>0 b1,b2)))) . (1 + b4)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b3 +* (Initialized b2))) . b4) | (Int-Locations \/ FinSeq-Locations ) holds
( IC ((Computation (b3 +* (Initialized (while>0 b1,b2)))) . ((1 + b4) + 1)) = (IC ((Computation (b3 +* (Initialized b2))) . (b4 + 1))) + 4 & ((Computation (b3 +* (Initialized (while>0 b1,b2)))) . ((1 + b4) + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b3 +* (Initialized b2))) . (b4 + 1)) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

theorem Th18: :: SCMISORT:18
for b1 being Int-Location
for b2 being Macro-Instruction
for b3 being State of SCM+FSA st b2 is_closed_onInit b3 & b2 is_halting_onInit b3 & IC ((Computation (b3 +* (Initialized (while>0 b1,b2)))) . (1 + (LifeSpan (b3 +* (Initialized b2))))) = (IC ((Computation (b3 +* (Initialized b2))) . (LifeSpan (b3 +* (Initialized b2))))) + 4 holds
CurInstr ((Computation (b3 +* (Initialized (while>0 b1,b2)))) . (1 + (LifeSpan (b3 +* (Initialized b2))))) = goto (insloc ((card b2) + 4))
proof end;

theorem Th19: :: SCMISORT:19
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being read-write Int-Location st b2 is_closed_onInit b1 & b2 is_halting_onInit b1 & b1 . b3 > 0 holds
( IC ((Computation (b1 +* (Initialized (while>0 b3,b2)))) . ((LifeSpan (b1 +* (Initialized b2))) + 3)) = insloc 0 & ( for b4 being Nat st b4 <= (LifeSpan (b1 +* (Initialized b2))) + 3 holds
IC ((Computation (b1 +* (Initialized (while>0 b3,b2)))) . b4) in dom (while>0 b3,b2) ) )
proof end;

theorem Th20: :: SCMISORT:20
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being read-write Int-Location st b2 is_closed_onInit b1 & b2 is_halting_onInit b1 & b1 . b3 > 0 holds
for b4 being Nat st b4 <= (LifeSpan (b1 +* (Initialized b2))) + 3 holds
IC ((Computation (b1 +* (Initialized (while>0 b3,b2)))) . b4) in dom (while>0 b3,b2)
proof end;

theorem Th21: :: SCMISORT:21
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being read-write Int-Location st b2 is_closed_onInit b1 & b2 is_halting_onInit b1 & b1 . b3 > 0 holds
( IC ((Computation (b1 +* (Initialized (while>0 b3,b2)))) . ((LifeSpan (b1 +* (Initialized b2))) + 3)) = insloc 0 & ((Computation (b1 +* (Initialized (while>0 b3,b2)))) . ((LifeSpan (b1 +* (Initialized b2))) + 3)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b1 +* (Initialized b2))) . (LifeSpan (b1 +* (Initialized b2)))) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

theorem Th22: :: SCMISORT:22
for b1 being State of SCM+FSA
for b2 being InitHalting Macro-Instruction
for b3 being read-write Int-Location st b1 . b3 > 0 holds
ex b4 being State of SCM+FSA ex b5 being Nat st
( b4 = b1 +* (Initialized (while>0 b3,b2)) & b5 = (LifeSpan (b1 +* (Initialized b2))) + 3 & IC ((Computation b4) . b5) = insloc 0 & ( for b6 being Int-Location holds ((Computation b4) . b5) . b6 = (IExec b2,b1) . b6 ) & ( for b6 being FinSeq-Location holds ((Computation b4) . b5) . b6 = (IExec b2,b1) . b6 ) )
proof end;

definition
let c1 be State of SCM+FSA ;
let c2 be Macro-Instruction;
let c3 be read-write Int-Location ;
func StepWhile>0 c3,c1,c2 -> Function of NAT , product the Object-Kind of SCM+FSA means :Def1: :: SCMISORT:def 1
( a4 . 0 = a1 & ( for b1 being Nat holds a4 . (b1 + 1) = (Computation ((a4 . b1) +* (Initialized (while>0 a3,a2)))) . ((LifeSpan ((a4 . b1) +* (Initialized a2))) + 3) ) );
existence
ex b1 being Function of NAT , product the Object-Kind of SCM+FSA st
( b1 . 0 = c1 & ( for b2 being Nat holds b1 . (b2 + 1) = (Computation ((b1 . b2) +* (Initialized (while>0 c3,c2)))) . ((LifeSpan ((b1 . b2) +* (Initialized c2))) + 3) ) )
proof end;
uniqueness
for b1, b2 being Function of NAT , product the Object-Kind of SCM+FSA st b1 . 0 = c1 & ( for b3 being Nat holds b1 . (b3 + 1) = (Computation ((b1 . b3) +* (Initialized (while>0 c3,c2)))) . ((LifeSpan ((b1 . b3) +* (Initialized c2))) + 3) ) & b2 . 0 = c1 & ( for b3 being Nat holds b2 . (b3 + 1) = (Computation ((b2 . b3) +* (Initialized (while>0 c3,c2)))) . ((LifeSpan ((b2 . b3) +* (Initialized c2))) + 3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines StepWhile>0 SCMISORT:def 1 :
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being read-write Int-Location
for b4 being Function of NAT , product the Object-Kind of SCM+FSA holds
( b4 = StepWhile>0 b3,b1,b2 iff ( b4 . 0 = b1 & ( for b5 being Nat holds b4 . (b5 + 1) = (Computation ((b4 . b5) +* (Initialized (while>0 b3,b2)))) . ((LifeSpan ((b4 . b5) +* (Initialized b2))) + 3) ) ) );

theorem Th23: :: SCMISORT:23
canceled;

theorem Th24: :: SCMISORT:24
canceled;

theorem Th25: :: SCMISORT:25
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being read-write Int-Location
for b4 being Nat holds (StepWhile>0 b3,b1,b2) . (b4 + 1) = (StepWhile>0 b3,((StepWhile>0 b3,b1,b2) . b4),b2) . 1
proof end;

theorem Th26: :: SCMISORT:26
for b1 being Macro-Instruction
for b2 being read-write Int-Location
for b3 being State of SCM+FSA holds (StepWhile>0 b2,b3,b1) . (0 + 1) = (Computation (b3 +* (Initialized (while>0 b2,b1)))) . ((LifeSpan (b3 +* (Initialized b1))) + 3)
proof end;

theorem Th27: :: SCMISORT:27
for b1 being Macro-Instruction
for b2 being read-write Int-Location
for b3 being State of SCM+FSA
for b4, b5 being Nat st IC ((StepWhile>0 b2,b3,b1) . b4) = insloc 0 & (StepWhile>0 b2,b3,b1) . b4 = (Computation (b3 +* (Initialized (while>0 b2,b1)))) . b5 & ((StepWhile>0 b2,b3,b1) . b4) . (intloc 0) = 1 holds
( (StepWhile>0 b2,b3,b1) . b4 = ((StepWhile>0 b2,b3,b1) . b4) +* (Initialized (while>0 b2,b1)) & (StepWhile>0 b2,b3,b1) . (b4 + 1) = (Computation (b3 +* (Initialized (while>0 b2,b1)))) . (b5 + ((LifeSpan (((StepWhile>0 b2,b3,b1) . b4) +* (Initialized b1))) + 3)) )
proof end;

theorem Th28: :: SCMISORT:28
for b1 being Macro-Instruction
for b2 being read-write Int-Location
for b3 being State of SCM+FSA st ex b4 being Function of product the Object-Kind of SCM+FSA , NAT st
for b5 being Nat holds
( ( b4 . ((StepWhile>0 b2,b3,b1) . b5) <> 0 implies ( b4 . ((StepWhile>0 b2,b3,b1) . (b5 + 1)) < b4 . ((StepWhile>0 b2,b3,b1) . b5) & b1 is_closed_onInit (StepWhile>0 b2,b3,b1) . b5 & b1 is_halting_onInit (StepWhile>0 b2,b3,b1) . b5 ) ) & ((StepWhile>0 b2,b3,b1) . (b5 + 1)) . (intloc 0) = 1 & ( b4 . ((StepWhile>0 b2,b3,b1) . b5) = 0 implies ((StepWhile>0 b2,b3,b1) . b5) . b2 <= 0 ) & ( ((StepWhile>0 b2,b3,b1) . b5) . b2 <= 0 implies b4 . ((StepWhile>0 b2,b3,b1) . b5) = 0 ) ) holds
( while>0 b2,b1 is_halting_onInit b3 & while>0 b2,b1 is_closed_onInit b3 )
proof end;

theorem Th29: :: SCMISORT:29
for b1 being good InitHalting Macro-Instruction
for b2 being read-write Int-Location st ( for b3 being State of SCM+FSA st b3 . b2 > 0 holds
(IExec b1,b3) . b2 < b3 . b2 ) holds
while>0 b2,b1 is InitHalting
proof end;

theorem Th30: :: SCMISORT:30
for b1 being good InitHalting Macro-Instruction
for b2 being read-write Int-Location st ( for b3 being State of SCM+FSA holds
( (IExec b1,b3) . b2 < b3 . b2 or (IExec b1,b3) . b2 <= 0 ) ) holds
while>0 b2,b1 is InitHalting
proof end;

definition
let c1 be set ;
let c2 be Function of c1, INT ;
let c3 be Element of c1;
redefine func . as c2 . c3 -> Integer;
coherence
c2 . c3 is Integer
proof end;
end;

theorem Th31: :: SCMISORT:31
for b1 being good InitHalting Macro-Instruction
for b2 being read-write Int-Location st ex b3 being Function of product the Object-Kind of SCM+FSA , INT st
for b4, b5 being State of SCM+FSA holds
( ( b3 . b4 > 0 implies b3 . (IExec b1,b4) < b3 . b4 ) & ( b4 | (Int-Locations \/ FinSeq-Locations ) = b5 | (Int-Locations \/ FinSeq-Locations ) implies b3 . b4 = b3 . b5 ) & ( b3 . b4 <= 0 implies b4 . b2 <= 0 ) & ( b4 . b2 <= 0 implies b3 . b4 <= 0 ) ) holds
while>0 b2,b1 is InitHalting
proof end;

theorem Th32: :: SCMISORT:32
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being read-write Int-Location st b1 . b3 <= 0 holds
(IExec (while>0 b3,b2),b1) | (Int-Locations \/ FinSeq-Locations ) = (Initialize b1) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th33: :: SCMISORT:33
for b1 being State of SCM+FSA
for b2 being good InitHalting Macro-Instruction
for b3 being read-write Int-Location st b1 . b3 > 0 & while>0 b3,b2 is InitHalting holds
(IExec (while>0 b3,b2),b1) | (Int-Locations \/ FinSeq-Locations ) = (IExec (while>0 b3,b2),(IExec b2,b1)) | (Int-Locations \/ FinSeq-Locations )
proof end;

theorem Th34: :: SCMISORT:34
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being FinSeq-Location
for b4 being read-write Int-Location st b1 . b4 <= 0 holds
(IExec (while>0 b4,b2),b1) . b3 = b1 . b3
proof end;

theorem Th35: :: SCMISORT:35
for b1 being State of SCM+FSA
for b2 being Macro-Instruction
for b3 being Int-Location
for b4 being read-write Int-Location st b1 . b4 <= 0 holds
(IExec (while>0 b4,b2),b1) . b3 = (Initialize b1) . b3
proof end;

theorem Th36: :: SCMISORT:36
for b1 being State of SCM+FSA
for b2 being good InitHalting Macro-Instruction
for b3 being FinSeq-Location
for b4 being read-write Int-Location st b1 . b4 > 0 & while>0 b4,b2 is InitHalting holds
(IExec (while>0 b4,b2),b1) . b3 = (IExec (while>0 b4,b2),(IExec b2,b1)) . b3
proof end;

theorem Th37: :: SCMISORT:37
for b1 being State of SCM+FSA
for b2 being good InitHalting Macro-Instruction
for b3 being Int-Location
for b4 being read-write Int-Location st b1 . b4 > 0 & while>0 b4,b2 is InitHalting holds
(IExec (while>0 b4,b2),b1) . b3 = (IExec (while>0 b4,b2),(IExec b2,b1)) . b3
proof end;

set c1 = intloc 0;

set c2 = intloc 1;

set c3 = intloc 2;

set c4 = intloc 3;

set c5 = intloc 4;

set c6 = intloc 5;

set c7 = intloc 6;

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

definition
let c9 be FinSeq-Location ;
func insert-sort c1 -> Macro-Instruction 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 a1)) ';' (SubFrom (intloc 1),(intloc 0))) ';' (Times (intloc 1),(((((((((intloc 2) :=len a1) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0))) ';' ((intloc 6) := a1,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := a1,(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) := a1,(intloc 2))) ';' ((intloc 6) := a1,(intloc 3))) ';' (a1,(intloc 2) := (intloc 6))) ';' (a1,(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 c9)) ';' (SubFrom (intloc 1),(intloc 0))) ';' (Times (intloc 1),(((((((((intloc 2) :=len c9) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0))) ';' ((intloc 6) := c9,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := c9,(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) := c9,(intloc 2))) ';' ((intloc 6) := c9,(intloc 3))) ';' (c9,(intloc 2) := (intloc 6))) ';' (c9,(intloc 3) := (intloc 5)))))) is Macro-Instruction ;
end;

:: deftheorem Def2 defines insert-sort SCMISORT:def 2 :
for b1 being FinSeq-Location holds insert-sort b1 = ((((((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0))) ';' ((intloc 1) :=len b1)) ';' (SubFrom (intloc 1),(intloc 0))) ';' (Times (intloc 1),(((((((((intloc 2) :=len b1) ';' (SubFrom (intloc 2),(intloc 1))) ';' ((intloc 3) := (intloc 2))) ';' (AddTo (intloc 3),(intloc 0))) ';' ((intloc 6) := b1,(intloc 3))) ';' (SubFrom (intloc 4),(intloc 4))) ';' (while>0 (intloc 2),((((intloc 5) := b1,(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) := b1,(intloc 2))) ';' ((intloc 6) := b1,(intloc 3))) ';' (b1,(intloc 2) := (intloc 6))) ';' (b1,(intloc 3) := (intloc 5))))));

definition
func Insert-Sort-Algorithm -> Macro-Instruction equals :: SCMISORT:def 3
 insert-sort (fsloc 0);
coherence
insert-sort (fsloc 0) is Macro-Instruction ;
end;

:: deftheorem Def3 defines Insert-Sort-Algorithm SCMISORT:def 3 :
Insert-Sort-Algorithm = insert-sort (fsloc 0);

theorem Th38: :: SCMISORT:38
for b1 being FinSeq-Location holds UsedIntLoc (insert-sort b1) = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}
proof end;

theorem Th39: :: SCMISORT:39
for b1 being FinSeq-Location holds UsedInt*Loc (insert-sort b1) = {b1}
proof end;

theorem Th40: :: SCMISORT:40
for b1, b2, b3, b4 being Instruction of SCM+FSA holds card (((b1 ';' b2) ';' b3) ';' b4) = 8
proof end;

theorem Th41: :: SCMISORT:41
for b1, b2, b3, b4, b5 being Instruction of SCM+FSA holds card ((((b1 ';' b2) ';' b3) ';' b4) ';' b5) = 10
proof end;

theorem Th42: :: SCMISORT:42
for b1 being FinSeq-Location holds card (insert-sort b1) = 82
proof end;

theorem Th43: :: SCMISORT:43
for b1 being FinSeq-Location
for b2 being Nat st b2 < 82 holds
insloc b2 in dom (insert-sort b1)
proof end;

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

set c9 = fsloc 0;

set c10 = intloc (0 + 1);

set c11 = intloc (1 + 1);

set c12 = intloc (2 + 1);

set c13 = intloc (3 + 1);

set c14 = intloc (4 + 1);

set c15 = intloc (5 + 1);

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

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

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

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

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

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

set c22 = ((((((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 c23 = (intloc (1 + 1)) := (intloc 0);

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

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

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

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

set c28 = 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 c29 = SubFrom (intloc (1 + 1)),(intloc (1 + 1));

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

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

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

set c33 = 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 c34 = (intloc (4 + 1)) := (fsloc 0),(intloc (1 + 1));

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

set c36 = (((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 c37 = (intloc (1 + 1)) :=len (fsloc 0);

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

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

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

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

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

set c43 = 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 c44 = ((((((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 c45 = ((((((((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 c46 = (((((intloc 2) := (intloc 0)) ';' ((intloc 3) := (intloc 0))) ';' ((intloc 4) := (intloc 0))) ';' ((intloc 5) := (intloc 0))) ';' ((intloc 6) := (intloc 0));

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

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

Lemma33: for b1 being State of SCM+FSA st Insert-Sort-Algorithm c= b1 & b1 starts_at insloc 0 holds
( ( for b2 being Nat st b2 > 0 & b2 < 12 holds
( ((Computation b1) . b2) . (IC SCM+FSA ) = insloc b2 & ((Computation b1) . b2) . (intloc 0) = b1 . (intloc 0) & ((Computation b1) . b2) . (fsloc 0) = b1 . (fsloc 0) ) ) & ((Computation b1) . 11) . (intloc 1) = len (b1 . (fsloc 0)) & ((Computation b1) . 11) . (intloc 2) = b1 . (intloc 0) & ((Computation b1) . 11) . (intloc 3) = b1 . (intloc 0) & ((Computation b1) . 11) . (intloc 4) = b1 . (intloc 0) & ((Computation b1) . 11) . (intloc 5) = b1 . (intloc 0) & ((Computation b1) . 11) . (intloc 6) = b1 . (intloc 0) )
proof end;

Lemma34: for b1 being State of SCM+FSA holds
( ( b1 . (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)))),b1) . (intloc (1 + 1)) = 0 ) & ( b1 . (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)))),b1) . (intloc (1 + 1)) = (b1 . (intloc (1 + 1))) - 1 ) )
proof end;

Lemma35: for b1 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))))),b1) . (intloc (1 + 1)) < b1 . (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))))),b1) . (intloc (1 + 1)) <= 0 )
proof end;

then Lemma36: 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 Macro-Instruction
by Th30;

Lemma37: ((((((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;

Lemma38: ((((((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;

Lemma39: (((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;

Lemma40: ((((((((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;

Lemma41: 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 Macro-Instruction
proof end;

Lemma42: ((((((((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 Macro-Instruction
proof end;

Lemma43: 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 Macro-Instruction
proof end;

theorem Th44: :: SCMISORT:44
( insert-sort (fsloc 0) is keepInt0_1 & insert-sort (fsloc 0) is InitHalting )
proof end;

Lemma45: for b1 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)))),b1) . (fsloc 0) = b1 . (fsloc 0)
proof end;

Lemma46: for b1 being State of SCM+FSA holds
( ( b1 . (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)))),b1) . (intloc (3 + 1)) = b1 . (intloc (3 + 1)) ) & ( b1 . (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)))),b1) . (intloc (3 + 1)) = (b1 . (intloc (3 + 1))) + 1 ) )
proof end;

Lemma47: for b1 being read-write Int-Location
for b2 being State of SCM+FSA st b1 <> intloc (3 + 1) & b1 <> 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)))),b2) . b1 = b2 . b1
proof end;

Lemma48: for b1 being State of SCM+FSA st b1 . (intloc (1 + 1)) >= 1 & b1 . (intloc (1 + 1)) <= len (b1 . (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))))),b1) . (intloc (2 + 1)) = b1 . (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))))),b1) . (intloc (5 + 1)) = b1 . (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))))),b1) . (fsloc 0) = b1 . (fsloc 0) & ex b2 being Integer st
( b2 = (b1 . (fsloc 0)) . (b1 . (intloc (1 + 1))) & ( b2 - (b1 . (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))))),b1) . (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))))),b1) . (intloc (3 + 1)) = b1 . (intloc (3 + 1)) ) ) & ( b2 - (b1 . (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))))),b1) . (intloc (1 + 1)) = (b1 . (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))))),b1) . (intloc (3 + 1)) = (b1 . (intloc (3 + 1))) + 1 ) ) ) )
proof end;

Lemma49: for b1 being Nat
for b2 being State of SCM+FSA st b2 . (intloc (1 + 1)) = b1 & b2 . (intloc (1 + 1)) <= len (b2 . (fsloc 0)) holds
( b2 . (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)))))),b2) . (fsloc 0) & b2 . (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)))))),b2) . (intloc (5 + 1)) & b2 . (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)))))),b2) . (intloc (2 + 1)) & ( b1 = 0 or ex b3 being Natex b4 being Integer st
( b3 = ((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)))))),b2) . (intloc (3 + 1))) - (b2 . (intloc (3 + 1))) & b3 <= b1 & ( b1 - b3 >= 1 implies ( b4 = (b2 . (fsloc 0)) . (b1 - b3) & b4 >= b2 . (intloc (5 + 1)) ) ) & ( for b5 being Nat st b5 > b1 - b3 & b5 < b1 + 1 holds
ex b6 being Integer st
( b6 = (b2 . (fsloc 0)) . b5 & b6 <= b2 . (intloc (5 + 1)) ) ) ) ) )
proof end;

Lemma50: for b1 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)))),b1) . (intloc (2 + 1)) = (b1 . (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)))),b1) . (fsloc 0) = ((b1 . (fsloc 0)) +* (abs (b1 . (intloc (2 + 1)))),((b1 . (fsloc 0)) /. (abs ((b1 . (intloc (2 + 1))) - 1)))) +* (abs ((b1 . (intloc (2 + 1))) - 1)),((b1 . (fsloc 0)) /. (abs (b1 . (intloc (2 + 1))))) )
proof end;

Lemma51: for b1 being Nat
for b2 being State of SCM+FSA st b2 . (intloc (3 + 1)) = b1 & b1 < b2 . (intloc (2 + 1)) & b2 . (intloc (2 + 1)) <= len (b2 . (fsloc 0)) holds
( b2 . (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))))),b2) . (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))))),b2) . (intloc (2 + 1)) = (b2 . (intloc (2 + 1))) - b1 & ((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))))),b2) . (fsloc 0)) . ((b2 . (intloc (2 + 1))) - b1) = (b2 . (fsloc 0)) . (b2 . (intloc (2 + 1))) & ( for b3 being Nat st (b2 . (intloc (2 + 1))) - b1 < b3 & b3 <= b2 . (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))))),b2) . (fsloc 0)) . b3 = (b2 . (fsloc 0)) . (b3 - 1) ) & ( for b3 being Nat st b2 . (intloc (2 + 1)) < b3 & b3 <= len (b2 . (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))))),b2) . (fsloc 0)) . b3 = (b2 . (fsloc 0)) . b3 ) & ( for b3 being Nat st 1 <= b3 & b3 < (b2 . (intloc (2 + 1))) - b1 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))))),b2) . (fsloc 0)) . b3 = (b2 . (fsloc 0)) . b3 ) )
proof end;

Lemma52: for b1 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)))),b1) . (intloc (1 + 1)) = (len (b1 . (fsloc 0))) - (b1 . (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)))),b1) . (intloc (2 + 1)) = ((len (b1 . (fsloc 0))) - (b1 . (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)))),b1) . (fsloc 0) = b1 . (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)))),b1) . (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)))),b1) . (intloc (5 + 1)) = (b1 . (fsloc 0)) /. (abs (((len (b1 . (fsloc 0))) - (b1 . (intloc (0 + 1)))) + 1)) )
proof end;

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

Lemma53: for b1 being State of SCM+FSA st b1 . (intloc (0 + 1)) = (len (b1 . (fsloc 0))) - 1 holds
( b1 . (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))))))),b1) . (fsloc 0) are_fiberwise_equipotent & ( for b2, b3 being Nat st b2 >= 1 & b3 <= len (b1 . (fsloc 0)) & b2 < b3 holds
for b4, b5 being Integer st b4 = ((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))))))),b1) . (fsloc 0)) . b2 & b5 = ((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))))))),b1) . (fsloc 0)) . b3 holds
b4 >= b5 ) )
proof end;

theorem Th45: :: SCMISORT:45
for b1 being State of SCM+FSA holds
( b1 . (fsloc 0),(IExec (insert-sort (fsloc 0)),b1) . (fsloc 0) are_fiberwise_equipotent & ( for b2, b3 being Nat st b2 >= 1 & b3 <= len (b1 . (fsloc 0)) & b2 < b3 holds
for b4, b5 being Integer st b4 = ((IExec (insert-sort (fsloc 0)),b1) . (fsloc 0)) . b2 & b5 = ((IExec (insert-sort (fsloc 0)),b1) . (fsloc 0)) . b3 holds
b4 >= b5 ) )
proof end;

theorem Th46: :: SCMISORT:46
for b1 being Nat
for b2 being State of SCM+FSA
for b3 being FinSequence of INT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0) .--> b3) c= b2 holds
IC ((Computation b2) . b1) in dom Insert-Sort-Algorithm
proof end;

theorem Th47: :: SCMISORT:47
for b1 being State of SCM+FSA
for b2 being FinSequence of INT st (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0) .--> b2) c= b1 holds
ex b3 being FinSequence of REAL st
( b2,b3 are_fiberwise_equipotent & b3 is non-increasing & b3 is FinSequence of INT & (Result b1) . (fsloc 0) = b3 )
proof end;

theorem Th48: :: SCMISORT:48
for b1 being FinSequence of INT holds (Initialized Insert-Sort-Algorithm ) +* ((fsloc 0) .--> b1) is autonomic
proof end;

theorem Th49: :: SCMISORT:49
Initialized Insert-Sort-Algorithm computes Sorting-Function
proof end;