proposition: Remark sigma_ctrl_copy_init : forall s0 : Site, sigma_ctrl_copy s0 bag_init = 0%Z.
proof: Proof. intros; unfold sigma_ctrl_copy in |- *; apply sigma_null. Qed.
imports: DistributedReferenceCounting.machine0.machine counting