proposition: Lemma not_in_post : forall (m m' : Message) (bom : Bag_of_message) (s1 s2 s3 s4 : Site), m <> m' -> ~ In_queue Message m (bom s3 s4) -> ~ In_queue Message m (Post_message Message m' bom s1 s2 s3 s4).
proof: Proof. intros m m' bom s1 s2 s3 s4; case (eq_queue_dec s1 s3 s2 s4); intro. decompose [and] a; rewrite H; rewrite H0. rewrite post_here. intros H1 H2. simpl in |- *. intuition. intros H H0. rewrite post_elsewhere. auto. auto. Qed.
imports: List fifo table reduce sigma2