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 (1 + 1)) = 0 ) & ( 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 (1 + 1)) = (s . (intloc (1 + 1))) - 1 ) )
set s0 = Initialized s;
set s1 = Exec (AddTo (intloc (3 + 1)),(intloc 0 )),(Initialized s);

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

end;

intloc (1 + 1) <> intloc (3 + 1) by AMI_3:52;
then A1: (Exec (AddTo (intloc (3 + 1)),(intloc 0 )),(Initialized s)) . (intloc (1 + 1)) = (Initialized s) . (intloc (1 + 1)) by SCMFSA_2:90
.= s . (intloc (1 + 1)) by SCMFSA6C:3 ;
A2: (Exec (AddTo (intloc (3 + 1)),(intloc 0 )),(Initialized s)) . (intloc 0 ) = (Initialized s) . (intloc 0 ) by SCMFSA_2:90
.= 1 by SCMFSA6C:3 ;

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

end;