proposition: Lemma inc_dec_not_in_post : forall (b : Bag_of_message) (s0 s1 s2 s3 : Site) (m : Message), ~ inc_dec_in_queue s1 (b s0 owner) -> (forall s4 : Site, m <> inc_dec s4) -> ~ inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner).
proof: Proof. intros. unfold not in |- *. intro. elim H. apply (inc_dec_in_post2 b s0 s1 s2 s3 m). auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4