InsCode (halt SCMPDS) = 0 by COMPOS_1:70;
hence for a being Int_position
for k1, k2 being Integer holds (a,k1) <>0_goto k2 <> halt SCMPDS by SCMPDS_2:16; :: thesis: verum