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