thus
InsCode (a =0_goto i1) is jump-only
; :: according to AMISTD_1:def 2 :: thesis: ( not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free )

JUMP (a =0_goto i1) <> {} ;

hence not a =0_goto i1 is sequential by AMISTD_1:13; :: thesis: not a =0_goto i1 is ins-loc-free

thus not JumpPart (a =0_goto i1) is empty ; :: according to COMPOS_0:def 8 :: thesis: verum

JUMP (a =0_goto i1) <> {} ;

hence not a =0_goto i1 is sequential by AMISTD_1:13; :: thesis: not a =0_goto i1 is ins-loc-free

thus not JumpPart (a =0_goto i1) is empty ; :: according to COMPOS_0:def 8 :: thesis: verum