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