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 1;
hence UsedInt*Loc (while=0 (b,I)) = UsedInt*Loc (if=0 (b,(I ';' (Goto 0)),(Stop SCM+FSA))) by Lm3
.= (UsedInt*Loc (I ';' (Goto 0))) \/ (UsedInt*Loc (Stop SCM+FSA)) by Th14
.= ((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