proposition: Lemma exist_non_empty_queue : forall c : Config, legal c -> ~ no_message c -> exists s1 : Site, (exists s2 : Site, s1 <> s2 /\ bm c s1 s2 <> empty Message).
proof: Proof. unfold no_message in |- *. intro. pattern LS at 1 in |- *. elim LS. simpl in |- *. intros. elim H0. intros; contradiction. simpl in |- *. intros a l H HLeg. elim (decide_exist_non_empty_queue1 c a HLeg); intro. intro. apply H. auto. unfold not in |- *; intro. elim H0; intros. elim H2; intro. rewrite <- H4. apply a0. auto. apply H1. auto. auto. intros. split with a. generalize b. elim LS. simpl in |- *. intro. elim b0; intros; contradiction. clear H. clear H0. clear b. simpl in |- *. intros. elim (decide_empty_queue c a a0); intro. apply H. unfold not in |- *; intros. elim b; intros. elim H1; intro. rewrite <- H3; auto. apply H0. auto. auto. case (eq_site_dec a a0); intro. elim b0; rewrite e; rewrite empty_q_to_me; auto. split with a0. split; auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8