proposition: Lemma ancestor_has_positive_st : forall c : Config, legal c -> forall s1 s2 : Site, ancestor c s1 s2 -> (st c s1 > 0)%Z.
proof: Proof. intros. elim H0. intros. elim H1. intros. generalize (inc_dec_in s4 (bm c s5 owner) H3). intro. apply positive_st with (s5 := s5). apply not_owner_inc3 with (s1 := s5) (s2 := owner) (c := c). auto. auto. auto. auto. intros; auto. Qed.
imports: DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4