proposition: Lemma decide_ancestor : forall x s s1 : Site, direct_son x -> ancestor x s -> indirect_son1 s1 -> (s1 = s \/ ancestor s1 s) \/ s1 <> s /\ ~ ancestor s1 s.
proof: Proof. intros. generalize H H1. elim H0. intros. case (eq_site_dec s1 s2). intro. left; left; auto. intro. case (eq_site_dec s0 s1). intro. generalize H3. rewrite e. elim H4. intros. intros. generalize H7. elim H8. intros. elim H12. auto. intro. right. split; auto. unfold not in |- *. intro. generalize (aux s0 s1 s2 H2 H3 H5). intro; elim n0; auto. intros. generalize (H3 H5 H1). intro. elim H7. intro. case (eq_site_dec s1 s3). intro. left; left; auto. intro. left; right. case (eq_site_dec s1 s0). intro. apply short. rewrite e; auto. intro. apply long with (s1 := s0). elim H8. intro; elim n0; auto. auto. auto. intro. case (eq_site_dec s1 s3). intro. left; left; auto. intro. right. split; auto. unfold not in |- *. intro. decompose [and] H8. generalize H4 H11 H10 n. elim H9. intros. elim H15. apply inc_dec_queue_equal with (q := bm c0 s5 owner). elim H12; auto. elim H13; auto. intros. cut (s0 = s5). intro. rewrite H18 in H16. elim H16; auto. apply inc_dec_queue_equal with (q := bm c0 s6 owner). elim H15; auto. elim H14; auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4