theorem Th21: :: SFMASTR3:23

for a being read-write Int-Location
for aa, bb, cc being Int-Location
for I being MacroInstruction of SCM+FSA st a <> aa & aa <> 1 -stRWNotIn ({a,bb,cc} \/ (UsedILoc I)) & not I destroys aa holds
not for-up (a,bb,cc,I) destroys aa