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