let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA holds
( ( s . (intloc (5 + 1)) > 0 implies (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = ((s . (fsloc 0)) +* (|.(s . (intloc (2 + 1))).|,((s . (fsloc 0)) /. |.(s . (intloc (3 + 1))).|))) +* (|.(s . (intloc (3 + 1))).|,(s . (intloc (4 + 1)))) ) & ( s . (intloc (5 + 1)) <= 0 implies (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = s . (fsloc 0) ) )
let s be State of SCM+FSA; ( ( s . (intloc (5 + 1)) > 0 implies (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = ((s . (fsloc 0)) +* (|.(s . (intloc (2 + 1))).|,((s . (fsloc 0)) /. |.(s . (intloc (3 + 1))).|))) +* (|.(s . (intloc (3 + 1))).|,(s . (intloc (4 + 1)))) ) & ( s . (intloc (5 + 1)) <= 0 implies (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = s . (fsloc 0) ) )
set s0 = Initialized s;
set s1 = Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s));
set s2 = IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),p,s);
A1:
(Initialized s) . (fsloc 0) = s . (fsloc 0)
by SCMFSA_M:37;
(Initialized s) . (intloc (3 + 1)) = s . (intloc (3 + 1))
by SCMFSA_M:37;
then A2:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (5 + 1)) = (s . (fsloc 0)) /. |.(s . (intloc (3 + 1))).|
by A1, Th1;
A3:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (fsloc 0) = s . (fsloc 0)
by A1, SCMFSA_2:72;
A4:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (2 + 1)) = s . (intloc (2 + 1))
by Th3;
A5:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (3 + 1)) = s . (intloc (3 + 1))
by Th3;
A6:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (4 + 1)) = s . (intloc (4 + 1))
by Th3;
A7: (IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),p,s)) . (fsloc 0) =
(Exec ((((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1))),(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))))) . (fsloc 0)
by SCMFSA6C:9
.=
(s . (fsloc 0)) +* (|.(s . (intloc (2 + 1))).|,((s . (fsloc 0)) /. |.(s . (intloc (3 + 1))).|))
by A2, A3, A4, Th2
;
A8: (IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),p,s)) . (intloc (3 + 1)) =
(Exec ((((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1))),(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))))) . (intloc (3 + 1))
by SCMFSA6C:8
.=
s . (intloc (3 + 1))
by A5, SCMFSA_2:73
;
A9: (IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),p,s)) . (intloc (4 + 1)) =
(Exec ((((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1))),(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))))) . (intloc (4 + 1))
by SCMFSA6C:8
.=
s . (intloc (4 + 1))
by A6, SCMFSA_2:73
;
set I = (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)));
set J = Stop SCM+FSA;
hereby ( s . (intloc (5 + 1)) <= 0 implies (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = s . (fsloc 0) )
assume
s . (intloc (5 + 1)) > 0
;
(IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = ((s . (fsloc 0)) +* (|.(s . (intloc (2 + 1))).|,((s . (fsloc 0)) /. |.(s . (intloc (3 + 1))).|))) +* (|.(s . (intloc (3 + 1))).|,(s . (intloc (4 + 1))))hence (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) =
(IExec (((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),p,s)) . (fsloc 0)
by SCM_HALT:44
.=
(Exec ((((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1))),(IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),p,s)))) . (fsloc 0)
by SCMFSA6C:7
.=
((s . (fsloc 0)) +* (|.(s . (intloc (2 + 1))).|,((s . (fsloc 0)) /. |.(s . (intloc (3 + 1))).|))) +* (
|.(s . (intloc (3 + 1))).|,
(s . (intloc (4 + 1))))
by A7, A8, A9, Th2
;
verum
end;
assume
s . (intloc (5 + 1)) <= 0
; (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) = s . (fsloc 0)
hence (IExec ((if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))),p,s)) . (fsloc 0) =
(IExec ((Stop SCM+FSA),p,s)) . (fsloc 0)
by SCM_HALT:44
.=
s . (fsloc 0)
by Th5
;
verum