proposition: Lemma chktrack_NOT_Omega_trkrate_eq_0 : forall (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT), h intr = V -> h (tr evad) = V -> (MinDistance T <= l intr evad T)%R -> (l intr evad T <= MaxDistance T)%R -> Omega (beta intr evad T + thetat intr 0) = false -> conflict intr evad T = true -> (0 < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R -> chktrack (measure2state intr 0) (measure2state (tr evad) 0) 0.
proof: Proof. Proof with trivial. intros intr evad T hyp_intr hyp_evad; intros; unfold chktrack in |- *; case (Rle_dec (tau (measure2state intr 0) (measure2state (tr evad) 0) 0) 0); intro... elim (Rlt_irrefl 0 (Rlt_le_trans 0 (tau (measure2state intr 0) (measure2state (tr evad) 0) 0) 0 H3 r))... rewrite Rplus_0_l; case (Rlt_dec AlertTime (tau (measure2state intr 0) (measure2state (tr evad) 0) 0)); intro... apply (alarm_NOT_Omega_AlertTime intr evad T)... apply (alarm_NOT_Omega_tau intr evad T)... Qed.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory