fact: Definition sigma_rooted (bm : Bag_of_message) := sigma2_table Site LS LS (queue Message) rooted bm.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm