theorem :: SF_MASTR:29
for i being Instruction of SCM+FSA
for J being Program of holds UsedILoc (i ";" J) = (UsedIntLoc i) \/ (UsedILoc J)