set i = a := k1;
InsCode (a := k1) = 2 by SCMPDS_2:14;
then a := k1 <> halt SCMPDS ;
hence a := k1 is No-StopCode ; :: thesis: verum