:: deftheorem defines IExec SCMFSA6B:def 1 :
for I being Program of
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds IExec (I,P,s) = Result ((P +* I),(Initialized s));