proposition: Lemma decide_inc_dec_in_queue : forall s : Site, {s1 : Site | inc_dec_in_queue s1 (bm c0 s owner)} + {(forall s1 : Site, ~ inc_dec_in_queue s1 (bm c0 s owner))}.
proof: Proof. intros. elim (bm c0 s owner). simpl in |- *. intuition. intros. case d. simpl in |- *. auto. simpl in |- *. intros. left. split with s0. case (eq_site_dec s0 s0). auto. intro; elim n; auto. simpl in |- *; auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4