proposition: Lemma decide_no_message : forall c : Config, {no_message c} + {~ no_message c}.
proof: Proof. intros. unfold no_message in |- *. simpl in |- *. pattern LS at 1 3 in |- *. elim LS. simpl in |- *. left; intros; contradiction. simpl in |- *. intros. elim H. clear H. elim LS. simpl in |- *. intro. left. intros; contradiction. intros. elim H. intros. elim (decide_empty_queue c a a0); intro. left. simpl in |- *. intros. elim H0; intro. elim H1; intro. rewrite <- H2; rewrite <- H3; auto. apply a2. auto. auto. elim H1; intro. apply a1. auto. simpl in |- *. auto. apply a2. auto. auto. right. unfold not in |- *. intro. generalize (H0 a a0). intro. elim b. apply H1. auto. simpl in |- *; auto. intro. right. unfold not in |- *; intro. elim b. intros. apply H0. auto. simpl in |- *; auto. intros. apply a1. auto. simpl in |- *; auto. intro. right. unfold not in |- *; intro. elim b. intros. apply H0. auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8