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. apply not_in_post. discriminate. case (eq_queue_dec s0 s1 owner s2). intro. decompose [and] a. rewrite H2; rewrite <- H3. rewrite that_queue. generalize H1. rewrite <- H2; rewrite <- H3; rewrite e. intro. apply not_in_q_input2 with (d' := inc_dec s3). exact eq_message_dec. apply not_in_q_input2 with (d' := dec). exact eq_message_dec. auto. intro. rewrite other_queue. auto. elim o; intro. auto. auto. case (eq_queue_dec s0 s1 s3 s2); intro. decompose [and] a. rewrite H2; rewrite H3; rewrite that_queue. rewrite H2 in e; rewrite H3 in e. rewrite e in H1. apply not_in_q_shuffle with (q1 := q1) (q2 := q2). auto. auto. rewrite other_queue. auto. elim o; intro; auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm