proposition: Lemma rooted_first_out : forall (s0 s1 s2 : Site) (q : queue Message) (m : Message), first Message q = value Message m -> rooted s0 s1 s2 (first_out Message q) = (rooted s0 s1 s2 q - rooted_fun s0 s1 s2 m)%Z.
proof: Proof. intros. unfold rooted in |- *. apply reduce_first_out. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm