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 y. right. apply (indirect_son1_intro s). auto. auto. unfold not in |- *; intros. elim y. auto. intros; left. apply (direct_son_intro s). auto. auto. auto. Qed.
imports: DistributedReferenceCounting.machine1.invariant0 DistributedReferenceCounting.machine1.invariant1 DistributedReferenceCounting.machine1.invariant2 DistributedReferenceCounting.machine1.invariant3 DistributedReferenceCounting.machine1.invariant4