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