let p be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA holds (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)) . (intloc (2 + 1)) = s . (intloc (2 + 1))
let s be State of SCM+FSA; :: thesis: (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)) . (intloc (2 + 1)) = s . (intloc (2 + 1))
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: (Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (2 + 1)) = s . (intloc (2 + 1)) by Th3;
A2: (IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),p,s)) . (intloc (2 + 1)) = (Exec ((((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1))),(Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))))) . (intloc (2 + 1)) by SCMFSA6C:8
.= s . (intloc (2 + 1)) by A1, SCMFSA_2:73 ;
per cases ( s . (intloc (5 + 1)) > 0 or s . (intloc (5 + 1)) <= 0 ) ;
suppose s . (intloc (5 + 1)) > 0 ; :: thesis: (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)) . (intloc (2 + 1)) = s . (intloc (2 + 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)) . (intloc (2 + 1)) = (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)) . (intloc (2 + 1)) 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)))) . (intloc (2 + 1)) by SCMFSA6C:6
.= s . (intloc (2 + 1)) by A2, SCMFSA_2:73 ;
:: thesis: verum
end;
suppose s . (intloc (5 + 1)) <= 0 ; :: thesis: (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)) . (intloc (2 + 1)) = s . (intloc (2 + 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)) . (intloc (2 + 1)) = (IExec ((Stop SCM+FSA),p,s)) . (intloc (2 + 1)) by SCM_HALT:44
.= s . (intloc (2 + 1)) by Th5 ;
:: thesis: verum
end;
end;