proposition: Lemma decide_parent : forall s1 s3 : Site, {parent s1 s3} + {~ parent s1 s3}.
proof: Proof. intros. elim (decide_rt s3). intro y. right. unfold not in |- *. intro. generalize y. elim H. intros. rewrite H0 in y0. discriminate. intro. elim (decide_inc_dec_in_queue s3). intros y0. elim y0. intros x y1. case (eq_site_dec x s1). intro. left. apply parent_intro. auto. rewrite <- e. auto. intro. right. unfold not in |- *. intro. generalize y1; generalize n. elim H. intros. elim n0. apply inc_dec_queue_equal with (q := bm c0 s2 owner). auto. auto. intros y0. right. unfold not in |- *. intro. generalize y0. elim H. intros. generalize (y1 s0). intro. elim H2; auto. Qed.
imports: DistributedReferenceCounting.machine1.invariant0 DistributedReferenceCounting.machine1.invariant1 DistributedReferenceCounting.machine1.invariant2 DistributedReferenceCounting.machine1.invariant3 DistributedReferenceCounting.machine1.invariant4