let k1 be Integer; :: thesis: goto k1 is No-StopCode
A1: InsCode (goto k1) = 14 by SCMPDS_2:12;
InsCode (halt SCMPDS) = 0 by COMPOS_1:70;
hence goto k1 <> halt the InstructionsF of SCMPDS by A1; :: according to COMPOS_0:def 12 :: thesis: verum