proposition: Lemma st_rt : forall s0 : Site, s0 <> owner -> (st c0 s0 > 0)%Z -> rt c0 s0 = true.
proof: Proof. elim Hlegal. intros; apply st_rt_init; trivial. simple induction t; unfold transition in |- *; intros. apply copy_trans_st_rt; auto. apply rdec_trans_st_rt; auto. apply rinc_trans_st_rt; auto. apply rcop1_trans_st_rt; auto. apply rcop2_trans_st_rt; auto. apply rcop3_trans_st_rt; auto. apply del_trans_st_rt; auto. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc