proposition: Lemma sigma_weight_collect_message : forall (m : Message) (s1 s2 : Site) (b : Bag_of_message), first Message (b s1 s2) = value Message m -> sigma_weight (Collect_message Message b s1 s2) = (sigma_weight b - cardinal_count m)%Z.
proof: Proof. unfold sigma_weight in |- *. unfold Collect_message in |- *. unfold change_queue in |- *. intros. rewrite sigma_table2_change. rewrite cardinal_first_out with (m := m). omega. auto. apply finite_site. apply finite_site. Qed.
imports: reduce DistributedReferenceCounting.machine2.cardinal sigma2 sum