let s be State of SCM+FSA ; :: thesis: (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (fsloc 0 ) = s . (fsloc 0 )
set s0 = Initialized s;

per cases ( s . (intloc (4 + 1)) > 0 or s . (intloc (4 + 1)) <= 0 ) ;

suppose s . (intloc (4 + 1)) > 0 ; :: thesis: (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (fsloc 0 ) = s . (fsloc 0 )

hence (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (fsloc 0 ) = (IExec (Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),s) . (fsloc 0 ) by SCM_HALT:54
.= (Exec (SubFrom (intloc (1 + 1)),(intloc (1 + 1))),(Initialized s)) . (fsloc 0 ) by SCMFSA6C:6
.= (Initialized s) . (fsloc 0 ) by SCMFSA_2:91
.= s . (fsloc 0 ) by SCMFSA6C:3 ;
:: thesis: verum

end;

suppose s . (intloc (4 + 1)) <= 0 ; :: thesis: (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (fsloc 0 ) = s . (fsloc 0 )

hence (IExec (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))),s) . (fsloc 0 ) = (IExec ((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),s) . (fsloc 0 ) by SCM_HALT:54
.= (Exec (SubFrom (intloc (1 + 1)),(intloc 0 )),(Exec (AddTo (intloc (3 + 1)),(intloc 0 )),(Initialized s))) . (fsloc 0 ) by SCMFSA6C:10
.= (Exec (AddTo (intloc (3 + 1)),(intloc 0 )),(Initialized s)) . (fsloc 0 ) by SCMFSA_2:91
.= (Initialized s) . (fsloc 0 ) by SCMFSA_2:90
.= s . (fsloc 0 ) by SCMFSA6C:3 ;
:: thesis: verum

end;

end;