theorem Th1: :: SFMASTR2:1

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