proposition: Lemma null_st : forall (c0 : Config) (s0 : Site), legal c0 -> s0 <> owner -> no_message c0 -> st c0 s0 = 0%Z.
proof: Proof. intros. rewrite invariant2. unfold sigma_rooted in |- *. unfold sigma2_table in |- *. unfold sigma_table in |- *. unfold Z_id in |- *. apply sigma_f_null. intros. apply sigma_f_null. intros. generalize H1; unfold no_message in |- *. intro. rewrite H2. simpl in |- *. auto. apply in_s_LS. apply in_s_LS. auto. auto. Qed.
imports: List DistributedReferenceCounting.machine2.invariant8