proposition: Lemma ancestor_rt : forall c : Config, legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> rt c s1 = true.
proof: Proof. intros. elim H0. intros. elim H1. intros. generalize (inc_dec_in s4 (bm c s5 owner) H3). intro. generalize (not_owner_inc3 c s5 owner H s4 H4). intro. generalize (positive_st c s4 s5 H5 H H4). intro. generalize (st_rt c s4 H H5 H6). auto. intros. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4