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