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