proposition: Lemma not_inc_dec_in : forall q : queue Message, (forall s : Site, ~ inc_dec_in_queue s q) -> forall s : Site, ~ In_queue Message (inc_dec s) q.
proof: Proof. simple induction q. simpl in |- *. auto. intro. case d. simpl in |- *. intros. intuition. discriminate. eauto. intros. generalize (H0 s). intro. elim H1. simpl in |- *. case (eq_site_dec s s). auto. intro; elim n; auto. intro; simpl in |- *. intros. intuition. discriminate. eauto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4