proposition: Lemma direct_or_indirect_son1 : forall s : Site, s <> owner -> rt c0 s = true -> {direct_son s} + {indirect_son1 s}.
proof: Proof. intros. elim (decide_inc_dec_in_queue s). intro. right. apply (indirect_son1_intro s). auto. auto. unfold not in |- *; intros. elim a. auto. intros; left. apply (direct_son_intro s). auto. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4