proposition: Lemma owner_st_positive : forall c : Config, legal c -> (st c owner >= 0)%Z.
proof: Proof. intros. rewrite (invariant4 c H). rewrite other_definition_for_sigma_receive_table. rewrite <- sigma_same_table. rewrite <- sigma_same_table. rewrite <- sigma_same_table2. unfold sigma_table in |- *. apply sigma_pos. unfold Z_id in |- *. unfold fun_minus in |- *. unfold fun_sum in |- *. exact (invariant5 c H). Qed.
imports: DistributedReferenceCounting.machine1.alternate DistributedReferenceCounting.machine1.invariant0 DistributedReferenceCounting.machine1.invariant1 DistributedReferenceCounting.machine1.invariant2 DistributedReferenceCounting.machine1.invariant3 DistributedReferenceCounting.machine1.invariant4