fact: Definition rooted (s1 s2 : Site) (q : queue Message) := reduce Message (rooted_fun s1 s2) q.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm