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