theorem :: SCMFSA9A:9

for b being Int-Location
for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if>0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)