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:27
.= ({b} \/ ((UsedIntLoc I) \/ {})) \/ (UsedIntLoc (Stop SCM+FSA)) by Th11
.= {b} \/ (UsedIntLoc I) by Th9 ;
:: thesis: verum