proposition: Lemma rcop3_trans_alt : D_queue (bm c0 s2 owner) -> alternate (bm c0 s0 owner) -> alternate (bm (rec_copy3_trans c0 s1 s2) s0 owner).
proof: Proof. case (eq_site_dec s2 s0); intros; simpl in |- *. rewrite e; apply alt_post_inc. apply alt_collect; trivial. rewrite collect_elsewhere. rewrite e in H; elim H; auto. case (eq_site_dec s1 s0); intro. rewrite e0 in not_owner; auto. auto. apply alt_post_elsewhere. auto. apply alt_collect; trivial. Qed.
imports: init table_act mess_act