let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA holds
( (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))),p,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))),p,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))),p,s)) . (fsloc 0) = s . (fsloc 0) )
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))),p,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))),p,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))),p,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)))),p,s);
set s3 = IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))),p,s);
A1: (Exec (((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s))) . (intloc (1 + 1)) =
(Initialized s) . (intloc (0 + 1))
by SCMFSA_2:63
.=
s . (intloc (0 + 1))
by SCMFSA_M:37
;
A2: (Exec (((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s))) . (fsloc 0) =
(Initialized s) . (fsloc 0)
by SCMFSA_2:63
.=
s . (fsloc 0)
by SCMFSA_M:37
;
A3: (Exec (((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s))) . (intloc 0) =
(Initialized s) . (intloc 0)
by SCMFSA_2:63
.=
1
by SCMFSA_M:9
;
A4: (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))),p,s)) . (fsloc 0) =
(Exec ((SubFrom ((intloc (1 + 1)),(intloc 0))),(Exec (((intloc (1 + 1)) := (intloc (0 + 1))),(Initialized s))))) . (fsloc 0)
by SCMFSA6C:9
.=
s . (fsloc 0)
by A2, SCMFSA_2:65
;
A5: (IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))),p,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:8
.=
(s . (intloc (0 + 1))) - 1
by A1, A3, SCMFSA_2:65
;
thus (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))),p,s)) . (intloc (1 + 1)) =
(Exec (((intloc (2 + 1)) :=len (fsloc 0)),(IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))),p,s)))) . (intloc (1 + 1))
by SCMFSA6C:6
.=
(s . (intloc (0 + 1))) - 1
by A5, Lm10, SCMFSA_2:74
; ( (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))),p,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))),p,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))),p,s)) . (intloc (2 + 1)) =
(Exec (((intloc (2 + 1)) :=len (fsloc 0)),(IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))),p,s)))) . (intloc (2 + 1))
by SCMFSA6C:6
.=
len (s . (fsloc 0))
by A4, SCMFSA_2:74
; (IExec (((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))),p,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))),p,s)) . (fsloc 0) =
(Exec (((intloc (2 + 1)) :=len (fsloc 0)),(IExec ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))),p,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
s . (fsloc 0)
by A4, SCMFSA_2:74
; verum