proposition: Remark aux3 : forall (s1 s2 : Site) (q : queue Message), (cardinal q - sigma_but Site owner eq_site_dec LS (fun s : Site => rooted s s1 s2 q))%Z = reduce Message (fun a : Message => (cardinal_count a - sigma_but Site owner eq_site_dec LS (fun s : Site => rooted_fun s s1 s2 a))%Z) q.
proof: Proof. intros. unfold rooted in |- *. unfold cardinal in |- *. rewrite permute_sigma_but_reduce. rewrite <- disjoint_reduce3. unfold fun_minus in |- *. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3