for i being Instruction of SCM+FSA
for a being Int-Location
for s being State of SCM+FSA st not i destroys a holds
(Exec (i,s)) . a = s . a