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))),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)))),s);
A1: (Exec (((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))),(Initialized s))) . (intloc (2 + 1)) = s . (intloc (2 + 1)) by Th10;
A2: (IExec ((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ';' (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))),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:9
.= s . (intloc (2 + 1)) by A1, SCMFSA_2:99 ;

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))),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))),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)))),s)) . (intloc (2 + 1)) 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)))) . (intloc (2 + 1)) by SCMFSA6C:7
.= s . (intloc (2 + 1)) by A2, SCMFSA_2:99 ;
:: 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))),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))),s)) . (intloc (2 + 1)) = (IExec ((Stop SCM+FSA),s)) . (intloc (2 + 1)) by SCM_HALT:54
.= s . (intloc (2 + 1)) by Th12 ;
:: thesis: verum

end;

end;