theorem :: SCMFSA9A:43

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