proposition: Lemma last_successor_has_no_message : forall y0 : legal_config, no_message (get_c (last_successor y0)).
proof: Proof. intros. generalize (last_successor_is_last y0). intro. elim (decide_no_message (get_c (last_successor y0))). auto. generalize H. elim (last_successor y0). simpl in |- *. intro; intro. elim p. intros. generalize (exist_non_empty_queue c l b). intro. elim H1; intro. intro. elim H2. intro. intros. decompose [and] H3. generalize (not_empty_implies_last Message (bm c x0 x1) H5); intro. elim H6. intros. generalize (always_process_messages c l x0 x1 x2 H7); intro. elim H8; intro. intro. decompose [and] H9. elim (H0 (existS legal_as_set (transition c x3) (intro_leg (transition c x3) H10))). unfold no_copy_succ in |- *. unfold get_c in |- *. split with x3. split. auto. unfold copy_p in |- *. generalize H11. elim x3; simpl in |- *; intros. generalize H12. case (eq_queue_dec s1 x0 s2 x1); intro. decompose [and] a0. rewrite H13; rewrite H14. rewrite post_here. generalize (different_queue1 Message (bm c x0 x1) copy). intros. elim H13; auto. rewrite post_elsewhere. generalize (different_queue2 Message (bm c x0 x1) x2 H7). intros. elim H13; auto. auto. tauto. tauto. tauto. tauto. tauto. tauto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8