theorem :: SCMPDS_2:27

for ins being Instruction of SCMPDS st InsCode ins = 1 holds
ex a being Int_position st ins = return a