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 Z_id in |- *. unfold fun_minus in |- *. unfold fun_sum in |- *. rewrite sigma_sigma_but_owner. rewrite owner_rt_true. rewrite empty_q_to_me. simpl in |- *. simpl in |- *. rewrite add_reduce. unfold sigma_table_but_owner in |- *. apply sigma_but_pos. exact (invariant5 c H). auto. auto. Qed.
imports: DistributedReferenceCounting.machine2.alternate DistributedReferenceCounting.machine2.invariant0 DistributedReferenceCounting.machine2.invariant1 DistributedReferenceCounting.machine2.invariant2 DistributedReferenceCounting.machine2.invariant3 DistributedReferenceCounting.machine2.invariant4