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

theorem :: SCMISORT:1
canceled;

::$CT theorem Th1: :: SCMISORT:2 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA st I is_halting_on Initialized s,P holds for a being Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),(),(LifeSpan ((P +* I),())))) . a proof end; theorem :: SCMISORT:3 canceled; theorem :: SCMISORT:4 canceled; theorem :: SCMISORT:5 canceled; ::$CT 3
theorem :: SCMISORT:6
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA
for k being Nat st I is_halting_onInit s,P & k < LifeSpan ((P +* I),()) & IC (Comput ((P +* (while>0 (a,I))),(),(1 + k))) = (IC (Comput ((P +* I),(),k))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(),(1 + k))) = DataPart (Comput ((P +* I),(),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(),((1 + k) + 1))) = (IC (Comput ((P +* I),(),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(),((1 + k) + 1))) = DataPart (Comput ((P +* I),(),(k + 1))) )
proof end;

theorem :: SCMISORT:7
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA st I is_halting_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))))) = (IC (Comput ((P +* I),(),(LifeSpan ((P +* I),()))))) + 3 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0
proof end;

theorem Th4: :: SCMISORT:8
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) ) )
proof end;

theorem :: SCMISORT:9
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds
for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I))
proof end;

theorem :: SCMISORT:10
canceled;

::$CT theorem :: SCMISORT:11 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitHalting really-closed MacroInstruction 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 Nat st ( s2 = Initialized s & k = (LifeSpan ((P +* I),())) + 2 & IC (Comput ((P +* (while>0 (a,I))),s2,k)) = 0 & ( for b being Int-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),s2,k)) . f = (IExec (I,P,s)) . f ) ) proof end; definition let s be State of SCM+FSA; let I be MacroInstruction of SCM+FSA ; let a be read-write Int-Location; let P be Instruction-Sequence of SCM+FSA; deffunc H1( Nat, Element of product ) -> set = Comput ((P +* (while>0 (a,I))),(),((LifeSpan (((P +* (while>0 (a,I))) +* I),())) + 2)); deffunc H2( Nat, Element of product ) -> Element of product = down H1($1,$2); func StepWhile>0 (a,P,s,I) -> sequence of means :Def1: :: SCMISORT:def 1 ( it . 0 = s & ( for i being Nat holds it . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (it . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (it . i)))) + 2)) ) ); existence ex b1 being sequence of st ( b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (b1 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (b1 . i)))) + 2)) ) ) proof end; uniqueness for b1, b2 being sequence of st b1 . 0 = s & ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (b1 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (b1 . i)))) + 2)) ) & b2 . 0 = s & ( for i being Nat holds b2 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (b2 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (b2 . i)))) + 2)) ) holds b1 = b2 proof end; end; :: deftheorem Def1 defines StepWhile>0 SCMISORT:def 1 : for s being State of SCM+FSA for I being MacroInstruction of SCM+FSA for a being read-write Int-Location for P being Instruction-Sequence of SCM+FSA for b5 being sequence of holds ( b5 = StepWhile>0 (a,P,s,I) iff ( b5 . 0 = s & ( for i being Nat holds b5 . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialized (b5 . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized (b5 . i)))) + 2)) ) ) ); theorem :: SCMISORT:12 for s being State of SCM+FSA for I being MacroInstruction of SCM+FSA for a being read-write Int-Location for k being Nat for P being Instruction-Sequence of SCM+FSA holds (StepWhile>0 (a,P,s,I)) . (k + 1) = (StepWhile>0 (a,P,((StepWhile>0 (a,P,s,I)) . k),I)) . 1 proof end; theorem Th8: :: SCMISORT:13 for P being Instruction-Sequence of SCM+FSA for I being MacroInstruction of SCM+FSA for a being read-write Int-Location for s being State of SCM+FSA holds (StepWhile>0 (a,P,s,I)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(),((LifeSpan (((P +* (while>0 (a,I))) +* I),())) + 2)) proof end; theorem Th9: :: SCMISORT:14 for P being Instruction-Sequence of SCM+FSA for I being MacroInstruction of SCM+FSA for a being read-write Int-Location for s being State of SCM+FSA for k, n being Nat st IC ((StepWhile>0 (a,P,s,I)) . k) = 0 & (StepWhile>0 (a,P,s,I)) . k = Comput ((P +* (while>0 (a,I))),(),n) & ((StepWhile>0 (a,P,s,I)) . k) . () = 1 holds ( (StepWhile>0 (a,P,s,I)) . k = Initialized ((StepWhile>0 (a,P,s,I)) . k) & (StepWhile>0 (a,P,s,I)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(),(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . k)))) + 2))) ) proof end; theorem :: SCMISORT:15 for P being Instruction-Sequence of SCM+FSA for I being really-closed MacroInstruction of SCM+FSA for a being read-write Int-Location for s being State of SCM+FSA st ex f being Function of ,NAT st for k being Nat holds ( ( f . ((StepWhile>0 (a,P,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,P,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,P,s,I)) . k) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) ) ) & ((StepWhile>0 (a,P,s,I)) . (k + 1)) . () = 1 & ( f . ((StepWhile>0 (a,P,s,I)) . k) = 0 implies ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,P,s,I)) . k) = 0 ) ) holds while>0 (a,I) is_halting_onInit s,P proof end; theorem :: SCMISORT:16 canceled; ::$CT
theorem Th11: :: SCMISORT:17
for I being InitHalting good really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st ( for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( (IExec (I,P,s)) . a < s . a or (IExec (I,P,s)) . a <= 0 ) ) holds
while>0 (a,I) is InitHalting
proof end;

theorem :: SCMISORT:18
for I being InitHalting good really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st ex f being Function of ,INT st
for s, t being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . s > 0 implies f . (IExec (I,P,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 Th13: :: SCMISORT:19
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart ()
proof end;

theorem :: SCMISORT:20
canceled;

::\$CT
theorem Th14: :: SCMISORT:21
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being MacroInstruction 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)),P,s)) . f = s . f
proof end;

theorem Th15: :: SCMISORT:22
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being MacroInstruction 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)),P,s)) . b = () . b
proof end;

theorem Th16: :: SCMISORT:23
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being InitHalting good really-closed MacroInstruction 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)),P,s)) . f = (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) . f
proof end;

theorem Th17: :: SCMISORT:24
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being InitHalting good really-closed MacroInstruction 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)),P,s)) . b = (IExec ((while>0 (a,I)),P,(IExec (I,P,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 = ((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ());

definition
let f be FinSeq-Location ;
func insert-sort f -> Program of SCM+FSA equals :: SCMISORT:def 2
(((((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() :=len f)) ";" (SubFrom ((),()))) ";" (Times ((),((((((((() :=len f) ";" (SubFrom ((),()))) ";" (() := ())) ";" (AddTo ((),()))) ";" (() := (f,()))) ";" (SubFrom ((),()))) ";" (while>0 ((),(((() := (f,())) ";" (SubFrom ((),()))) ";" (if>0 ((),(Macro (SubFrom ((),()))),((AddTo ((),())) ";" (SubFrom ((),()))))))))) ";" (Times ((),((((((() := ()) ";" (SubFrom ((),()))) ";" (() := (f,()))) ";" (() := (f,()))) ";" ((f,()) := ())) ";" ((f,()) := ())))))));
coherence
(((((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() :=len f)) ";" (SubFrom ((),()))) ";" (Times ((),((((((((() :=len f) ";" (SubFrom ((),()))) ";" (() := ())) ";" (AddTo ((),()))) ";" (() := (f,()))) ";" (SubFrom ((),()))) ";" (while>0 ((),(((() := (f,())) ";" (SubFrom ((),()))) ";" (if>0 ((),(Macro (SubFrom ((),()))),((AddTo ((),())) ";" (SubFrom ((),()))))))))) ";" (Times ((),((((((() := ()) ";" (SubFrom ((),()))) ";" (() := (f,()))) ";" (() := (f,()))) ";" ((f,()) := ())) ";" ((f,()) := ()))))))) is Program of SCM+FSA
;
end;

:: deftheorem defines insert-sort SCMISORT:def 2 :
for f being FinSeq-Location holds insert-sort f = (((((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() :=len f)) ";" (SubFrom ((),()))) ";" (Times ((),((((((((() :=len f) ";" (SubFrom ((),()))) ";" (() := ())) ";" (AddTo ((),()))) ";" (() := (f,()))) ";" (SubFrom ((),()))) ";" (while>0 ((),(((() := (f,())) ";" (SubFrom ((),()))) ";" (if>0 ((),(Macro (SubFrom ((),()))),((AddTo ((),())) ";" (SubFrom ((),()))))))))) ";" (Times ((),((((((() := ()) ";" (SubFrom ((),()))) ";" (() := (f,()))) ";" (() := (f,()))) ";" ((f,()) := ())) ";" ((f,()) := ())))))));

definition
coherence ;
end;

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

theorem Th18: :: SCMISORT:25
for f being FinSeq-Location holds UsedILoc () = {(),(),(),(),(),(),()}
proof end;

theorem Th19: :: SCMISORT:26
for f being FinSeq-Location holds UsedI*Loc () = {f}
proof end;

theorem Th20: :: SCMISORT:27
for k1, k2, k3, k4 being Instruction of SCM+FSA holds card (((k1 ";" k2) ";" k3) ";" k4) = 8
proof end;

theorem Th21: :: SCMISORT:28
for k1, k2, k3, k4, k5 being Instruction of SCM+FSA holds card ((((k1 ";" k2) ";" k3) ";" k4) ";" k5) = 10
proof end;

theorem Th22: :: SCMISORT:29
for f being FinSeq-Location holds card () = 71
proof end;

theorem Th23: :: SCMISORT:30
for f being FinSeq-Location
for k being Nat st k < 71 holds
k in dom ()
proof end;

Lm1: for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
( P . 0 = () := () & P . 1 = goto 2 & P . 2 = () := () & P . 3 = goto 4 & P . 4 = () := () & P . 5 = goto 6 & P . 6 = () := () & P . 7 = goto 8 & P . 8 = () := () & P . 9 = goto 10 & P . 10 = () :=len () & P . 11 = goto 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)),());

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

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

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

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

set body3 = ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)));

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

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

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

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

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

set T3 = Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(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)),());

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

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

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

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

set body2 = (((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))));

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

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

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

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

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

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

set Wg = while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))));

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

set body1 = ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))));

set WM = ((((() := ()) ";" (() := ())) ";" (() := ())) ";" (() := ())) ";" (() := ());

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

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

Lm2: for s being 0 -started State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
( ( for k being Nat st k > 0 & k < 12 holds
( (Comput (P,s,k)) . () = k & (Comput (P,s,k)) . () = s . () & (Comput (P,s,k)) . () = s . () ) ) & (Comput (P,s,11)) . () = len (s . ()) & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () & (Comput (P,s,11)) . () = s . () )

proof end;

Lm3: for P being Instruction-Sequence of SCM+FSA
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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))),P,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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))),P,s)) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 ) )

proof end;

Lm4: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (1 + 1)) < s . (intloc (1 + 1)) or (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),P,s)) . (intloc (1 + 1)) <= 0 )

proof end;

then Lm5: while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))) is InitHalting good Program of SCM+FSA
by Th11;

Lm6: not ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))) destroys intloc (3 + 1)
proof end;

Lm7: not ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))) destroys intloc (0 + 1)
proof end;

Lm8: not (((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))) destroys intloc (0 + 1)
proof end;

Lm9: not ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))) destroys intloc (0 + 1)
proof end;

Lm10: ( Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) is good & Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))) is InitHalting )
proof end;

Lm11: ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))) is InitHalting good Program of SCM+FSA
proof end;

Lm12: ( Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))))) is good & Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))))) is InitHalting )
proof end;

theorem :: SCMISORT:31
( insert-sort () is keepInt0_1 & insert-sort () is InitHalting ) by Lm12;

Lm13: for P being Instruction-Sequence of SCM+FSA
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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))),P,s)) . () = s . ()

proof end;

Lm14: for P being Instruction-Sequence of SCM+FSA
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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))),P,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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) )

proof end;

Lm15: for P being Instruction-Sequence of SCM+FSA
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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))),P,s)) . a = s . a

proof end;

Lm16: for t being State of SCM+FSA
for Q being Instruction-Sequence of SCM+FSA st t . (intloc (1 + 1)) >= 1 & t . (intloc (1 + 1)) <= len (t . ()) holds
( (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),Q,t)) . (intloc (2 + 1)) = t . (intloc (2 + 1)) & (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),Q,t)) . (intloc (5 + 1)) = t . (intloc (5 + 1)) & (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),Q,t)) . () = t . () & ex x1 being Integer st
( x1 = (t . ()) . (t . (intloc (1 + 1))) & ( x1 - (t . (intloc (5 + 1))) > 0 implies ( (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),Q,t)) . (intloc (1 + 1)) = 0 & (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),Q,t)) . (intloc (3 + 1)) = t . (intloc (3 + 1)) ) ) & ( x1 - (t . (intloc (5 + 1))) <= 0 implies ( (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),Q,t)) . (intloc (1 + 1)) = (t . (intloc (1 + 1))) - 1 & (IExec (((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))),Q,t)) . (intloc (3 + 1)) = (t . (intloc (3 + 1))) + 1 ) ) ) )

