proposition: Lemma copy_diff_site : forall (c0 : Config) (s1 s2 : Site), legal c0 -> In_queue Message copy (bm c0 s1 s2) -> s1 <> s2.
proof: Proof. intros c0 s1 s2 Hlegal; elim Hlegal. intros; apply init_copy_diff_site; trivial. simple induction t; unfold transition in |- *; intros. apply copy_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial. apply rdec_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial. apply rinc_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial. apply rcop1_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial. apply rcop2_trans_diff_site with (c0 := c) (s2 := s0); trivial. apply rcop3_trans_diff_site with (c0 := c) (s1 := s0) (s2 := s3); trivial. apply del_trans_diff_site with (c0 := c) (s0 := s); trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc