for a being Int_position
for k1, k2 being Integer holds (a,k1) >=0_goto k2 <> halt SCMPDS