let s be State of SCM+FSA ; :: thesis:
assume that
A1: Insert-Sort-Algorithm c= s and
A2: s starts_at 0 ; :: thesis:
A3: Computation s,0 = s by AMI_1:13;
then A4: IC (Computation s,0 ) = insloc 0 by A2, AMI_1:def 41;
then A5: Computation s,(0 + 1) = Exec (s . (insloc 0 )),(Computation s,0 ) by AMI_1:55
.= Exec ((intloc 2) := (intloc 0 )),(Computation s,0 ) by A1, Lm1 ;
then A6: (Computation s,1) . (IC SCM+FSA ) = Next (IC (Computation s,0 )) by SCMFSA_2:89
.= insloc 1 by A4 ;
then A7: IC (Computation s,1) = insloc 1 ;
A8: (Computation s,1) . (intloc 2) = s . (intloc 0 ) by A3, A5, SCMFSA_2:89;
A9: intloc 2 <> intloc 0 by AMI_3:52;
then A10: (Computation s,1) . (intloc 0 ) = s . (intloc 0 ) by A3, A5, SCMFSA_2:89;
A11: (Computation s,1) . (fsloc 0 ) = s . (fsloc 0 ) by A3, A5, SCMFSA_2:89;
A12: Computation s,(1 + 1) = Exec (s . (insloc 1)),(Computation s,1) by A7, AMI_1:55
.= Exec (goto (insloc 2)),(Computation s,1) by A1, Lm1 ;
then A13: (Computation s,2) . (IC SCM+FSA ) = insloc 2 by SCMFSA_2:95;
A14: IC (Computation s,2) = insloc 2 by A12, SCMFSA_2:95;
A15: (Computation s,2) . (intloc 0 ) = s . (intloc 0 ) by A10, A12, SCMFSA_2:95;
A16: (Computation s,2) . (fsloc 0 ) = s . (fsloc 0 ) by A11, A12, SCMFSA_2:95;
A17: (Computation s,2) . (intloc 2) = s . (intloc 0 ) by A8, A12, SCMFSA_2:95;
A18: Computation s,(2 + 1) = Exec (s . (insloc 2)),(Computation s,2) by A14, AMI_1:55
.= Exec ((intloc 3) := (intloc 0 )),(Computation s,2) by A1, Lm1 ;
then A19: (Computation s,3) . (IC SCM+FSA ) = Next (IC (Computation s,2)) by SCMFSA_2:89
.= insloc 3 by A13 ;
then A20: IC (Computation s,3) = insloc 3 ;
A21: (Computation s,3) . (intloc 3) = s . (intloc 0 ) by A15, A18, SCMFSA_2:89;
A23: (Computation s,3) . (intloc 0 ) = s . (intloc 0 ) by A15, A18, SCMFSA_2:89;
A24: (Computation s,3) . (fsloc 0 ) = s . (fsloc 0 ) by A16, A18, SCMFSA_2:89;
intloc 2 <> intloc 3 by AMI_3:52;
then A25: (Computation s,3) . (intloc 2) = s . (intloc 0 ) by A17, A18, SCMFSA_2:89;
A26: Computation s,(3 + 1) = Exec (s . (insloc 3)),(Computation s,3) by A20, AMI_1:55
.= Exec (goto (insloc 4)),(Computation s,3) by A1, Lm1 ;
then A27: (Computation s,4) . (IC SCM+FSA ) = insloc 4 by SCMFSA_2:95;
A28: IC (Computation s,4) = insloc 4 by A26, SCMFSA_2:95;
A29: (Computation s,4) . (intloc 0 ) = s . (intloc 0 ) by A23, A26, SCMFSA_2:95;
A30: (Computation s,4) . (fsloc 0 ) = s . (fsloc 0 ) by A24, A26, SCMFSA_2:95;
A31: (Computation s,4) . (intloc 2) = s . (intloc 0 ) by A25, A26, SCMFSA_2:95;
A32: (Computation s,4) . (intloc 3) = s . (intloc 0 ) by A21, A26, SCMFSA_2:95;
A33: Computation s,(4 + 1) = Exec (s . (insloc 4)),(Computation s,4) by A28, AMI_1:55
.= Exec ((intloc 4) := (intloc 0 )),(Computation s,4) by A1, Lm1 ;
then A34: (Computation s,5) . (IC SCM+FSA ) = Next (IC (Computation s,4)) by SCMFSA_2:89
.= insloc 5 by A27 ;
then A35: IC (Computation s,5) = insloc 5 ;
A36: (Computation s,5) . (intloc 4) = s . (intloc 0 ) by A29, A33, SCMFSA_2:89;
A37: intloc 4 <> intloc 0 by AMI_3:52;
then A38: (Computation s,5) . (intloc 0 ) = s . (intloc 0 ) by A29, A33, SCMFSA_2:89;
A39: (Computation s,5) . (fsloc 0 ) = s . (fsloc 0 ) by A30, A33, SCMFSA_2:89;
intloc 2 <> intloc 4 by AMI_3:52;
then A40: (Computation s,5) . (intloc 2) = s . (intloc 0 ) by A31, A33, SCMFSA_2:89;
intloc 3 <> intloc 4 by AMI_3:52;
then A41: (Computation s,5) . (intloc 3) = s . (intloc 0 ) by A32, A33, SCMFSA_2:89;
A42: Computation s,(5 + 1) = Exec (s . (insloc 5)),(Computation s,5) by A35, AMI_1:55
.= Exec (goto (insloc 6)),(Computation s,5) by A1, Lm1 ;
then A43: (Computation s,6) . (IC SCM+FSA ) = insloc 6 by SCMFSA_2:95;
A44: IC (Computation s,6) = insloc 6 by A42, SCMFSA_2:95;
A45: (Computation s,6) . (intloc 0 ) = s . (intloc 0 ) by A38, A42, SCMFSA_2:95;
A46: (Computation s,6) . (fsloc 0 ) = s . (fsloc 0 ) by A39, A42, SCMFSA_2:95;
A47: (Computation s,6) . (intloc 2) = s . (intloc 0 ) by A40, A42, SCMFSA_2:95;
A48: (Computation s,6) . (intloc 3) = s . (intloc 0 ) by A41, A42, SCMFSA_2:95;
A49: (Computation s,6) . (intloc 4) = s . (intloc 0 ) by A36, A42, SCMFSA_2:95;
A50: Computation s,(6 + 1) = Exec (s . (insloc 6)),(Computation s,6) by A44, AMI_1:55
.= Exec ((intloc 5) := (intloc 0 )),(Computation s,6) by A1, Lm1 ;
then A51: (Computation s,7) . (IC SCM+FSA ) = Next (IC (Computation s,6)) by SCMFSA_2:89
.= insloc 7 by A43 ;
then A52: IC (Computation s,7) = insloc 7 ;
A53: (Computation s,7) . (intloc 5) = s . (intloc 0 ) by A45, A50, SCMFSA_2:89;
A54: intloc 5 <> intloc 0 by AMI_3:52;
then A55: (Computation s,7) . (intloc 0 ) = s . (intloc 0 ) by A45, A50, SCMFSA_2:89;
A56: (Computation s,7) . (fsloc 0 ) = s . (fsloc 0 ) by A46, A50, SCMFSA_2:89;
intloc 2 <> intloc 5 by AMI_3:52;
then A57: (Computation s,7) . (intloc 2) = s . (intloc 0 ) by A47, A50, SCMFSA_2:89;
intloc 3 <> intloc 5 by AMI_3:52;
then A58: (Computation s,7) . (intloc 3) = s . (intloc 0 ) by A48, A50, SCMFSA_2:89;
intloc 4 <> intloc 5 by AMI_3:52;
then A59: (Computation s,7) . (intloc 4) = s . (intloc 0 ) by A49, A50, SCMFSA_2:89;
A60: Computation s,(7 + 1) = Exec (s . (insloc 7)),(Computation s,7) by A52, AMI_1:55
.= Exec (goto (insloc 8)),(Computation s,7) by A1, Lm1 ;
then A61: (Computation s,8) . (IC SCM+FSA ) = insloc 8 by SCMFSA_2:95;
A62: IC (Computation s,8) = insloc 8 by A60, SCMFSA_2:95;
A63: (Computation s,8) . (intloc 0 ) = s . (intloc 0 ) by A55, A60, SCMFSA_2:95;
A64: (Computation s,8) . (fsloc 0 ) = s . (fsloc 0 ) by A56, A60, SCMFSA_2:95;
A65: (Computation s,8) . (intloc 2) = s . (intloc 0 ) by A57, A60, SCMFSA_2:95;
A66: (Computation s,8) . (intloc 3) = s . (intloc 0 ) by A58, A60, SCMFSA_2:95;
A67: (Computation s,8) . (intloc 4) = s . (intloc 0 ) by A59, A60, SCMFSA_2:95;
A68: (Computation s,8) . (intloc 5) = s . (intloc 0 ) by A53, A60, SCMFSA_2:95;
A69: Computation s,(8 + 1) = Exec (s . (insloc 8)),(Computation s,8) by A62, AMI_1:55
.= Exec ((intloc 6) := (intloc 0 )),(Computation s,8) by A1, Lm1 ;
then A70: (Computation s,9) . (IC SCM+FSA ) = Next (IC (Computation s,8)) by SCMFSA_2:89
.= insloc 9 by A61 ;
then A71: IC (Computation s,9) = insloc 9 ;
A72: (Computation s,9) . (intloc 6) = s . (intloc 0 ) by A63, A69, SCMFSA_2:89;
A73: intloc 6 <> intloc 0 by AMI_3:52;
then A74: (Computation s,9) . (intloc 0 ) = s . (intloc 0 ) by A63, A69, SCMFSA_2:89;
A75: (Computation s,9) . (fsloc 0 ) = s . (fsloc 0 ) by A64, A69, SCMFSA_2:89;
intloc 2 <> intloc 6 by AMI_3:52;
then A76: (Computation s,9) . (intloc 2) = s . (intloc 0 ) by A65, A69, SCMFSA_2:89;
intloc 3 <> intloc 6 by AMI_3:52;
then A77: (Computation s,9) . (intloc 3) = s . (intloc 0 ) by A66, A69, SCMFSA_2:89;
intloc 4 <> intloc 6 by AMI_3:52;
then A78: (Computation s,9) . (intloc 4) = s . (intloc 0 ) by A67, A69, SCMFSA_2:89;
intloc 5 <> intloc 6 by AMI_3:52;
then A79: (Computation s,9) . (intloc 5) = s . (intloc 0 ) by A68, A69, SCMFSA_2:89;
A80: Computation s,(9 + 1) = Exec (s . (insloc 9)),(Computation s,9) by A71, AMI_1:55
.= Exec (goto (insloc 10)),(Computation s,9) by A1, Lm1 ;
then A81: (Computation s,10) . (IC SCM+FSA ) = insloc 10 by SCMFSA_2:95;
A82: IC (Computation s,10) = insloc 10 by A80, SCMFSA_2:95;
A83: (Computation s,10) . (intloc 0 ) = s . (intloc 0 ) by A74, A80, SCMFSA_2:95;
A84: (Computation s,10) . (fsloc 0 ) = s . (fsloc 0 ) by A75, A80, SCMFSA_2:95;
A85: (Computation s,10) . (intloc 2) = s . (intloc 0 ) by A76, A80, SCMFSA_2:95;
A86: (Computation s,10) . (intloc 3) = s . (intloc 0 ) by A77, A80, SCMFSA_2:95;
A87: (Computation s,10) . (intloc 4) = s . (intloc 0 ) by A78, A80, SCMFSA_2:95;
A88: (Computation s,10) . (intloc 5) = s . (intloc 0 ) by A79, A80, SCMFSA_2:95;
A89: (Computation s,10) . (intloc 6) = s . (intloc 0 ) by A72, A80, SCMFSA_2:95;
A90: Computation s,(10 + 1) = Exec (s . (insloc 10)),(Computation s,10) by A82, AMI_1:55
.= Exec ((intloc 1) :=len (fsloc 0 )),(Computation s,10) by A1, Lm1 ;
then A91: (Computation s,11) . (IC SCM+FSA ) = Next (IC (Computation s,10)) by SCMFSA_2:100
.= insloc 11 by A81 ;

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume A93: ( k > 0 & k < 12 ) ; :: thesis:
then k < 11 + 1 ;
then A94: k <= 11 by NAT_1:13;
set c1 = (Computation s,k) . (IC SCM+FSA );
set d1 = insloc k;
set c2 = (Computation s,k) . (intloc 0 );
set d2 = s . (intloc 0 );
set c3 = (Computation s,k) . (fsloc 0 );
set d3 = s . (fsloc 0 );

per cases by A93, A94, NAT_1:36;

suppose k = 1 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A3, A5, A6, A9, SCMFSA_2:89; :: thesis:

end;

suppose k = 2 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A10, A11, A12, SCMFSA_2:95; :: thesis:

end;

suppose k = 3 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A15, A16, A18, A19, SCMFSA_2:89; :: thesis:

end;

suppose k = 4 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A23, A24, A26, SCMFSA_2:95; :: thesis:

end;

suppose k = 5 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A29, A30, A33, A34, A37, SCMFSA_2:89; :: thesis:

end;

suppose k = 6 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A38, A39, A42, SCMFSA_2:95; :: thesis:

end;

suppose k = 7 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A45, A46, A50, A51, A54, SCMFSA_2:89; :: thesis:

end;

suppose k = 8 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A55, A56, A60, SCMFSA_2:95; :: thesis:

end;

suppose k = 9 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A63, A64, A69, A70, A73, SCMFSA_2:89; :: thesis:

end;

suppose k = 10 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A74, A75, A80, SCMFSA_2:95; :: thesis:

end;

suppose k = 11 ; :: thesis:

hence ( (Computation s,k) . (IC SCM+FSA ) = insloc k & (Computation s,k) . (intloc 0 ) = s . (intloc 0 ) & (Computation s,k) . (fsloc 0 ) = s . (fsloc 0 ) ) by A83, A84, A90, A91, SCMFSA_2:100; :: thesis:

end;

thus (Computation s,11) . (intloc 1) = len (s . (fsloc 0 )) by A84, A90, SCMFSA_2:100; :: thesis:
intloc 2 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 2) = s . (intloc 0 ) by A85, A90, SCMFSA_2:100; :: thesis:
intloc 3 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 3) = s . (intloc 0 ) by A86, A90, SCMFSA_2:100; :: thesis:
intloc 4 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 4) = s . (intloc 0 ) by A87, A90, SCMFSA_2:100; :: thesis:
intloc 5 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 5) = s . (intloc 0 ) by A88, A90, SCMFSA_2:100; :: thesis:
intloc 6 <> intloc 1 by AMI_3:52;
hence (Computation s,11) . (intloc 6) = s . (intloc 0 ) by A89, A90, SCMFSA_2:100; :: thesis: