proposition: Lemma rcop1_trans_D : D_queue (bm c0 s0 owner) -> D_queue (bm (rec_copy1_trans c0 s1 s2) s0 owner).
proof: Proof. simpl in |- *; intros. case (eq_queue_dec s2 s0 s1 owner); intro. decompose [and] a; rewrite H0; rewrite H1. apply D_post_dec. apply D_post_elsewhere. trivial. apply D_collect; trivial. Qed.
imports: init table_act mess_act