theorem :: SFMASTR2:22

for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being really-closed MacroInstruction of SCM+FSA st s . a <= 0 & s . (intloc 0) = 1 holds
(IExec ((times (a,I)),p,s)) | ((UsedILoc I) \/ FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations)