proposition: Lemma inc_dec_in_post2 : forall (b : Bag_of_message) (s0 s1 s2 s3 : Site) (m : Message), inc_dec_in_queue s1 (Post_message Message m b s2 s3 s0 owner) -> m <> inc_dec s1 -> inc_dec_in_queue s1 (b s0 owner).
proof: Proof. intros. generalize H. case (eq_queue_dec s2 s0 s3 owner). intros. decompose [and] a. generalize H1. rewrite H2; rewrite H3. rewrite post_here. generalize H0. elim m. simpl in |- *; auto. intro; intro. simpl in |- *. case (eq_site_dec s s1). intro; elim H4. rewrite e; auto. intuition. simpl in |- *; auto. intro. rewrite post_elsewhere. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4