theorem :: SCMFSA9A:7

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)