let k1 be Integer; :: thesis: ( k1 <> 0 implies goto k1 is No-StopCode )
set i = goto k1;
assume A1: k1 <> 0 ; :: thesis: goto k1 is No-StopCode
assume not goto k1 is No-StopCode ; :: thesis: contradiction
then goto k1 = halt SCMPDS by COMPOS_1:def 24;
hence contradiction by A1, SCMPDS_2:73; :: thesis: verum