let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA holds
( ( s . (intloc (4 + 1)) > 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) & ( s . (intloc (4 + 1)) <= 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) )
let s be State of SCM+FSA; ( ( s . (intloc (4 + 1)) > 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) & ( s . (intloc (4 + 1)) <= 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) )
set s0 = Initialized s;
A1:
intloc (1 + 1) <> intloc (3 + 1)
by SCMFSA_2:101;
hereby ( s . (intloc (4 + 1)) <= 0 implies (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 )
assume
s . (intloc (4 + 1)) > 0
;
(IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = s . (intloc (3 + 1))hence (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) =
(IExec ((Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),P,s)) . (intloc (3 + 1))
by SCM_HALT:44
.=
(IExec ((Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),P,s)) . (intloc (3 + 1))
.=
(Exec ((SubFrom ((intloc (1 + 1)),(intloc (1 + 1)))),(Initialized s))) . (intloc (3 + 1))
by SCMFSA6C:5
.=
(Exec ((SubFrom ((intloc (1 + 1)),(intloc (1 + 1)))),(Initialized s))) . (intloc (3 + 1))
.=
(Initialized s) . (intloc (3 + 1))
by A1, SCMFSA_2:65
.=
s . (intloc (3 + 1))
by SCMFSA_M:37
;
verum
end;
assume
s . (intloc (4 + 1)) <= 0
; (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1
hence (IExec ((if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))))),P,s)) . (intloc (3 + 1)) =
(IExec (((AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))),P,s)) . (intloc (3 + 1))
by SCM_HALT:44
.=
(Exec ((SubFrom ((intloc (1 + 1)),(intloc 0))),(Exec ((AddTo ((intloc (3 + 1)),(intloc 0))),(Initialized s))))) . (intloc (3 + 1))
by SCMFSA6C:8
.=
(Exec ((AddTo ((intloc (3 + 1)),(intloc 0))),(Initialized s))) . (intloc (3 + 1))
by A1, SCMFSA_2:65
.=
((Initialized s) . (intloc (3 + 1))) + ((Initialized s) . (intloc 0))
by SCMFSA_2:64
.=
((Initialized s) . (intloc (3 + 1))) + 1
by SCMFSA_M:9
.=
(s . (intloc (3 + 1))) + 1
by SCMFSA_M:37
;
verum