proposition: Lemma legal_alternate : forall (s0 : Site) (c0 : Config), legal c0 -> alternate (bm c0 s0 owner).
proof: Proof. intros; elim H. apply alt_init. simple induction t; unfold transition in |- *; intros. apply copy_trans_alt; trivial. apply rdec_trans_alt; trivial. apply rinc_trans_alt. apply (not_owner_first_inc c s3 s1 owner); auto. trivial. apply rcop1_trans_alt; trivial. apply rcop2_trans_alt; trivial. apply rcop3_trans_alt. trivial. apply legal_false_D; trivial. trivial. apply del_trans_alt; trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc