proposition: Lemma D_first_out : forall q0 : queue Message, D_queue q0 -> D_queue (first_out Message q0).
proof: Proof. intros; elim H; simpl in |- *. apply D_empty. simple destruct qm. apply D_empty. intros; apply D_dec. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm