theorem :: SCMPDS_2:68

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