theorem :: SF_MASTR:66

for I being MacroInstruction of SCM+FSA
for k being Nat holds UsedILoc (I ';' (goto k)) = UsedILoc I