proposition: Lemma reduce_post_message_null : forall (m : Message) (s1 s2 s3 s4 : Site) (b : Bag_of_message), f m = 0%Z -> reduce Message f (Post_message Message m b s1 s2 s3 s4) = reduce Message f (b s3 s4).
proof: Proof. intros m s1 s2 s3 s4 b H. case (eq_queue_dec s1 s3 s2 s4). intros a. decompose [and] a. rewrite H0; rewrite H1. rewrite post_here. simpl in |- *. rewrite H. omega. intro o. rewrite post_elsewhere. auto. auto. Qed.
imports: List fifo table reduce sigma2