proposition: Theorem ails_alarm_tau_gt0 : 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 -> (0 < tau (measure2state intr 0) (measure2state (tr evad) 0) 0)%R -> conflict intr evad T = true -> ails_alert (measure2state intr 0) (measure2state (tr evad) 0).
proof: Proof. Proof with trivial. intros intr evad T hyp_intr hyp_evad; intros; unfold ails_alert in |- *; case (Req_EM_var (trkrate (bank (measure2state intr 0))) 0); intro... apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... case (Rle_dec 3 (trkrate (bank (measure2state intr 0)))); intro... unfold arc_loop in |- *; rewrite mod_eq_0... case (Rlt_le_dec 0 (trkrate (bank (measure2state intr 0)))); intro... unfold INR in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; unfold intruderSpeed in |- *; replace (v V) with 250%R... cut (let z := 250%R in mkState (xt (measure2state intr 0) + Rsqr z / (g * tand (bank (measure2state intr 0))) * (sind (heading (measure2state intr 0)) - sind (heading (measure2state intr 0)))) (yt (measure2state intr 0) + Rsqr z / (g * tand (bank (measure2state intr 0))) * (cosd (heading (measure2state intr 0)) - cosd (heading (measure2state intr 0)))) (heading (measure2state intr 0)) (bank (measure2state intr 0)) = measure2state intr 0)... intro; rewrite H4... cut (mkState (xt (measure2state (tr evad) 0)) (yt (measure2state (tr evad) 0)) (heading (measure2state (tr evad) 0)) (bank (measure2state (tr evad) 0)) = measure2state (tr evad) 0)... intro; rewrite H5... apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... unfold Rminus in |- *; repeat rewrite Rplus_opp_r; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r... unfold INR in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... case (Rle_dec (3 / 2) (trkrate (bank (measure2state intr 0)))); intro... unfold arc_loop in |- *; rewrite mod_eq_0; case (Rlt_le_dec 0 (trkrate (bank (measure2state intr 0)))); intro... repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... case (Rle_dec (3 / 4) (trkrate (bank (measure2state intr 0)))); intro... unfold arc_loop in |- *; rewrite mod_eq_0; case (Rlt_le_dec 0 (trkrate (bank (measure2state intr 0)))); intro... repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... unfold arc_loop in |- *; rewrite mod_eq_0; case (Rlt_le_dec 0 (trkrate (bank (measure2state intr 0)))); intro... repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; unfold Rdiv in |- *; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; apply (chktrack_NOT_Omega_trkrate_eq_0 intr evad T)... Qed.
imports: Bool Reals trajectory_const trajectory_def constants ycngftys ycngstys ails_def math_prop tau ails trajectory measure2state ails_trajectory