proposition: Lemma alt_first_out : forall q0 : queue Message, alternate q0 -> alternate (first_out Message q0).
proof: Proof. intros; elim H; simpl in |- *. apply alt_null. intro; apply alt_null. simple induction qm; intros. apply alt_null. apply alt_any_alt; trivial. simple induction qm; intros. apply alt_single_inc. apply alt_inc_dec; trivial. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm