proposition: Lemma alarm_NOT_Omega_AlertTime : 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 -> (AlertTime < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R -> (RR (measure2state intr 0) (measure2state (tr evad) 0) AlertTime <= AlertRange)%R.
proof: Proof. Proof with trivial. intros intr evad T hyp_intr hyp_evad; intros; apply Rle_trans with (RR (measure2state intr 0) (measure2state (tr evad) 0) T)... rewrite <- (Rplus_0_l AlertTime); rewrite <- (Rplus_0_l T); apply asymptotic_decrease_tau... left... unfold AlertTime in |- *; apply Rle_trans with MaxT... apply (cond_2 T)... unfold MaxT in |- *; left; prove_sup... apply (alarm_NOT_Omega_T _ _ _ hyp_intr hyp_evad H H0 H1 H2)... Qed.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory