for s being State of SCMPDS
for I being Instruction of SCMPDS st InsCode I = 0 holds
Exec (I,s) = s by Lm11;