for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being really-closed Program of st ( I is_halting_on Initialized s,p or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedILoc I holds
(IExec (I,p,s)) . a = s . a