theorem :: SCMFSA9A:10

for b being Int-Location
for I, J being MacroInstruction of SCM+FSA holds UsedI*Loc (if>0 (b,I,J)) = (UsedI*Loc I) \/ (UsedI*Loc J)