proposition: Lemma decide_direct_son : forall s1 : Site, s1 <> owner -> {direct_son s1} + {~ direct_son s1}.
proof: Proof. intros. elim (decide_rt s1). intros. right. unfold not in |- *. intro. generalize a. elim H0. intros. rewrite H2 in a0. discriminate. intro. elim (decide_inc_dec_in_queue s1). intro. right. unfold not in |- *. intro. generalize a. elim H0. intros. elim a0. auto. intro. left. apply direct_son_intro. auto. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4