theorem :: SF_MASTR:67

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