thus InsCode (a =0_goto i1) is jump-only ; :: according to AMISTD_1:def 4 :: 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:43; :: thesis: not a =0_goto i1 is ins-loc-free
dom (JumpPart (a =0_goto i1)) = dom <*i1*> by Th24
.= {1} by FINSEQ_1:4, FINSEQ_1:55 ;
hence not JumpPart (a =0_goto i1) is empty ; :: according to AMISTD_2:def 13 :: thesis: verum