proposition: Lemma aux : forall s0 s1 s2 : Site, parent s0 s2 -> direct_son s0 -> ancestor s1 s2 -> s1 = s0.
proof: Proof. intros. generalize H H0. elim H1. intros. apply inc_dec_queue_equal with (q := bm c0 s4 owner). elim H2; auto. elim H3; auto. intros. cut (s0 = s4). intro. rewrite <- H7 in H2. generalize H2. elim H6. intros. generalize H10. elim H11. intros. generalize H13. elim H12. intros. elim (H16 s8). auto. intros. generalize H15. elim H14. intros. elim (H18 s9). auto. apply inc_dec_queue_equal with (q := bm c0 s5 owner). elim H5; auto. elim H4; auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4