proposition: Lemma direct_son_is_positive : forall c : Config, legal c -> forall s : Site, direct_son c s -> (Int (rt c s) + reduce Message dec_count (bm c s owner) + reduce Message copy_count (bm c owner s) - reduce Message new_inc_count (bm c s owner) > 0)%Z.
proof: Proof. intros. elim H0. intros. rewrite H2; unfold Int in |- *. generalize (not_inc_dec_in (bm c s0 owner) H3); intro. generalize (copy_count_is_positive (bm c owner s0)). intro. generalize (dec_count_is_positive (bm c s0 owner)); intro. cut (reduce Message new_inc_count (bm c s0 owner) = 0%Z). intro. omega. generalize H4. elim (bm c s0 owner). simpl in |- *; auto. intro. case d. simpl in |- *. intros. rewrite H7. auto. intro. generalize (H8 s1). intuition. intros. elim (H8 s1); simpl in |- *. left; auto. simpl in |- *; intros. rewrite H7. omega. intro. generalize (H8 s1). intuition. Qed.
imports: DistributedReferenceCounting.machine2.invariant5 DistributedReferenceCounting.machine2.invariant7