let k1, k2 be Integer; for a being Int_position holds not AddTo (a,k1,k2) is halting
let a be Int_position; not AddTo (a,k1,k2) is halting
set s = the State of SCMPDS;
(Exec ((AddTo (a,k1,k2)), the State of SCMPDS)) . (IC ) = (IC the State of SCMPDS) + 1
by Th45;
hence
not AddTo (a,k1,k2) is halting
by Th60; verum