delay_3D[D,H:posreal]  : THEORY 

% Shows that if the max delay will result in a conflict free maneuver
% with a given new velocity, then any turn off to that velocity before
% then will also be conflict free.

BEGIN

  IMPORTING cd3d

  nnt: VAR posreal % conflict time
  rt : VAR posreal % future resolution time


  s,v,nv,so,si,vo,vi,nvo,nvi: VAR Vect3


  delay_conflict_free_rel: LEMMA
    nnt <= rt AND
    conflict?[D,H](s,v) AND
    (NOT conflict_3D?[D,H,0,rt](s,v)) AND
    (NOT conflict?[D,H](s + rt*v,nv))
    IMPLIES
    (NOT conflict_3D?[D,H,0,nnt](s,v))
    AND
    (NOT conflict?[D,H](s+nnt*v,nv))

  delay_conflict_free: LEMMA
    nnt <= rt AND
    conflict?[D,H](so-si,vo-vi) AND
    (NOT conflict_3D?[D,H,0,rt](so-si,vo-vi)) AND
    (NOT conflict?[D,H]((so+rt*vo)-(si+rt*vi),nvo-vi))
    IMPLIES
    (NOT conflict_3D?[D,H,0,nnt](so-si,vo-vi))
    AND
    (NOT conflict?[D,H]((so+nnt*vo)-(si+nnt*vi),nvo-vi))


END delay_3D