proof end;

Lm17: for P being Instruction-Sequence of SCM+FSA
for k being Nat
for s being State of SCM+FSA st s . (intloc (1 + 1)) = k & s . (intloc (1 + 1)) <= len (s . ()) holds
( s . () = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . () & s . (intloc (2 + 1)) = (IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (2 + 1)) & ( k = 0 or ex n being Nat ex x1 being Integer st
( n = ((IExec ((while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))),P,s)) . (intloc (3 + 1))) - (s . (intloc (3 + 1))) & n <= k & ( k - n >= 1 implies ( x1 = (s . ()) . (k - n) & x1 >= s . (intloc (5 + 1)) ) ) & ( for i being Nat st i > k - n & i < k + 1 holds
ex x2 being Integer st
( x2 = (s . ()) . i & x2 <= s . (intloc (5 + 1)) ) ) ) ) )

proof end;

Lm18: for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds
( (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . (intloc (2 + 1)) = (s . (intloc (2 + 1))) - 1 & (IExec ((((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))),P,s)) . () = ((s . ()) +* (|.(s . (intloc (2 + 1))).|,((s . ()) /. |.((s . (intloc (2 + 1))) - 1).|))) +* (|.((s . (intloc (2 + 1))) - 1).|,((s . ()) /. |.(s . (intloc (2 + 1))).|)) )

proof end;

Lm19: for k being Nat
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st s . (intloc (3 + 1)) = k & k < s . (intloc (2 + 1)) & s . (intloc (2 + 1)) <= len (s . ()) holds
( s . (),(IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . () are_fiberwise_equipotent & (IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,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 (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . ()) . ((s . (intloc (2 + 1))) - k) = (s . ()) . (s . (intloc (2 + 1))) & ( for i being 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 (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . ()) . i = (s . ()) . (i - 1) ) & ( for i being Nat st s . (intloc (2 + 1)) < i & i <= len (s . ()) holds
((IExec ((Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . ()) . i = (s . ()) . i ) & ( for i being 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 (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1)))))),P,s)) . ()) . i = (s . ()) . i ) )

proof end;

Lm20: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (1 + 1)) = (len (s . ())) - (s . (intloc (0 + 1))) & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (2 + 1)) = ((len (s . ())) - (s . (intloc (0 + 1)))) + 1 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . () = s . () & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (3 + 1)) = 0 & (IExec ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))),P,s)) . (intloc (5 + 1)) = (s . ()) /. |.(((len (s . ())) - (s . (intloc (0 + 1)))) + 1).| )

proof end;

set T1 = Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))))));

Lm21: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st s . (intloc (0 + 1)) = (len (s . ())) - 1 holds
( s . (),(IExec ((Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))))))),P,s)) . () are_fiberwise_equipotent & ( for i, j being Nat st i >= 1 & j <= len (s . ()) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))))))),P,s)) . ()) . i & x2 = ((IExec ((Times ((intloc (0 + 1)),(((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(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)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))))))))),P,s)) . ()) . j holds
x1 >= x2 ) )

proof end;

theorem Th25: :: SCMISORT:32
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA holds
( s . (),(IExec ((),P,s)) . () are_fiberwise_equipotent & ( for i, j being Nat st i >= 1 & j <= len (s . ()) & i < j holds
for x1, x2 being Integer st x1 = ((IExec ((),P,s)) . ()) . i & x2 = ((IExec ((),P,s)) . ()) . j holds
x1 >= x2 ) )
proof end;

theorem Th26: :: SCMISORT:33
for i being Nat
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds
for w being FinSequence of INT st Initialized (() .--> w) c= s holds
IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm
proof end;

theorem Th27: :: SCMISORT:34
for s being State of SCM+FSA
for t being FinSequence of INT
for P being Instruction-Sequence of SCM+FSA st (Initialize (() .--> 1)) +* (() .--> t) c= s & Insert-Sort-Algorithm c= P holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (P,s)) . () = u )
proof end;

theorem Th28: :: SCMISORT:35
for w being FinSequence of INT holds Initialized (() .--> w) is Insert-Sort-Algorithm -autonomic
proof end;

registration
coherence ;
end;

theorem :: SCMISORT:36
proof end;