theorem :: SCMFSA8C:95

for s being State of SCM+FSA
for a being Int-Location
for p being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,p & not I destroys a holds
(IExec (I,p,s)) . a = (Initialized s) . a