proposition: Lemma inc_dec_in : forall (s : Site) (q : queue Message), inc_dec_in_queue s q -> In_queue Message (inc_dec s) q.
proof: Proof. simple induction q. simpl in |- *. auto. simpl in |- *. intro. intro. intro. case d. intuition. intro. case (eq_site_dec s0 s). intro. rewrite e. intuition. intro. intuition. intuition. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4