theorem :: SCM_HALT:24

for s being State of SCM+FSA
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA
for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . f = (Exec (j,(IExec (I,p,s)))) . f