proposition: Lemma alarm_NOT_Omega_T : 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 -> (RR (measure2state intr 0) (measure2state (tr evad) 0) T <= AlertRange)%R.
proof: Proof. Proof with trivial. intros intr evad T hyp_intr hyp_evad; intros; apply Rsqr_incr_0_var... rewrite R_T... generalize (conflict_beta_theta intr evad T hyp_intr H H0 H1 H2); intro; elim H3; intro... cut (0 <= beta intr evad T + thetat intr 0)%R... intro; apply (Math_prop_alarm_1 (beta intr evad T + thetat intr 0) (l intr evad T) T H H0 H5 H4)... generalize (beta_def intr evad T); intro; decompose [and] H5; intros... cut (beta intr evad T + thetat intr 0 <= 2 * PI)%R... intro; apply (Math_prop_alarm_2 (beta intr evad T + thetat intr 0) (l intr evad T) T H H0 (Rlt_le (2 * PI - MinBeta) (beta intr evad T + thetat intr 0) H4))... generalize (beta_def intr evad T); intro; decompose [and] H5; intros; left... left; apply AlertRange_pos... Qed.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory