let s be State of SCM+FSA ; ( (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (intloc (1 + 1)) = (s . (intloc (0 + 1))) - 1 & (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (intloc (2 + 1)) = len (s . (fsloc 0 )) & (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (fsloc 0 ) = s . (fsloc 0 ) )
set s0 = Initialized s;
set s1 = Exec ((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s);
set s2 = IExec (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),s;
set s3 = IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s;
A1: (Exec ((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s)) . (intloc (1 + 1)) =
(Initialized s) . (intloc (0 + 1))
by SCMFSA_2:89
.=
s . (intloc (0 + 1))
by SCMFSA6C:3
;
A2: (Exec ((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s)) . (fsloc 0 ) =
(Initialized s) . (fsloc 0 )
by SCMFSA_2:89
.=
s . (fsloc 0 )
by SCMFSA6C:3
;
A3: (Exec ((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s)) . (intloc 0 ) =
(Initialized s) . (intloc 0 )
by SCMFSA_2:89
.=
1
by SCMFSA6C:3
;
A4: (IExec (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),s) . (fsloc 0 ) =
(Exec (SubFrom (intloc (1 + 1)),(intloc 0 )),(Exec ((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s))) . (fsloc 0 )
by SCMFSA6C:10
.=
s . (fsloc 0 )
by A2, SCMFSA_2:91
;
A5: (IExec (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),s) . (intloc (1 + 1)) =
(Exec (SubFrom (intloc (1 + 1)),(intloc 0 )),(Exec ((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s))) . (intloc (1 + 1))
by SCMFSA6C:9
.=
(s . (intloc (0 + 1))) - 1
by A1, A3, SCMFSA_2:91
;
thus (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (intloc (1 + 1)) =
(Exec ((intloc (2 + 1)) :=len (fsloc 0 )),(IExec (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),s)) . (intloc (1 + 1))
by SCMFSA6C:7
.=
(s . (intloc (0 + 1))) - 1
by A5, Lm10, SCMFSA_2:100
; ( (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (intloc (2 + 1)) = len (s . (fsloc 0 )) & (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (fsloc 0 ) = s . (fsloc 0 ) )
thus (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (intloc (2 + 1)) =
(Exec ((intloc (2 + 1)) :=len (fsloc 0 )),(IExec (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),s)) . (intloc (2 + 1))
by SCMFSA6C:7
.=
len (s . (fsloc 0 ))
by A4, SCMFSA_2:100
; (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (fsloc 0 ) = s . (fsloc 0 )
thus (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 ))),s) . (fsloc 0 ) =
(Exec ((intloc (2 + 1)) :=len (fsloc 0 )),(IExec (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),s)) . (fsloc 0 )
by SCMFSA6C:8
.=
s . (fsloc 0 )
by A4, SCMFSA_2:100
; verum