proposition: Lemma sigma_rooted_collect_message : forall (m : Message) (s0 s1 s2 : Site) (b : Bag_of_message), first Message (b s1 s2) = value Message m -> s0 <> owner -> sigma_rooted s0 (Collect_message Message b s1 s2) = (sigma_rooted s0 b - rooted_fun s0 s1 s2 m)%Z.
proof: Proof. unfold sigma_rooted, Collect_message, change_queue in |- *. intros. rewrite sigma_table2_change. rewrite (rooted_first_out s0 s1 s2 (b s1 s2) m). simpl in |- *. omega. auto. apply finite_site. apply finite_site. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm