let s be State of SCM+FSA ; :: thesis: ( ( s . (intloc (4 + 1)) > 0 implies (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) . (intloc (3 + 1)) = s . (intloc (3 + 1)) ) & ( s . (intloc (4 + 1)) <= 0 implies (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) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 ) )
set s0 = Initialize s;
A1: intloc (1 + 1) <> intloc (3 + 1) by AMI_3:52;

hereby :: thesis: ( s . (intloc (4 + 1)) <= 0 implies (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) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1 )

assume 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) . (intloc (3 + 1)) = s . (intloc (3 + 1))
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) . (intloc (3 + 1)) = (IExec (Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),s) . (intloc (3 + 1)) by SCM_HALT:54
.= (Exec (SubFrom (intloc (1 + 1)),(intloc (1 + 1))),(Initialize s)) . (intloc (3 + 1)) by SCMFSA6C:6
.= (Initialize s) . (intloc (3 + 1)) by A1, SCMFSA_2:91
.= s . (intloc (3 + 1)) by SCMFSA6C:3 ;
:: thesis: verum

end;

hereby :: thesis: verum

assume 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) . (intloc (3 + 1)) = (s . (intloc (3 + 1))) + 1
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) . (intloc (3 + 1)) = (IExec ((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))),s) . (intloc (3 + 1)) by SCM_HALT:54
.= (Exec (SubFrom (intloc (1 + 1)),(intloc 0 )),(Exec (AddTo (intloc (3 + 1)),(intloc 0 )),(Initialize s))) . (intloc (3 + 1)) by SCMFSA6C:9
.= (Exec (AddTo (intloc (3 + 1)),(intloc 0 )),(Initialize s)) . (intloc (3 + 1)) by A1, SCMFSA_2:91
.= ((Initialize s) . (intloc (3 + 1))) + ((Initialize s) . (intloc 0 )) by SCMFSA_2:90
.= ((Initialize s) . (intloc (3 + 1))) + 1 by SCMFSA6C:3
.= (s . (intloc (3 + 1))) + 1 by SCMFSA6C:3 ;
:: thesis: verum

end;