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:47
.= (UsedInt*Loc I) \/ {} by Th10, Th12
.= UsedInt*Loc I ;
:: thesis: verum