proposition: Lemma not_in_queue_collect : forall (b : Bag_of_message) (s1 s2 s3 s4 : Site) (m1 : Message), ~ In_queue Message m1 (b s1 s2) -> ~ In_queue Message m1 (Collect_message Message b s3 s4 s1 s2).
proof: Proof. intros. case (eq_queue_dec s3 s1 s4 s2). intro; decompose [and] a. rewrite H0; rewrite H1; rewrite collect_here. apply not_in_q_output. auto. intro; rewrite collect_elsewhere; auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm