proposition: Remark sigma_ctrl_copy_pos : forall s0 : Site, (sigma_ctrl_copy s0 bom >= 0)%Z.
proof: Proof. intro; unfold sigma_ctrl_copy in |- *; apply sigma_pos; intro; apply ctrl_copy_pos. Qed.
imports: DistributedReferenceCounting.machine0.machine