theorem Th2: :: SCMPDS_8:3

for t being State of SCMPDS
for i being Instruction of SCMPDS st InsCode i in {0,4,5,6,14} holds
Initialize t = Initialize (Exec (i,t))