proposition: Lemma not_owner_inc : forall (c : Config) (s0 s1 s2 : Site), legal c -> In_queue Message (inc_dec s0) (bm c s1 s2) -> s0 <> owner.
proof: Proof. intros c s0 s1 s2 H; elim H; simpl in |- *. contradiction. simple induction t; unfold transition in |- *; intros. apply H1; apply copy_trans_in_queue with (s1 := s3) (s2 := s4); trivial. apply H1; apply rdec_trans_in_queue with (s1 := s3) (s2 := s4); trivial. apply H1; apply rinc_trans_in_queue with (s1 := s3) (s2 := s4); trivial. apply H1; apply rcop1_trans_in_queue with (s1 := s3) (s2 := s4); trivial. apply H1; apply rcop2_trans_in_queue with (s2 := s3); trivial. case (eq_site_dec s0 s3); intro. rewrite e1; trivial. apply H1; apply rcop3_trans_in_queue with (s1 := s3) (s2 := s4); trivial. apply H1; apply del_trans_in_queue with (s1 := s); trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc