proposition: Lemma decide_no_copy_successor : forall c : Config, legal c -> (exists t : class_trans c, ~ copy_p c t /\ legal (transition c t)) \/ (forall t : class_trans c, copy_p c t).
proof: Proof. intros. elim (decide_no_message c); intro. elim (decide_no_rt c); intro. right. intros. apply blocked_config2. auto. auto. auto. elim b. intros. decompose [and] H0. generalize (null_st c x H H1 a). intro. left. split with (delete_entry c x H3 H2 H1). split. unfold copy_p in |- *. unfold not in |- *; contradiction. apply after. auto. elim (exist_non_empty_queue c H b). intros. elim H0. intros. decompose [and] H1. generalize (not_empty_implies_last Message (bm c x x0) H3). intro. elim H4. intros. generalize (always_process_messages c H x x0 x1 H5). intro. elim H6. intros. decompose [and] H7. left. split with x2. split. unfold copy_p in |- *. generalize H9. case x2. simpl in |- *. intros. generalize H10. case (eq_queue_dec s1 x s2 x0); intro. decompose [and] a0. rewrite H11; rewrite H12. rewrite post_here. generalize (different_queue1 Message (bm c x x0) copy). intros. elim H11; auto. rewrite post_elsewhere. generalize (different_queue2 Message (bm c x x0) x1 H5). intros. elim H11; auto. auto. intros; unfold not in |- *; auto. intros; unfold not in |- *; auto. intros; unfold not in |- *; auto. intros; unfold not in |- *; auto. intros; unfold not in |- *; auto. intros; unfold not in |- *; auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8