theorem :: SCMPDS_2:66

for k1, k2 being Integer
for a being Int_position holds not (a,k1) := k2 is halting