:: Insert Sort on SCM+FSA :: by JingChao Chen :: :: Received March 13, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users begin theorem :: SCMISORT:1 for p being preProgram of SCM+FSA for l being Element of NAT 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)) proofend; theorem :: SCMISORT:2 for a being Int-Location for I being Program of SCM+FSA holds (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = goto ((card I) + 4) proofend; theorem :: SCMISORT:3 for p being preProgram of SCM+FSA for l being Element of NAT 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)) proofend; theorem Th4: :: SCMISORT:4 for I being Program of SCM+FSA for a, b being Int-Location st not I destroys b holds not while>0 (a,I) destroys b proofend; theorem Th5: :: SCMISORT:5 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),(Initialize (Initialized s)),(LifeSpan ((P +* I),(Initialize (Initialized s)))))) . a proofend; theorem Th6: :: SCMISORT:6 for P1, P2 being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds for k being Element of NAT holds ( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) proofend; theorem Th7: :: SCMISORT:7 for P1, P2 being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds ( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) ) proofend; begin theorem Th8: :: SCMISORT:8 for P being Instruction-Sequence of SCM+FSA 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,P & while>0 (a,I) is_closed_onInit s,P ) proofend; theorem :: SCMISORT:9 for P being Instruction-Sequence of SCM+FSA 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,P & I is_halting_onInit s,P & k < LifeSpan ((P +* I),(Initialized s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = (IC (Comput ((P +* I),(Initialized s),k))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + k))) = DataPart (Comput ((P +* I),(Initialized s),k)) holds ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialized s),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialized s),(k + 1))) ) proofend; theorem :: SCMISORT:10 for P being Instruction-Sequence of SCM+FSA 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,P & I is_halting_onInit s,P & IC (Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s)))))) = (IC (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))) + 4 holds CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),(1 + (LifeSpan ((P +* I),(Initialized s))))))) = goto ((card I) + 4) proofend; theorem Th11: :: SCMISORT:11 for P being Instruction-Sequence of SCM+FSA 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,P & I is_halting_onInit s,P & s . a > 0 holds ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialized s))) + 3 holds IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) in dom (while>0 (a,I)) ) ) proofend; theorem :: SCMISORT:12 for P being Instruction-Sequence of SCM+FSA 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,P & I is_halting_onInit s,P & s . a > 0 holds for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialized s))) + 3 holds IC (Comput ((P +* (while>0 (a,I))),(Initialized s),k)) in dom (while>0 (a,I)) proofend; theorem Th13: :: SCMISORT:13 for P being Instruction-Sequence of SCM+FSA 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,P & I is_halting_onInit s,P & s . a > 0 holds ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 3))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) ) proofend; theorem :: SCMISORT:14 for P being Instruction-Sequence of SCM+FSA 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 = Initialized s & k = (LifeSpan ((P +* I),(Initialized s))) + 3 & 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 ) ) proofend; definition let s be State of SCM+FSA; let I be Program of SCM+FSA; let a be read-write Int-Location; let P be Instruction-Sequence of SCM+FSA; deffunc H1( Nat, Element of product (the_Values_of SCM+FSA)) -> set = Comput ((P +* (while>0 (a,I))),(Initialized $2),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized $2))) + 3)); deffunc H2( Nat, Element of product (the_Values_of SCM+FSA)) -> Element of product (the_Values_of SCM+FSA) = down H1($1,$2); func StepWhile>0 (a,P,s,I) -> Function of NAT,(product (the_Values_of SCM+FSA)) 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)))) + 3)) ) ); existence ex b1 being Function of NAT,(product (the_Values_of SCM+FSA)) 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)))) + 3)) ) ) proofend; uniqueness for b1, b2 being Function of NAT,(product (the_Values_of SCM+FSA)) 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)))) + 3)) ) & 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)))) + 3)) ) holds b1 = b2 proofend; 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 P being Instruction-Sequence of SCM+FSA for b5 being Function of NAT,(product (the_Values_of SCM+FSA)) 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)))) + 3)) ) ) ); theorem :: SCMISORT:15 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 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 proofend; theorem Th16: :: SCMISORT:16 for P being Instruction-Sequence of SCM+FSA 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,P,s,I)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized s))) + 3)) proofend; theorem Th17: :: SCMISORT:17 for P being Instruction-Sequence of SCM+FSA 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,P,s,I)) . k) = 0 & (StepWhile>0 (a,P,s,I)) . k = Comput ((P +* (while>0 (a,I))),(Initialized s),n) & ((StepWhile>0 (a,P,s,I)) . k) . (intloc 0) = 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))),(Initialized s),(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . k)))) + 3))) ) proofend; theorem :: SCMISORT:18 for P being Instruction-Sequence of SCM+FSA 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_Values_of SCM+FSA)),NAT st for k being Element of 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_closed_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) ) ) & ((StepWhile>0 (a,P,s,I)) . (k + 1)) . (intloc 0) = 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 & while>0 (a,I) is_closed_onInit s,P ) proofend; theorem Th19: :: SCMISORT:19 for I being InitHalting good Program 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 st s . a > 0 holds (IExec (I,P,s)) . a < s . a ) holds while>0 (a,I) is InitHalting proofend; theorem Th20: :: SCMISORT:20 for I being InitHalting good Program 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 proofend; theorem :: SCMISORT:21 for I being InitHalting good Program of SCM+FSA for a being read-write Int-Location st ex f being Function of (product (the_Values_of SCM+FSA)),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 proofend; theorem Th22: :: SCMISORT:22 for P being Instruction-Sequence of SCM+FSA 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)),P,s)) = DataPart (Initialized s) proofend; theorem Th23: :: SCMISORT:23 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitHalting good 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)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) proofend; theorem Th24: :: SCMISORT:24 for P being Instruction-Sequence of SCM+FSA 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)),P,s)) . f = s . f proofend; theorem Th25: :: SCMISORT:25 for P being Instruction-Sequence of SCM+FSA 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)),P,s)) . b = (Initialized s) . b proofend; theorem Th26: :: SCMISORT:26 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitHalting good 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)),P,s)) . f = (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) . f proofend; theorem Th27: :: SCMISORT:27 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being InitHalting good 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)),P,s)) . b = (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) . b proofend; begin 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 Th28: :: SCMISORT:28 for f being FinSeq-Location holds UsedIntLoc (insert-sort f) = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} proofend; theorem Th29: :: SCMISORT:29 for f being FinSeq-Location holds UsedInt*Loc (insert-sort f) = {f} proofend; theorem Th30: :: SCMISORT:30 for k1, k2, k3, k4 being Instruction of SCM+FSA holds card (((k1 ";" k2) ";" k3) ";" k4) = 8 proofend; theorem Th31: :: SCMISORT:31 for k1, k2, k3, k4, k5 being Instruction of SCM+FSA holds card ((((k1 ";" k2) ";" k3) ";" k4) ";" k5) = 10 proofend; theorem Th32: :: SCMISORT:32 for f being FinSeq-Location holds card (insert-sort f) = 82 proofend; theorem Th33: :: SCMISORT:33 for f being FinSeq-Location for k being Element of NAT st k < 82 holds k in dom (insert-sort f) proofend; Lm1: for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds ( P . 0 = (intloc 2) := (intloc 0) & P . 1 = goto 2 & P . 2 = (intloc 3) := (intloc 0) & P . 3 = goto 4 & P . 4 = (intloc 4) := (intloc 0) & P . 5 = goto 6 & P . 6 = (intloc 5) := (intloc 0) & P . 7 = goto 8 & P . 8 = (intloc 6) := (intloc 0) & P . 9 = goto 10 & P . 10 = (intloc 1) :=len (fsloc 0) & P . 11 = goto 12 ) proofend; 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 0 -started State of SCM+FSA for P being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P holds ( ( for k being Element of NAT st k > 0 & k < 12 holds ( (Comput (P,s,k)) . (IC ) = k & (Comput (P,s,k)) . (intloc 0) = s . (intloc 0) & (Comput (P,s,k)) . (fsloc 0) = s . (fsloc 0) ) ) & (Comput (P,s,11)) . (intloc 1) = len (s . (fsloc 0)) & (Comput (P,s,11)) . (intloc 2) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 3) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 4) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 5) = s . (intloc 0) & (Comput (P,s,11)) . (intloc 6) = s . (intloc 0) ) proofend; 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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (1 + 1)) = (s . (intloc (1 + 1))) - 1 ) ) proofend; Lm4: for s being State of SCM+FSA for P being Instruction-Sequence 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))))))),P,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))))))),P,s)) . (intloc (1 + 1)) <= 0 ) proofend; 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 InitHalting good Program of SCM+FSA by Th20; Lm6: not ((((((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))) destroys intloc (3 + 1) proofend; Lm7: not ((((((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))) destroys intloc (0 + 1) proofend; Lm8: not (((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)))))) destroys intloc (0 + 1) proofend; Lm9: not ((((((((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)))))) destroys intloc (0 + 1) proofend; 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 & 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 InitHalting ) proofend; 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 InitHalting good Program of SCM+FSA proofend; 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 & 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 InitHalting ) proofend; theorem :: SCMISORT:34 ( insert-sort (fsloc 0) is keepInt0_1 & insert-sort (fsloc 0) 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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (fsloc 0) = s . (fsloc 0) proofend; 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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) ) proofend; 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)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . a = s . a proofend; 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 . (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))))))),Q,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))))))),Q,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))))))),Q,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))))))),Q,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))))))),Q,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))))))),Q,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))))))),Q,t)) . (intloc (3 + 1)) = (t . (intloc (3 + 1))) + 1 ) ) ) ) proofend; Lm17: for P being Instruction-Sequence of SCM+FSA 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))))))))),P,s)) . (fsloc 0) & 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))))))))),P,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))))))))),P,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)) ) ) ) ) ) proofend; 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 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)))),P,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)))),P,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)))))) ) proofend; Lm19: for k being Element of 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 . (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)))))),P,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)))))),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 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)))))),P,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)))))),P,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)))))),P,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)))))),P,s)) . (fsloc 0)) . i = (s . (fsloc 0)) . i ) ) proofend; Lm20: for s being State of SCM+FSA for P being Instruction-Sequence 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))))),P,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))))),P,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))))),P,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))))),P,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))))),P,s)) . (intloc (5 + 1)) = (s . (fsloc 0)) /. (abs (((len (s . (fsloc 0))) - (s . (intloc (0 + 1)))) + 1)) ) proofend; 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 for P being Instruction-Sequence 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))))))))),P,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))))))))),P,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))))))))),P,s)) . (fsloc 0)) . j holds x1 >= x2 ) ) proofend; theorem Th35: :: SCMISORT:35 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA holds ( s . (fsloc 0),(IExec ((insert-sort (fsloc 0)),P,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)),P,s)) . (fsloc 0)) . i & x2 = ((IExec ((insert-sort (fsloc 0)),P,s)) . (fsloc 0)) . j holds x1 >= x2 ) ) proofend; theorem Th36: :: SCMISORT:36 for i being Element of 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 ((fsloc 0) .--> w) c= s holds IC (Comput (P,s,i)) in dom Insert-Sort-Algorithm proofend; theorem Th37: :: SCMISORT:37 for s being State of SCM+FSA for t being FinSequence of INT for P being Instruction-Sequence of SCM+FSA st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> 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)) . (fsloc 0) = u ) proofend; theorem Th38: :: SCMISORT:38 for w being FinSequence of INT holds Initialized ((fsloc 0) .--> w) is Insert-Sort-Algorithm -autonomic proofend; registration cluster Insert-Sort-Algorithm -> non halt-free ; coherence not Insert-Sort-Algorithm is halt-free ; end; theorem :: SCMISORT:39 Insert-Sort-Algorithm , Initialize ((intloc 0) .--> 1) computes Sorting-Function proofend;