proposition: Lemma not_owner_inc : forall (c : Config) (s1 s2 : Site), legal c -> ~ In_queue Message (inc_dec owner) (bm c s1 s2).
proof: Proof. intro; intro; intro. intro. elim H. simpl in |- *. intuition. simple induction t; intros; simpl in |- *. apply not_in_post. discriminate. auto. apply not_in_collect. auto. apply not_in_post. discriminate. apply not_in_collect. auto. apply not_in_post. discriminate. apply not_in_collect. auto. apply not_in_collect. auto. apply not_in_post. injection. intuition. apply not_in_collect. auto. apply not_in_post. discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm