thus InsCode (goto i1) is jump-only ; :: according to AMISTD_1:def 2 :: thesis: ( not goto i1 is sequential & not goto i1 is ins-loc-free )
JUMP (goto i1) <> {} ;
hence not goto i1 is sequential by AMISTD_1:13; :: thesis: not goto i1 is ins-loc-free
thus not JumpPart (goto i1) is empty ; :: according to COMPOS_0:def 8 :: thesis: verum