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

cd_sphere  : THEORY 
BEGIN

  IMPORTING reals@sign,
            reals@quadratic_2b,
     reals@quad_minmax,
            vectors@vectors_3D

  s,v   : VAR Vect3
  D : VAR posreal     


  conflict_sphere_ever(D,s,v) : bool =
    EXISTS (t:nnreal): norm(s+t*v)<D

  cd_sphere(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

  cd_sphere_def: LEMMA cd_sphere(D,s,v) IFF conflict_sphere_ever(D,s,v)



END cd_sphere