proposition: Remark sigma_ctrl_inc_strct_pos : forall s0 s1 : Site, In_queue Message (inc_dec s0) (bom s1 owner) -> (sigma_ctrl_inc s0 bom > 0)%Z.
proof: Proof. intros; unfold sigma_ctrl_inc in |- *. generalize (le_sigma Site LS (fun si : Site => ctrl_inc s0 si bom) s1 (ctrl_inc_pos s0) (in_s_LS s1)); intros. generalize (ctrl_inc_strct_pos s0 s1 H); intro; omega. Qed.
imports: DistributedReferenceCounting.machine0.machine