proposition: Lemma no_copy_to_owner : forall c0 : Config, legal c0 -> forall s1 : Site, ~ In_queue Message copy (bm c0 s1 owner).
proof: Proof. intros c0 H. elim H. intros. simpl in |- *. intuition. simple induction t; intros; simpl in |- *. rewrite post_elsewhere. auto. right; auto. case (eq_queue_dec s1 s0 s2 owner). intro. decompose [and] a. rewrite H2; rewrite H3. rewrite collect_here. apply not_in_q_output. auto. intro; rewrite collect_elsewhere. auto. auto. case (eq_queue_dec owner s3 s0 owner). intro. decompose [and] a. rewrite H3; rewrite <- H2. rewrite post_here. case (eq_site_dec s1 owner). intro. rewrite e0. rewrite collect_here. simpl in |- *. generalize (H1 owner). intro. generalize (not_in_q_output Message copy (bm c owner owner)). intro. generalize (H5 H4). intro. unfold not in |- *. intuition. discriminate. intro. rewrite collect_elsewhere. simpl in |- *. generalize (H1 owner). intuition. discriminate. left; auto. intro. rewrite post_elsewhere. case (eq_site_dec s1 s0). intro. rewrite e0. rewrite collect_here. apply not_in_q_output. auto. intro. rewrite collect_elsewhere. auto. auto. decompose [or] o. right; auto. left; auto. case (eq_queue_dec s2 s0 s1 owner). intro. decompose [and] a. rewrite H2; rewrite H3. rewrite post_here. case (eq_site_dec s0 owner). intro. rewrite e1; rewrite collect_here. simpl in |- *. generalize (not_in_q_output Message copy (bm c owner owner)). intro. generalize (H1 owner). intuition. discriminate. intro. rewrite collect_elsewhere. simpl in |- *. generalize (H1 s0). intuition. discriminate. right; auto. intro. rewrite post_elsewhere. case (eq_queue_dec s1 s0 s2 owner). intro. decompose [and] a. rewrite H2; rewrite H3; rewrite collect_here. apply not_in_q_output. auto. intro. rewrite collect_elsewhere. auto. auto. auto. case (eq_queue_dec owner s1 s2 owner). intro. decompose [and] a. rewrite <- H2; rewrite H3. rewrite collect_here. apply not_in_q_output. auto. intro. rewrite collect_elsewhere. auto. auto. case (eq_site_dec s2 s0). intro. rewrite e1. rewrite post_here. case (eq_queue_dec s1 s0 s0 owner). intro. decompose [and] a. rewrite H2; rewrite <- H3. rewrite collect_here. simpl in |- *. generalize (not_in_q_output Message copy (bm c s0 s0)). intros. generalize (H1 s0). rewrite H3. rewrite H3 in H4. intro. generalize (H4 H5). intuition. discriminate. intro. rewrite collect_elsewhere. simpl in |- *. generalize (H1 s0). intro. intuition. discriminate. discriminate. auto. intro. rewrite post_elsewhere. case (eq_queue_dec s1 s0 s2 owner). intros. decompose [and] a. rewrite H2; rewrite H3. rewrite collect_here. apply not_in_q_output. auto. intro. rewrite collect_elsewhere. auto. auto. left; auto. case (eq_site_dec s s1). intro. rewrite e1. rewrite post_here. simpl in |- *. generalize (H1 s1). intuition. discriminate. intro. rewrite post_elsewhere. auto. auto. Qed.
imports: DistributedReferenceCounting.machine1.machine DistributedReferenceCounting.machine1.cardinal DistributedReferenceCounting.machine1.comm