theorem :: SCMFSA8A:42

for I being Program of SCM+FSA
for a being Int-Location
for k being Nat
for i being Instruction of SCM+FSA st not I destroys a & not i destroys a holds
not I +* (k,i) destroys a