let b be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds UsedILoc (while>0 (b,I)) = {b} \/ (UsedILoc I)
let I be MacroInstruction of SCM+FSA ; :: thesis: UsedILoc (while>0 (b,I)) = {b} \/ (UsedILoc I)
set J = Stop SCM+FSA;
set a = b;
set IG = I ';' (goto 0);
A1: UsedILoc (I ';' (goto 0)) = UsedILoc I by SF_MASTR:66;
thus UsedILoc (while>0 (b,I)) = UsedILoc (if>0 (b,(I ';' (goto 0)))) by Lm5
.= (UsedILoc (((b >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0)))) \/ {} by Th3, SF_MASTR:27
.= (UsedILoc ((b >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1)))) \/ (UsedILoc I) by A1, SF_MASTR:27
.= ((UsedIntLoc (b >0_goto 3)) \/ (UsedILoc (Goto ((card (I ';' (goto 0))) + 1)))) \/ (UsedILoc I) by SF_MASTR:29
.= ((UsedIntLoc (b >0_goto 3)) \/ {}) \/ (UsedILoc I) by Th5
.= {b} \/ (UsedILoc I) by SF_MASTR:16 ; :: thesis: verum