proposition: Lemma le_dt_time : forall (c0 : Config) (s0 : Site), legal c0 -> dt c0 s0 <= time c0.
proof: Proof. intros; elim H. apply init_le_dt_time. simple induction t; unfold transition in |- *; intros. apply copy_trans_le_dt_time; trivial. apply rdec_trans_le_dt_time; trivial. apply rinc_trans_le_dt_time; trivial. apply rcop1_trans_le_dt_time; trivial. apply rcop2_trans_le_dt_time; trivial. apply rcop3_trans_le_dt_time; trivial. apply del_trans_le_dt_time; trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc