set DD = {(intloc 0),(IC ),(fsloc 0)};
let w be FinSequence of INT ; :: thesis: Initialized ((fsloc 0) .--> w) is Insert-Sort-Algorithm -autonomic
set p = Initialized ((fsloc 0) .--> w);
set q = Insert-Sort-Algorithm ;
set UD = {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)};
set Us = (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm);
A3: UsedIntLoc Insert-Sort-Algorithm = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by Th38;
A4: UsedInt*Loc Insert-Sort-Algorithm = {(fsloc 0)} by Th39;
then A5: (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) = {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by A3, ENUMSET1:22;
A6: for i being Element of NAT
for s1, s2 being State of SCM+FSA
for P1, P2 being Instruction-Sequence of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )

proof

let i be Element of NAT ; :: thesis: for s1, s2 being State of SCM+FSA
for P1, P2 being Instruction-Sequence of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )
let s1, s2 be State of SCM+FSA; :: thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 holds
( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )
let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: ( 11 <= i & Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 implies ( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) ) )
assume that
A7: 11 <= i and
A8: Initialized ((fsloc 0) .--> w) c= s1 and
A9: Initialized ((fsloc 0) .--> w) c= s2 and
A10: Insert-Sort-Algorithm c= P1 and
A11: Insert-Sort-Algorithm c= P2 ; :: thesis: ( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) )
A12: s1 . (intloc 0) = 1 by A8, SCMBSORT:30
.= s2 . (intloc 0) by A9, SCMBSORT:30 ;
A13: s2 is 0 -started by A9, MEMSTR_0:17;
set Cs11 = Comput (P1,s1,11);
set Cs21 = Comput (P2,s2,11);
A14: s1 is 0 -started by A8, MEMSTR_0:17;
A15: s1 . (fsloc 0) = w by A8, SCMBSORT:30
.= s2 . (fsloc 0) by A9, SCMBSORT:30 ;

A16: now

let x be set ; :: thesis: ( x in (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) implies (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁ )
assume x in (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁
then A17: x in {(fsloc 0),(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)} by A4, A3, ENUMSET1:22;

per cases ( x = fsloc 0 or x = intloc 0 or x = intloc 1 or x = intloc 2 or x = intloc 3 or x = intloc 4 or x = intloc 5 or x = intloc 6 ) by A17, ENUMSET1:def 6;

suppose A18: x = fsloc 0 ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁

hence (Comput (P1,s1,11)) . x = s1 . (fsloc 0) by A14, Lm2, A10
.= (Comput (P2,s2,11)) . x by A13, A15, A18, Lm2, A11 ;
:: thesis: verum

end;

suppose A19: x = intloc 0 ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁

hence (Comput (P1,s1,11)) . x = s1 . (intloc 0) by A14, Lm2, A10
.= (Comput (P2,s2,11)) . x by A13, A12, A19, Lm2, A11 ;
:: thesis: verum

end;

suppose A20: x = intloc 1 ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁

hence (Comput (P1,s1,11)) . x = len (s1 . (fsloc 0)) by A14, Lm2, A10
.= (Comput (P2,s2,11)) . x by A13, A15, A20, Lm2, A11 ;
:: thesis: verum

end;

suppose A21: x = intloc 2 ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁

hence (Comput (P1,s1,11)) . x = s1 . (intloc 0) by A14, Lm2, A10
.= (Comput (P2,s2,11)) . x by A13, A12, A21, Lm2, A11 ;
:: thesis: verum

end;

suppose A22: x = intloc 3 ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁

hence (Comput (P1,s1,11)) . x = s1 . (intloc 0) by A14, Lm2, A10
.= (Comput (P2,s2,11)) . x by A13, A12, A22, Lm2, A11 ;
:: thesis: verum

end;

suppose A23: x = intloc 4 ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁

hence (Comput (P1,s1,11)) . x = s1 . (intloc 0) by A14, Lm2, A10
.= (Comput (P2,s2,11)) . x by A13, A12, A23, Lm2, A11 ;
:: thesis: verum

end;

suppose A24: x = intloc 5 ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁

hence (Comput (P1,s1,11)) . x = s1 . (intloc 0) by A14, Lm2, A10
.= (Comput (P2,s2,11)) . x by A13, A12, A24, Lm2, A11 ;
:: thesis: verum

end;

suppose A25: x = intloc 6 ; :: thesis: (Comput (P1,s1,11)) . b₁ = (Comput (P2,s2,11)) . b₁

hence (Comput (P1,s1,11)) . x = s1 . (intloc 0) by A14, Lm2, A10
.= (Comput (P2,s2,11)) . x by A13, A12, A25, Lm2, A11 ;
:: thesis: verum

end;

end;

end;

A26: for i being Element of NAT holds IC (Comput (P2,s2,i)) in dom Insert-Sort-Algorithm by A9, Th46, A11;
A27: for i being Element of NAT holds IC (Comput (P1,s1,i)) in dom Insert-Sort-Algorithm by A8, Th46, A10;
A28: (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) c= dom (Comput (P2,s2,11)) by SCMBSORT:32;
(UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) c= dom (Comput (P1,s1,11)) by SCMBSORT:32;
then A29: (Comput (P1,s1,11)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,11)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) by A28, A16, FUNCT_1:95;
(Comput (P1,s1,11)) . (IC ) = 11 by A14, Lm2, A10
.= (Comput (P2,s2,11)) . (IC ) by A13, Lm2, A11 ;
hence ( (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) ) by A7, A29, A27, A26, A10, A11, SCMBSORT:15; :: thesis: verum

end;

A30: for s1, s2 being State of SCM+FSA
for P1, P2 being Instruction-Sequence of SCM+FSA
for i being Element of NAT st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 & i <= 10 holds
( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

proof

let s1, s2 be State of SCM+FSA; :: thesis: for P1, P2 being Instruction-Sequence of SCM+FSA
for i being Element of NAT st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 & i <= 10 holds
( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: for i being Element of NAT st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 & i <= 10 holds
( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
let i be Element of NAT ; :: thesis: ( Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 & Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 & i <= 10 implies ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) ) )
assume that
A31: Initialized ((fsloc 0) .--> w) c= s1 and
A32: Initialized ((fsloc 0) .--> w) c= s2 and
A33: Insert-Sort-Algorithm c= P1 and
A34: Insert-Sort-Algorithm c= P2 and
A35: i <= 10 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
A36: s2 is 0 -started by A32, MEMSTR_0:17;
A37: s1 . (fsloc 0) = w by A31, SCMBSORT:30
.= s2 . (fsloc 0) by A32, SCMBSORT:30 ;
A38: s1 . (intloc 0) = 1 by A31, SCMBSORT:30
.= s2 . (intloc 0) by A32, SCMBSORT:30 ;
A39: Comput (P1,s1,0) = s1 by EXTPRO_1:2;
A40: s1 is 0 -started by A31, MEMSTR_0:17;
then A41: IC s1 = 0 by MEMSTR_0:def 8
.= IC s2 by A36, MEMSTR_0:def 8 ;

per cases ( i = 0 or i = 1 or i = 2 or i = 3 or i = 4 or i = 5 or i = 6 or i = 7 or i = 8 or i = 9 or i = 10 ) by A35, NAT_1:34;

suppose A42: i = 0 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) by A39, A38, EXTPRO_1:2; :: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) by A39, A41, A42, EXTPRO_1:2; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) by A39, A37, A42, EXTPRO_1:2; :: thesis: verum

end;

suppose A43: i = 1 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A43, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 1 by A40, A43, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A43, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A43, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A43, Lm2, A34 ; :: thesis: verum

end;

suppose A44: i = 2 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A44, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 2 by A40, A44, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A44, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A44, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A44, Lm2, A34 ; :: thesis: verum

end;

suppose A45: i = 3 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A45, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 3 by A40, A45, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A45, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A45, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A45, Lm2, A34 ; :: thesis: verum

end;

suppose A46: i = 4 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A46, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 4 by A40, A46, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A46, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A46, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A46, Lm2, A34 ; :: thesis: verum

end;

suppose A47: i = 5 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A47, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 5 by A40, A47, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A47, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A47, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A47, Lm2, A34 ; :: thesis: verum

end;

suppose A48: i = 6 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A48, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 6 by A40, A48, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A48, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A48, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A48, Lm2, A34 ; :: thesis: verum

end;

suppose A49: i = 7 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A49, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 7 by A40, A49, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A49, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A49, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A49, Lm2, A34 ; :: thesis: verum

end;

suppose A50: i = 8 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A50, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 8 by A40, A50, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A50, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A50, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A50, Lm2, A34 ; :: thesis: verum

end;

suppose A51: i = 9 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A51, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 9 by A40, A51, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A51, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A51, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A51, Lm2, A34 ; :: thesis: verum

end;

suppose A52: i = 10 ; :: thesis: ( (Comput (P1,s1,i)) . (intloc 0) = (Comput (P2,s2,i)) . (intloc 0) & (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )

hence (Comput (P1,s1,i)) . (intloc 0) = s1 . (intloc 0) by A40, Lm2, A33
.= (Comput (P2,s2,i)) . (intloc 0) by A36, A38, A52, Lm2, A34 ;
:: thesis: ( (Comput (P1,s1,i)) . (IC ) = (Comput (P2,s2,i)) . (IC ) & (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0) )
thus (Comput (P1,s1,i)) . (IC ) = 10 by A40, A52, Lm2, A33
.= (Comput (P2,s2,i)) . (IC ) by A36, A52, Lm2, A34 ; :: thesis: (Comput (P1,s1,i)) . (fsloc 0) = (Comput (P2,s2,i)) . (fsloc 0)
thus (Comput (P1,s1,i)) . (fsloc 0) = s1 . (fsloc 0) by A40, A52, Lm2, A33
.= (Comput (P2,s2,i)) . (fsloc 0) by A36, A37, A52, Lm2, A34 ; :: thesis: verum

end;

end;

end;

A53: dom (Initialized ((fsloc 0) .--> w)) = {(intloc 0),(IC ),(fsloc 0)} by SCMBSORT:21;
reconsider ini = (intloc 0) .--> 1 as data-only FinPartState of SCM+FSA ;
Initialized ((fsloc 0) .--> w) = ((fsloc 0) .--> w) +* (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:def 3;
then DataPart (Initialized ((fsloc 0) .--> w)) = (DataPart ((fsloc 0) .--> w)) +* (DataPart (Initialize ((intloc 0) .--> 1))) by FUNCT_4:71
.= (DataPart ((fsloc 0) .--> w)) +* (DataPart ((intloc 0) .--> 1)) by MEMSTR_0:45
.= ((fsloc 0) .--> w) +* (DataPart ini) by MEMSTR_0:7
.= ((fsloc 0) .--> w) +* ((intloc 0) .--> 1) by MEMSTR_0:7 ;
then A60: dom (DataPart (Initialized ((fsloc 0) .--> w))) = (dom ((fsloc 0) .--> w)) \/ (dom ((intloc 0) .--> 1)) by FUNCT_4:def 1
.= {(fsloc 0)} \/ (dom ((intloc 0) .--> 1)) by FUNCOP_1:13
.= {(fsloc 0)} \/ {(intloc 0)} by FUNCOP_1:13
.= {(intloc 0),(fsloc 0)} by ENUMSET1:1 ;
IC in {(intloc 0),(IC ),(fsloc 0)} by ENUMSET1:def 1;
then IC in dom (Initialized ((fsloc 0) .--> w)) by A53;
then A61: dom (Initialized ((fsloc 0) .--> w)) = {(IC )} \/ (dom (DataPart (Initialized ((fsloc 0) .--> w)))) by MEMSTR_0:24
.= {(IC ),(intloc 0),(fsloc 0)} by A60, ENUMSET1:2
.= {(intloc 0),(IC ),(fsloc 0)} by ENUMSET1:58 ;
for P, Q being Instruction-Sequence of SCM+FSA st Insert-Sort-Algorithm c= P & Insert-Sort-Algorithm c= Q holds
for s1, s2 being State of SCM+FSA st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
for i being Element of NAT holds (Comput (P,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (Q,s2,i)) | (dom (Initialized ((fsloc 0) .--> w)))

proof

let P1, P2 be Instruction-Sequence of SCM+FSA; :: thesis: ( Insert-Sort-Algorithm c= P1 & Insert-Sort-Algorithm c= P2 implies for s1, s2 being State of SCM+FSA st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized ((fsloc 0) .--> w))) )
assume that
A64: Insert-Sort-Algorithm c= P1 and
A65: Insert-Sort-Algorithm c= P2 ; :: thesis: for s1, s2 being State of SCM+FSA st Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 holds
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized ((fsloc 0) .--> w)))
let s1, s2 be State of SCM+FSA; :: thesis: ( Initialized ((fsloc 0) .--> w) c= s1 & Initialized ((fsloc 0) .--> w) c= s2 implies for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized ((fsloc 0) .--> w))) )
assume that
A62: Initialized ((fsloc 0) .--> w) c= s1 and
A63: Initialized ((fsloc 0) .--> w) c= s2 ; :: thesis: for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized ((fsloc 0) .--> w)))
let i be Element of NAT ; :: thesis: (Comput (P1,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized ((fsloc 0) .--> w)))
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
A66: (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) c= dom (Comput (P1,s1,i)) by SCMBSORT:32;
A67: fsloc 0 in (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) by A5, ENUMSET1:def 6;
A68: (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) c= dom (Comput (P2,s2,i)) by SCMBSORT:32;
A69: ( i > 10 implies 10 + 1 < i + 1 ) by XREAL_1:6;
A70: intloc 0 in (UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm) by A5, ENUMSET1:def 6;

A71: now

let x be set ; :: thesis: ( x in {(intloc 0),(IC ),(fsloc 0)} implies (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁ )
assume A72: x in {(intloc 0),(IC ),(fsloc 0)} ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

per cases ( x = intloc 0 or x = IC or x = fsloc 0 ) by A72, ENUMSET1:def 1;

suppose A73: x = intloc 0 ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

per cases ( i <= 10 or i > 10 ) ;

suppose i <= 10 ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A30, A62, A63, A73, A64, A65; :: thesis: verum

end;

suppose i > 10 ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

then 11 <= i by A69, NAT_1:13;
then (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) by A6, A62, A63, A64, A65;
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A70, A66, A68, A73, FUNCT_1:95; :: thesis: verum

end;

end;

end;

suppose A74: x = IC ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

per cases ( i <= 10 or i > 10 ) ;

suppose i <= 10 ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A30, A62, A63, A74, A64, A65; :: thesis: verum

end;

suppose i > 10 ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

then 11 <= i by A69, NAT_1:13;
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A6, A62, A63, A74, A64, A65; :: thesis: verum

end;

end;

end;

suppose A75: x = fsloc 0 ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

per cases ( i <= 10 or i > 10 ) ;

suppose i <= 10 ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A30, A62, A63, A75, A64, A65; :: thesis: verum

end;

suppose i > 10 ; :: thesis: (Comput (P1,s1,i)) . b₁ = (Comput (P2,s2,i)) . b₁

then 11 <= i by A69, NAT_1:13;
then (Comput (P1,s1,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) = (Comput (P2,s2,i)) | ((UsedInt*Loc Insert-Sort-Algorithm) \/ (UsedIntLoc Insert-Sort-Algorithm)) by A6, A62, A63, A64, A65;
hence (Comput (P1,s1,i)) . x = (Comput (P2,s2,i)) . x by A67, A66, A68, A75, FUNCT_1:95; :: thesis: verum

end;

end;

end;

end;

end;

A76: {(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (P2,s2,i)) by SCMBSORT:31;
{(intloc 0),(IC ),(fsloc 0)} c= dom (Comput (P1,s1,i)) by SCMBSORT:31;
then (Comput (P1,s1,i)) | {(intloc 0),(IC ),(fsloc 0)} = (Comput (P2,s2,i)) | {(intloc 0),(IC ),(fsloc 0)} by A76, A71, FUNCT_1:95;
hence (Comput (P1,s1,i)) | (dom (Initialized ((fsloc 0) .--> w))) = (Comput (P2,s2,i)) | (dom (Initialized ((fsloc 0) .--> w))) by A61; :: thesis: verum

end;

hence Initialized ((fsloc 0) .--> w) is Insert-Sort-Algorithm -autonomic by EXTPRO_1:def 10; :: thesis: verum