proposition: Lemma two : forall (c0 : Config) (s0 : Site), legal c0 -> s0 <> owner -> st c0 s0 = sigma_ctrl s0 (bm c0).
proof: Proof. intros; elim H; simpl in |- *. rewrite sigma_ctrl_init; auto. simple induction t; unfold transition in |- *; intros. rewrite copy_trans_sigma_ctrl. rewrite copy_trans_st. case (eq_site_dec s0 s1); intro; omega. rewrite rdec_trans_sigma_ctrl. rewrite rdec_trans_st. case (eq_site_dec s0 s2); intro; omega. trivial. rewrite rinc_trans_sigma_ctrl. rewrite rinc_trans_st. rewrite case_ineq; auto. trivial. trivial. rewrite rcop1_trans_sigma_ctrl; auto. rewrite rcop2_trans_sigma_ctrl; auto. rewrite rcop3_trans_sigma_ctrl; auto. rewrite del_trans_sigma_ctrl; auto. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc