:: deftheorem defines IExec SCMPDS_4:def 5 :
for I being Program of
for s being State of SCMPDS
for P being Instruction-Sequence of SCMPDS holds IExec (I,P,s) = Result ((P +* (stop I)),s);