fact: Definition arc_loop (intruder evader : State) (arcrad trkrate : R) (idtrk iarc : nat) : Prop := match iarc with | S p => False | O => let tpred := (INR iarc * tstep)%R in let xloc := (xt evader + v evaderSpeed * tpred)%R in let yloc := yt evader in let xtrk := match Rlt_le_dec 0 trkrate with | left _ => (xt intruder + arcrad * (sind (heading intruder + trkrate * tpred) - sind (heading intruder)))%R | right _ => (xt intruder + arcrad * (sind (heading intruder) - sind (heading intruder) + trkrate * tpred))%R end in let ytrk := match Rlt_le_dec 0 trkrate with | left _ => (yt intruder + arcrad * (cosd (heading intruder) - cosd (heading intruder + trkrate * tpred)))%R | right _ => (yt intruder + arcrad * (cosd (heading intruder + trkrate * tpred) - cosd (heading intruder)))%R end in match mod_ iarc idtrk with | O => let tantrk := (heading intruder + tpred * trkrate)%R in let int := mkState xtrk ytrk tantrk (bank intruder) in let eva := mkState xloc yloc (heading evader) (bank evader) in chktrack int eva tpred | _ => let range := sqrt (Rsqr (xtrk - xloc) + Rsqr (ytrk - yloc)) in chkrange range tpred end end.
imports: Reals trajectory_const constants ails_def tau Omega