proposition: Lemma empty_q_to_me : forall c : Config, legal c -> forall s : Site, bm c s s = empty Message.
proof: Proof. intros c H. elim H. intros. simpl in |- *. unfold bag_init in |- *. auto. simple induction t; intros; simpl in |- *. rewrite post_elsewhere; auto. apply not_s1_s2; auto. case (eq_site_dec s1 s2). intro; generalize e. rewrite e0. rewrite H1. simpl in |- *; intro; discriminate. intros. rewrite collect_elsewhere; auto. apply not_s1_s2; auto. generalize (not_owner_inc2 c0 s3 s1 owner H0). intros. rewrite post_elsewhere. case (eq_site_dec s1 owner). intro. generalize e. rewrite e0. rewrite H1. simpl in |- *; intro; discriminate. intros. rewrite collect_elsewhere; auto. apply not_s1_s2; auto. apply not_s1_s2; auto. cut (s3 <> owner). auto. apply H2. apply first_in. auto. case (eq_site_dec s1 s2). intro; generalize e0. rewrite e1. rewrite H1. simpl in |- *. intro; discriminate. intro. rewrite post_elsewhere. rewrite collect_elsewhere. auto. apply not_s1_s2. auto. apply not_s1_s2. auto. case (eq_site_dec owner s2). intro. generalize e0; rewrite e1; simpl in |- *. rewrite H1. simpl in |- *. intro; discriminate. intro. rewrite collect_elsewhere. auto. apply not_s1_s2. auto. case (eq_queue_dec s2 s owner s); intro. decompose [and] a. elim n0; rewrite H3; auto. rewrite post_elsewhere. case (eq_queue_dec s1 s s2 s); intro. decompose [and] a. generalize e0; rewrite H2; rewrite H3; rewrite H1. simpl in |- *; intro; discriminate. rewrite collect_elsewhere; auto. auto. rewrite post_elsewhere. auto. apply not_s1_s2. auto. rewrite post_elsewhere. rewrite other_queue. auto. case (eq_queue_dec s1 s owner s); intro. decompose [and] a. generalize e. rewrite H2; rewrite H3. rewrite H1. intro; discriminate. elim o; intro; auto. case (eq_queue_dec s1 s s2 s); intro. decompose [and] a. elim n. rewrite H2; rewrite H3; auto. auto. rewrite other_queue. auto. case (eq_queue_dec s s1 s s2); intro. decompose [and] a; elim n; auto. rewrite <- H2; rewrite <- H3; auto. auto. Qed.
imports: DistributedReferenceCounting.machine4.machine DistributedReferenceCounting.machine4.cardinal DistributedReferenceCounting.machine4.comm