proposition: Lemma inc_dec_owner4 : forall (c : Config) (s1 s2 : Site), legal c -> s1 = owner -> forall s0 : Site, ~ In_queue Message (inc_dec s0) (bm c s1 s2).
proof: Proof. intros. apply inc_dec_owner; auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm