let b be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedIntLoc (while>0 b,I) = {b} \/ (UsedIntLoc I)
let I be Program of SCM+FSA ; :: thesis: UsedIntLoc (while>0 b,I) = {b} \/ (UsedIntLoc I)
set J = Stop SCM+FSA ;
set a = b;
set IG = I ';' (Goto 0 );
while>0 b,I = (if>0 b,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )) by SCMFSA_9:def 2;
hence UsedIntLoc (while>0 b,I) = UsedIntLoc (if>0 b,(I ';' (Goto 0 )),(Stop SCM+FSA )) by Lm5
.= ({b} \/ (UsedIntLoc (I ';' (Goto 0 )))) \/ (UsedIntLoc (Stop SCM+FSA )) by Th15
.= ({b} \/ ((UsedIntLoc I) \/ (UsedIntLoc (Goto 0 )))) \/ (UsedIntLoc (Stop SCM+FSA )) by SF_MASTR:31
.= ({b} \/ ((UsedIntLoc I) \/ {} )) \/ (UsedIntLoc (Stop SCM+FSA )) by Th11
.= {b} \/ (UsedIntLoc I) by Th9 ;
:: thesis: verum