theorem Th6: :: SFMASTR3:7

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