theorem :: SCMPDS_2:78

for k1 being Integer
for a being Int_position holds not saveIC (a,k1) is halting