theorem :: SF_MASTR:31

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