proposition: Lemma in_queue_post : forall (b : Bag_of_message) (s1 s2 s3 s4 : Site) (m1 m2 : Message), m1 <> m2 -> In_queue Message m1 (Post_message Message m2 b s3 s4 s1 s2) -> In_queue Message m1 (b s1 s2).
proof: Proof. intros. case (eq_queue_dec s3 s1 s4 s2). intro. decompose [and] a; generalize H0. rewrite H1; rewrite H2; rewrite post_here. simpl in |- *. intro. elim H3; intro. elim H; auto. auto. intro. generalize H0. rewrite post_elsewhere. auto. auto. Qed.
imports: DistributedReferenceCounting.machine4.invariant0 DistributedReferenceCounting.machine4.invariant1 DistributedReferenceCounting.machine4.invariant2 DistributedReferenceCounting.machine4.invariant3 DistributedReferenceCounting.machine4.invariant4