proposition: Lemma not_reflexive : forall c : Config, legal c -> forall s1 s5 : Site, In_queue Message (inc_dec s1) (bm c s5 owner) -> s1 <> s5.
proof: Proof. intros c H. elim H. simpl in |- *. intuition. intros c0 t. elim t. simpl in |- *. intros. apply H1. apply (in_post Message (inc_dec s0) copy (bm c0) s1 s2). discriminate. auto. simpl in |- *. intros. apply H1. apply (in_collect Message (inc_dec s0) (bm c0) s1 s2). auto. simpl in |- *. intros. apply H1. apply (in_collect Message (inc_dec s0) (bm c0) s1 owner). generalize H2. simpl in |- *. case (eq_queue_dec owner s5 s3 owner). intro. decompose [and] a. rewrite H4; rewrite H3. rewrite post_here. simpl in |- *. intuition. discriminate. intro. rewrite post_elsewhere. auto. auto. simpl in |- *. intros. apply H1. apply (in_collect Message (inc_dec s0) (bm c0) s1 s2). generalize H2. case (eq_queue_dec s2 s5 s1 owner). intro. decompose [and] a. rewrite H3; rewrite H4. rewrite post_here. simpl in |- *. intuition. discriminate. intro. rewrite post_elsewhere. auto. auto. simpl in |- *. intros. apply H1. apply (in_collect Message (inc_dec s1) (bm c0) owner s2). auto. simpl in |- *; intros. case (eq_site_dec s2 s5); intro. generalize H2; rewrite e1. rewrite post_here. simpl in |- *. case (eq_queue_dec s1 s5 s5 owner). intro. decompose [and] a. elim n. rewrite H3; auto. intro. rewrite collect_elsewhere. generalize (H1 s0 s5). intro. case (eq_site_dec s0 s1). intro. rewrite <- e1; rewrite e2. unfold not in |- *. intro. intro. generalize e0. rewrite H5. rewrite empty_q_to_me. simpl in |- *. discriminate. auto. intros. apply H3. elim H4; intro. elim n1; inversion H5. auto. auto. auto. generalize H2. rewrite post_elsewhere. intro. apply H1. apply (in_collect Message (inc_dec s0) (bm c0) s1 s2). auto. left; auto. simpl in |- *. intros. apply H1. apply (in_post Message (inc_dec s1) dec (bm c0) s owner). discriminate. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm