proposition: Lemma always_process_messages : forall c : Config, legal c -> forall (s1 s2 : Site) (m : Message), first Message (bm c s1 s2) = value Message m -> exists t : class_trans c, legal (transition c t) /\ bm (transition c t) s1 s2 = first_out Message (bm c s1 s2).
proof: Proof. intros c H. generalize H. elim H. simpl in |- *. intros; discriminate. intros c0 t H0 H1 H2 s1 s2 m. case m. intro. split with (receive_dec (transition c0 t) s1 s2 H3). split. apply after. auto. simpl in |- *. rewrite collect_here. auto. intros. case (eq_site_dec s2 owner); intro. rewrite e in H3. split with (receive_inc (transition c0 t) s1 s H3). split. apply after. auto. simpl in |- *. rewrite post_elsewhere. rewrite e. rewrite collect_here. auto. left; unfold not in |- *; intro. generalize H3; rewrite H4; rewrite empty_q_to_me. simpl in |- *. intro; discriminate. auto. generalize (inc_dec_owner3 (transition c0 t) s1 s2 H2 n); intro. elim (H4 s). apply first_in. auto. elim (decide_rt (transition c0 t) s2); intro. case (eq_site_dec s1 owner); intro. intro. rewrite e in H3. split with (receive_copy2 (transition c0 t) s2 a H3). split. apply after. auto. simpl in |- *. rewrite e; rewrite collect_here; auto. intro. cut (s2 <> owner). intro. split with (receive_copy3 (transition c0 t) s1 s2 a n H4 H3). split. apply after. auto. simpl in |- *. rewrite post_elsewhere. rewrite collect_here; auto. left. unfold not in |- *; intro; generalize H3. rewrite H5; rewrite empty_q_to_me. simpl in |- *; intro. discriminate. auto. unfold not in |- *; intro; generalize a. rewrite H4; rewrite owner_rt_true. auto with bool. auto. intro. split with (receive_copy1 (transition c0 t) s1 s2 b H3). split. apply after; auto. simpl in |- *. rewrite post_elsewhere. rewrite collect_here. auto. case (eq_site_dec s1 s2); intro. generalize H3; rewrite e; rewrite empty_q_to_me. simpl in |- *; intro; discriminate. auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8