for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for I being really-closed InitHalting Program of SCM+FSA
for f being FinSeq-Location st not f in UsedI*Loc I holds
(IExec (I,p,s)) . f = s . f