let b be Int-Location; for I being MacroInstruction of SCM+FSA holds UsedILoc (while=0 (b,I)) = {b} \/ (UsedILoc I)
let I be MacroInstruction of SCM+FSA ; 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 Lm3
.=
(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
; verum