theorem :: SF_MASTR:47

for i, j being Instruction of SCM+FSA holds UsedI*Loc (i ";" j) = (UsedInt*Loc i) \/ (UsedInt*Loc j)