proposition: Lemma rcop3_trans_in_other_queue : s2 <> s3 \/ s4 <> owner -> In_queue Message (inc_dec s0) (bm (rec_copy3_trans c0 s1 s2) s3 s4) -> In_queue Message (inc_dec s0) (bm c0 s3 s4).
proof: Proof. simpl in |- *; intros. apply in_collect with (s1 := s1) (s2 := s2). generalize H0; rewrite post_elsewhere. auto. elim H; auto. Qed.
imports: init table_act mess_act