JUMP (a =0_goto i1) <> {} ;
hence not a =0_goto i1 is sequential by AMISTD_1:13; :: thesis: verum