%------------------------------------------------------------------------------
% cd2d_ever
%
% Correctness and completeness of 3-D conflict (ever) detection algorithm for
% a spherical protection zone.
%------------------------------------------------------------------------------

cd2d_ever  : THEORY 
BEGIN

  IMPORTING reals@sign,
            reals@quadratic_2b,
     reals@quad_minmax,
     vectors@vectors_2D,
     horizontal

  s,v   : VAR Vect2
  D : VAR posreal  

  cd2d_ever(D,s,v): bool =
    IF   s*v < 0 THEN (sq(s*v)-sqv(v)*(sqv(s)-sq(D)) > 0)
    ELSE (sqv(s) < sq(D))
    ENDIF

  cd2d_ever_def: LEMMA 
    cd2d_ever(D,s,v) IFF horizontal_conflict?[D](s,v)

END cd2d_ever