set i = return a;
A1: InsCode (halt SCMPDS) = 0 by RECDEF_2:def 1;
InsCode (return a) = 1 by SCMPDS_2:13;
then return a <> halt SCMPDS by A1;
hence return a is No-StopCode by COMPOS_0:def 12; :: thesis: verum