theorem :: SCMPDS_2:31

for ins being Instruction of SCMPDS st InsCode ins = 5 holds
ex a being Int_position ex k1, k2 being Integer st ins = (a,k1) <=0_goto k2