proposition: Lemma decide_exist_non_empty_queue1 : forall (c : Config) (a : Site), legal c -> {(forall s2 : Site, In s2 LS -> bm c a s2 = empty Message)} + {~ (forall s2 : Site, In s2 LS -> s2 <> a -> bm c a s2 = empty Message)}.
proof: Proof. intros. elim LS. simpl in |- *. left; intros; contradiction. simpl in |- *. intros. elim (decide_empty_queue c a a0); intro. case (eq_site_dec a a0); intro. elim H0; intro. left; intros. elim H1; intros. rewrite <- H2. auto. apply a2. auto. right. unfold not in |- *; intros. elim b; intros. unfold not in |- *. apply H1. auto. intro. elim H3; auto. elim H0; intros. left; intros. case (eq_site_dec s2 a0); intro. rewrite e; auto. elim H1; intro. elim n0; auto. apply a2; auto. right. unfold not in |- *; intros. elim b; intros. unfold not in |- *. apply H1. auto. intro; elim H3; auto. elim H0; intros. case (eq_site_dec a a0); intro. elim b. rewrite e. rewrite empty_q_to_me. auto. auto. right. unfold not in |- *; intros. generalize (H1 a0); intro. cut (a0 = a0 \/ In a0 l). intro. generalize (H2 H3); intro. decompose [and] H4. elim b; auto. auto. right. unfold not in |- *; intro. elim b0. unfold not in |- *; intros. apply H1. auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8