proposition: Lemma safety1 : forall c : Config, legal c -> forall s : Site, s <> owner -> rt c s = true -> (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 |- *. unfold Z_id in |- *. unfold fun_minus in |- *. unfold fun_sum in |- *. elim (direct_or_indirect_son1 c s H0 H1); intro. apply sigma_strictly_positive with (x := s). exact eq_site_dec. apply in_s_LS. intro; apply invariant5; auto. apply direct_son_is_positive; auto. elim (parent_invariant c H s b). intros. decompose [and] H2. apply sigma_strictly_positive with (x := x). exact eq_site_dec. apply in_s_LS. intro; apply invariant5; auto. apply direct_son_is_positive; auto. Qed.
imports: DistributedReferenceCounting.machine1.invariant5 DistributedReferenceCounting.machine1.invariant7