proposition: Theorem ails_correctness : forall (intr : Trajectory) (evad : EvaderTrajectory) (T : TimeT), h intr = V -> h (tr evad) = V -> conflict intr evad T = true -> ails_alert (measure2state intr 0) (measure2state (tr evad) 0).
proof: Proof. Proof with trivial. intros; case (Rle_dec (d intr evad) AlertRange); intro; [ apply (ails_alarm_at_alerting_distance _ _ r) | cut (AlertRange < d intr evad)%R; [ intro; apply (ails_alarm_when_conflict intr evad T) | auto with real ] ]... Qed.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory alarm alpha_no_conflict