set i = AddTo (a,k1,k2);
InsCode (AddTo (a,k1,k2)) = 8 by SCMPDS_2:20;
then AddTo (a,k1,k2) <> halt SCMPDS ;
hence AddTo (a,k1,k2) is No-StopCode ; :: thesis: verum