theorem :: SCMFSA6B:11

for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being parahalting keeping_0 Program of holds (IExec (I,P,s)) . (intloc 0) = 1