let b be Int-Location ; :: thesis: for I being Program of SCM+FSA holds UsedInt*Loc (while>0 (b,I)) = UsedInt*Loc I
let I be Program of SCM+FSA; :: thesis: UsedInt*Loc (while>0 (b,I)) = UsedInt*Loc 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 UsedInt*Loc (while>0 (b,I)) = UsedInt*Loc (if>0 (b,(I ';' (Goto 0)),(Stop SCM+FSA))) by Lm6
.= (UsedInt*Loc (I ';' (Goto 0))) \/ (UsedInt*Loc (Stop SCM+FSA)) by Th16
.= ((UsedInt*Loc I) \/ (UsedInt*Loc (Goto 0))) \/ (UsedInt*Loc (Stop SCM+FSA)) by SF_MASTR:43
.= (UsedInt*Loc I) \/ {} by Th10, Th12
.= UsedInt*Loc I ;
:: thesis: verum