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))),(Initialize 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))),(Initialize 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))),(Initialize 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;