proposition: Lemma parent_does_not_join2 : forall (c0 : Config) (s1 s2 s3 s4 : Site), legal c0 -> legal (rec_copy3_trans c0 s1 s2) -> parent (rec_copy3_trans c0 s1 s2) s3 s4 -> rt c0 s2 = false -> first Message (bm c0 s1 s2) = value Message copy -> s3 <> s2.
proof: Proof. intros. elim H1. intros. generalize (inc_dec_in s0 (bm (rec_copy3_trans c0 s1 s2) s5 owner) H5). intro. generalize (not_reflexive (rec_copy3_trans c0 s1 s2) H0 s0 s5 H6). intro. cut (s0 <> owner). intro. generalize (positive_st (rec_copy3_trans c0 s1 s2) s0 s5 H8 H0 H6). intro. generalize (st_rt (rec_copy3_trans c0 s1 s2) s0 H0 H8 H9). intro. generalize H5. simpl in |- *. intro. case (eq_site_dec s2 s5). intro. rewrite e; auto. intro. generalize H11. rewrite post_elsewhere. intro. generalize (inc_dec_in_collect2 (bm c0) copy s5 s1 s2 s0 H3 H12). intro. generalize (inc_dec_in s0 (bm c0 s5 owner) H13). intro. generalize (positive_st c0 s0 s5 H8 H H14). intro. generalize (st_rt c0 s0 H H8 H15). intro. unfold not in |- *. intro. rewrite H17 in H16. rewrite H16 in H2. discriminate. left; auto. apply (not_owner_inc3 (rec_copy3_trans c0 s1 s2) s5 owner H0). auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4