proposition: Lemma legal_alternate : forall (s : Site) (c : Config), legal c -> alternate (bm c s owner) /\ (rt c s = false -> D_queue (bm c s owner)).
proof: Proof. intros. elim H. split. apply alt_null. simpl in |- *. intro. apply D_empty. simple induction t; simpl in |- *; intros. decompose [and] H1. split. case (eq_queue_dec s1 s s2 owner); intro. decompose [and] a0. rewrite H4; rewrite H5; rewrite post_here. apply alt_any_alt; auto. intro; discriminate. rewrite post_elsewhere. auto. auto. case (eq_site_dec s1 s); intro. generalize a; unfold access in |- *. rewrite e. intros. rewrite H4 in a0. discriminate. rewrite post_elsewhere. auto. left; auto. decompose [and] H1. split. apply alt_collect; auto. intro. apply D_collect; auto. decompose [and] H1. split. apply alt_post_elsewhere. right. apply (not_owner_inc3 c0 s1 owner H0 s3). apply first_in. auto. apply alt_collect; auto. intro. apply D_post_elsewhere. right. apply (not_owner_inc3 c0 s1 owner H0 s3). apply first_in. auto. apply D_collect. apply H3. auto. split. decompose [and] H1. case (eq_queue_dec s2 s s1 owner); intros. decompose [and] a. rewrite H4; rewrite H5. apply alt_post_any. intro; discriminate. apply alt_collect; auto. apply alt_post_elsewhere; auto. apply alt_collect; auto. decompose [and] H1. intro. case (eq_queue_dec s2 s s1 owner); intros; simpl in |- *. decompose [and] a. rewrite H5; rewrite H6. apply D_post_dec. apply alt_collect. decompose [and] H1; auto. rewrite post_elsewhere. apply D_collect. apply H3. auto. auto. decompose [and] H1; split. apply alt_collect; trivial. case (eq_site_dec s s2); intro. rewrite e1; unfold Set_rec_table in |- *; rewrite that_site. intro; discriminate. intro. apply D_collect. apply H3. generalize H4; unfold Set_rec_table in |- *; rewrite other_site; auto. decompose [and] H1; split. case (eq_site_dec s2 s); intro. rewrite e1; apply alt_post_inc. apply alt_collect; trivial. rewrite collect_elsewhere. rewrite e1 in e. generalize (H3 e). intro. elim H4. auto. simpl in |- *. intros. auto. rewrite <- e1. auto. apply alt_post_elsewhere; auto. apply alt_collect; trivial. case (eq_site_dec s s2); intro. rewrite e1; unfold Set_rec_table in |- *; rewrite that_site; intro; discriminate. intro. apply D_post_elsewhere; auto. apply D_collect; auto. apply H3. generalize H4; unfold Set_rec_table in |- *; rewrite other_site; auto. decompose [and] H1; split. case (eq_site_dec s0 s); intro. rewrite e1; apply alt_post_any; auto. intro; discriminate. apply alt_post_elsewhere; auto. case (eq_site_dec s0 s); intro. intro. rewrite e1. apply D_post_dec. auto. unfold Reset_rec_table in |- *; rewrite other_site. intro. apply D_post_elsewhere; auto. auto. decompose [and] H1; split. rewrite post_elsewhere. case (eq_site_dec s1 s); intro. rewrite e0. rewrite that_queue. rewrite e0 in e. rewrite e in H2. inversion H2. inversion H7. apply alt_null. auto. apply alt_any_alt. auto. auto. rewrite other_queue. auto. auto. right. apply (not_owner_inc3 c0 s1 owner). auto. rewrite e; simpl in |- *. right; left; auto. intro. rewrite post_elsewhere. case (eq_site_dec s1 s); intro. rewrite e0. rewrite that_queue. generalize (H3 H4). rewrite <- e0; rewrite e. intro. inversion H5. inversion H7. apply D_empty. generalize (H10 s2). intro. elim H12; auto. apply D_dec. auto. rewrite other_queue. apply H3; auto. auto. right. apply (not_owner_inc3 c0 s1 owner). auto. rewrite e. simpl in |- *. right; left; auto. Qed.
imports: DistributedReferenceCounting.machine3.alternate DistributedReferenceCounting.machine3.invariant0 DistributedReferenceCounting.machine3.invariant1 DistributedReferenceCounting.machine3.invariant2 DistributedReferenceCounting.machine3.invariant3 DistributedReferenceCounting.machine3.invariant4