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 Th10
.= ((UsedInt*Loc I) \/ (UsedInt*Loc (Goto 0))) \/ (UsedInt*Loc (Stop SCM+FSA)) by SF_MASTR:43
.= (UsedInt*Loc I) \/ {} by Th4, Th6
.= UsedInt*Loc I ;
:: thesis: verum