theorem Th24: :: SCMFSA9A:24

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