proposition: Lemma step2 : forall (evader intruder : State) (x : nat), (distance evader intruder <= AlertRange)%R -> trkrate (bank intruder) <> 0%R -> arc_loop intruder evader (Rsqr intruderSpeed / (g * tand (bank intruder))) (trkrate (bank intruder)) x 0.
proof: Proof. Proof with trivial. intros evader intruder x H n; unfold arc_loop in |- *; rewrite mod_eq_0; case (Rlt_le_dec 0 (trkrate (bank intruder)))... cut (INR 0 = 0%R)... intros; rewrite H0; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; cut (mkState (xt intruder + Rsqr intruderSpeed / (g * tand (bank intruder)) * (sind (heading intruder) - sind (heading intruder))) (yt intruder + Rsqr intruderSpeed / (g * tand (bank intruder)) * (cosd (heading intruder) - cosd (heading intruder))) (heading intruder) (bank intruder) = intruder)... cut (mkState (xt evader) (yt evader) (heading evader) (bank evader) = evader)... intros; rewrite H1; rewrite H2; unfold chktrack in |- *; case (Rle_dec (tau intruder evader 0) 0); intro... unfold chkrange in |- *; split... unfold RR in |- *; unfold dx, dy in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rplus_0_r; unfold distance in H... unfold AlertTime in |- *; left; prove_sup... rewrite Rplus_0_l; case (Rlt_dec AlertTime (tau intruder evader 0)); intro... cut (0 <= AlertTime)%R... intro; assert (H4 := asymptotic_decrease_tau intruder evader 0 0 AlertTime (Rlt_le _ _ r0) H3); repeat rewrite Rplus_0_l in H4; apply Rle_trans with (RR intruder evader 0)... unfold RR in |- *; unfold dx, dy in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rplus_0_r... unfold AlertTime in |- *; left; prove_sup... assert (H3 := derivative_eq_zero_min intruder evader 0 0); repeat rewrite Rplus_0_l in H3; apply Rle_trans with (RR intruder evader 0)... unfold RR in |- *; unfold dx, dy in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rplus_0_r... unfold xt, yt in |- *; case evader... unfold xt, yt in |- *; case intruder; intros; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r... cut (INR 0 = 0%R)... intros; rewrite H0; repeat rewrite Rmult_0_l; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r; cut (mkState (xt intruder + Rsqr intruderSpeed / (g * tand (bank intruder)) * (sind (heading intruder) - sind (heading intruder))) (yt intruder + Rsqr intruderSpeed / (g * tand (bank intruder)) * (cosd (heading intruder) - cosd (heading intruder))) (heading intruder) (bank intruder) = intruder)... cut (mkState (xt evader) (yt evader) (heading evader) (bank evader) = evader)... intros; rewrite H1; rewrite H2; unfold chktrack in |- *; case (Rle_dec (tau intruder evader 0) 0); intro... unfold chkrange in |- *; split... unfold RR in |- *; unfold dx, dy in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rplus_0_r; unfold distance in H... unfold AlertTime in |- *; left; prove_sup... rewrite Rplus_0_l; case (Rlt_dec AlertTime (tau intruder evader 0)); intro... cut (0 <= AlertTime)%R... intro; assert (H4 := asymptotic_decrease_tau intruder evader 0 0 AlertTime (Rlt_le _ _ r0) H3); repeat rewrite Rplus_0_l in H4; apply Rle_trans with (RR intruder evader 0)... unfold RR in |- *; unfold dx, dy in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rplus_0_r... unfold AlertTime in |- *; left; prove_sup... assert (H3 := derivative_eq_zero_min intruder evader 0 0); repeat rewrite Rplus_0_l in H3; apply Rle_trans with (RR intruder evader 0)... unfold RR in |- *; unfold dx, dy in |- *; repeat rewrite Rmult_0_l; repeat rewrite Rplus_0_r... unfold xt, yt in |- *; case evader... unfold xt, yt in |- *; case intruder; intros; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; repeat rewrite Rmult_0_r; repeat rewrite Rplus_0_r... Qed.
imports: Reals trajectory_const constants ails_def tau Omega