theorem :: SCMPDS_2:65

for k1 being Integer
for a being Int_position holds not a := k1 is halting