for f being FinSeq-Location
for i being Instruction of SCM+FSA
for s being State of SCM+FSA st not f in UsedInt*Loc i holds
(Exec (i,s)) . f = s . f