proposition: Lemma four : forall c : Config, legal c -> (st c owner + sigma_yi c)%Z = sigma_xi c.
proof: Proof. intros; elim H; simpl in |- *. rewrite sigma_xi_init; rewrite sigma_yi_init; trivial. simple induction t; unfold transition in |- *; intros. rewrite copy_trans_st. rewrite copy_trans_sigma_xi. rewrite copy_trans_sigma_yi. case (eq_site_dec owner s1); intro; omega. rewrite rdec_trans_st. rewrite rdec_trans_sigma_xi. rewrite rdec_trans_sigma_yi. case (eq_site_dec owner s2); intro; omega. trivial. trivial. rewrite rinc_trans_st. rewrite rinc_trans_sigma_xi. rewrite rinc_trans_sigma_yi. rewrite case_eq; omega. trivial. trivial. apply (not_owner_inc c0 s3 s1 owner). trivial. apply first_in; auto. rewrite rcop1_trans_sigma_xi. rewrite rcop1_trans_sigma_yi. auto. trivial. trivial. rewrite rcop2_trans_sigma_xi. rewrite rcop2_trans_sigma_yi. auto. trivial. trivial. trivial. rewrite rcop3_trans_sigma_xi. rewrite rcop3_trans_sigma_yi. simpl in |- *; omega. trivial. trivial. trivial. trivial. rewrite del_trans_sigma_xi. rewrite del_trans_sigma_yi. auto. trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc