fact: Axiom sigma_weight_change_queue : forall (s1 s2 s3 : Site) (b : Bag_of_message) (q : queue Message), b s1 s2 = input Message dec (input Message (inc_dec s3) q) -> sigma_weight (change_queue (queue Message) b s1 s2 q) = (sigma_weight b - cardinal_count dec - cardinal_count (inc_dec s3))%Z.
imports: DistributedReferenceCounting.machine3.machine DistributedReferenceCounting.machine3.cardinal DistributedReferenceCounting.machine3.comm