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