proposition: Lemma positive_st : forall (c : Config) (s0 s5 : Site), s0 <> owner -> legal c -> In_queue Message (inc_dec s0) (bm c s5 owner) -> (st c s0 > 0)%Z.
proof: Proof. intros c s0 s5 H HA. rewrite invariant2. unfold sigma_rooted in |- *. intros. apply sigma2_strictly_positive with (x := s5) (y := owner). auto. exact eq_site_dec. apply in_s_LS. apply in_s_LS. intros. unfold rooted in |- *. intros. simpl in |- *. intros. simpl in |- *. apply reduce_positive_or_null. intro. apply rooted_fun_positive_or_null. generalize H0. elim (bm c s5 owner). simpl in |- *; intuition. intros. generalize H2. case d. simpl in |- *. intros. elim H3. intro; discriminate. intro. generalize (H1 H4). intro. case (eq_site_dec owner s0). intros; omega. intros; omega. simpl in |- *. intros. case (eq_site_dec s s0). intro. case (eq_site_dec owner owner). intro. generalize (rooted_positive_or_null s0 s5 owner q). intro. omega. intro. elim n; auto. intro. elim H3. intro; elim n. inversion H4. auto. intro. generalize (H1 H4). intro. omega. simpl in |- *. intro. elim H3. intro; discriminate. intro. generalize (H1 H4). intro. case (eq_site_dec s5 s0). intro; omega. intro; omega. auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.machine DistributedReferenceCounting.machine2.cardinal DistributedReferenceCounting.machine2.comm