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))),s)) . (fsloc 0) = ((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs (s . (intloc (3 + 1))))))) +* ((abs (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))),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)))),s);
A1:
(Initialized s) . (fsloc 0) = s . (fsloc 0)
by SCMFSA6C:3;
(Initialized s) . (intloc (3 + 1)) = s . (intloc (3 + 1))
by SCMFSA6C:3;
then A2:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (5 + 1)) = (s . (fsloc 0)) /. (abs (s . (intloc (3 + 1))))
by A1, Th8;
A3:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (fsloc 0) = s . (fsloc 0)
by A1, SCMFSA_2:98;
A4:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (2 + 1)) = s . (intloc (2 + 1))
by Th10;
A5:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (3 + 1)) = s . (intloc (3 + 1))
by Th10;
A6:
(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (4 + 1)) = s . (intloc (4 + 1))
by Th10;
A7: (IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),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:10
.=
(s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs (s . (intloc (3 + 1))))))
by A2, A3, A4, Th9
;
A8: (IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),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:9
.=
s . (intloc (3 + 1))
by A5, SCMFSA_2:99
;
A9: (IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),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:9
.=
s . (intloc (4 + 1))
by A6, SCMFSA_2:99
;
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))),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))),s)) . (fsloc 0) = ((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs (s . (intloc (3 + 1))))))) +* ((abs (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))),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)))),s)) . (fsloc 0)
by SCM_HALT:54
.=
(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)))),s)))) . (fsloc 0)
by SCMFSA6C:8
.=
((s . (fsloc 0)) +* ((abs (s . (intloc (2 + 1)))),((s . (fsloc 0)) /. (abs (s . (intloc (3 + 1))))))) +* (
(abs (s . (intloc (3 + 1)))),
(s . (intloc (4 + 1))))
by A7, A8, A9, Th9
;
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))),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))),s)) . (fsloc 0) =
(IExec ((Stop SCM+FSA),s)) . (fsloc 0)
by SCM_HALT:54
.=
s . (fsloc 0)
by Th12
;
verum