theorem :: SCMFSA8C:96

for aa being Int-Location
for I, J being MacroInstruction of SCM+FSA st not I destroys aa & not J destroys aa holds
not I ';' J destroys aa by Lm1;