proposition: Lemma reduce_collect_message_null : forall (m : Message) (s1 s2 s3 s4 : Site) (b : Bag_of_message), first Message (b s1 s2) = value Message m -> f m = 0%Z -> reduce Message f (Collect_message Message b s1 s2 s3 s4) = reduce Message f (b s3 s4).
proof: Proof. intros m s1 s2 s3 s4 b H H0. case (eq_queue_dec s1 s3 s2 s4). intros a. decompose [and] a. rewrite H1; rewrite H2. rewrite collect_here. rewrite reduce_first_out with (m := m). rewrite H0. omega. rewrite <- H1; rewrite <- H2; auto. intro o. rewrite collect_elsewhere. auto. auto. Qed.
imports: List fifo table reduce sigma2