theorem :: SF_MASTR:30

for j being Instruction of SCM+FSA
for I being Program of holds UsedILoc (I ";" j) = (UsedILoc I) \/ (UsedIntLoc j)