proposition: Lemma joining_node : forall (c : Config) (s2 : Site), legal c -> rt c s2 = false -> forall s3 s4 : Site, parent c s3 s4 -> s2 <> s3.
proof: Proof. intros. unfold not in |- *. intro. rewrite H2 in H0. generalize H0. elim H1. intros. generalize (inc_dec_in s1 (bm c s0 owner) H4). intro. generalize (not_owner_inc3 c s0 owner H s1 H6). intro. generalize (positive_st c s1 s0 H7 H H6). intro. generalize (st_rt c s1 H H7 H8). rewrite H5. discriminate. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4