proposition: Lemma inc_dec_owner : forall (c : Config) (s1 s2 : Site), legal c -> s1 = owner \/ s2 <> owner -> forall s0 : Site, ~ In_queue Message (inc_dec s0) (bm c s1 s2).
proof: Proof. intros c s1 s2 H. elim H. simpl in |- *. intros; unfold not in |- *; auto. simple induction t; simpl in |- *; intros. apply not_in_queue_post. discriminate. auto. apply not_in_queue_collect. auto. apply not_in_queue_post. discriminate. apply not_in_queue_collect; auto. apply not_in_queue_post. discriminate. apply not_in_queue_collect. auto. apply not_in_queue_collect. auto. case (eq_queue_dec s3 s1 owner s2). intro; decompose [and] a. elim H2. intro. cut (s3 <> owner). intro. elim H6. rewrite H3; rewrite H5; auto. auto. intro. elim H3; auto. intro; rewrite post_elsewhere. apply not_in_queue_collect. auto. auto. apply not_in_queue_post. discriminate. auto. apply not_in_queue_post. discriminate. generalize (H1 H2 s4). intro. case (eq_queue_dec s0 s1 owner s2); intro. decompose [and] a. rewrite H4. rewrite H5. rewrite that_queue. generalize H3. rewrite <- H4; rewrite <- H5. 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. rewrite other_queue. auto. elim o; intro. left; auto. right; auto. case (eq_queue_dec s0 s1 s3 s2); intro. decompose [and] a. rewrite H3; rewrite H4; rewrite that_queue. apply not_in_q_shuffle with (q1 := q1) (q2 := q2). generalize (H1 H2 s4). rewrite H3 in e; rewrite H4 in e. rewrite e. auto. auto. rewrite other_queue. auto. elim o; intro; auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm