proposition: Lemma legal_alternate : forall (s : Site) (c : Config), legal c -> alternate (bm c s owner).
proof: Proof. intros; elim H. apply alt_null. simple induction t; simpl in |- *; intros. case (eq_queue_dec s1 s s2 owner); intro. decompose [and] a0. rewrite H2; rewrite H3; rewrite post_here. apply alt_any_alt; auto. intro; discriminate. rewrite post_elsewhere. auto. auto. apply alt_collect; auto. apply alt_post_elsewhere. right. apply (not_owner_inc3 c0 s1 owner H0 s3). apply first_in. auto. apply alt_collect; auto. case (eq_queue_dec s2 s s1 owner); intros. decompose [and] a. rewrite H2; rewrite H3. apply alt_post_any. intro; discriminate. apply alt_collect; auto. apply alt_post_elsewhere; auto. apply alt_collect; auto. apply alt_collect; trivial. case (eq_site_dec s2 s); intro. rewrite e1; apply alt_post_inc. apply alt_collect; trivial. rewrite collect_elsewhere. generalize (false_rt_D_queue c0 s2 H0 e); intro. rewrite e1 in H2. elim H2. auto. auto. case (eq_site_dec s1 s); intro. rewrite e2 in n; auto. auto. apply alt_post_elsewhere; auto. apply alt_collect; trivial. case (eq_site_dec s0 s); intro. rewrite e1; apply alt_post_any; auto. intro; discriminate. apply alt_post_elsewhere; auto. Qed.
imports: DistributedReferenceCounting.machine2.alternate DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4