%------------------------------------------------------------------------------
% vertical_cr.pvs
% ACCoRD v.1.0
% Vertical resolution algorithm
%------------------------------------------------------------------------------

vertical_cr[D,H: posreal] : THEORY
BEGIN

  IMPORTING vs_circle[D,H],
            gs_circle[D,H],
            trk_circle[D,H],
            opt_vertical[D,H]

  sp        : VAR Sp_vect3 % 3-D separation
  nvo       : VAR Vect3
  vo,vi     : VAR Nzv2_vect3
  epsh,epsv : VAR Sign

  %------------%
  % ALGORITHMS %
  %------------%

  hor_circle?(sp,vo,vi,epsh,epsv)(nvo) : bool =
    gs_vertical?(sp,vo,vi,epsh,epsv)(nvo) OR
    trk_vertical?(sp,vo,vi,epsh,epsv)(nvo) OR
    opt_vertical?(sp,vo,vi,epsh,epsv)(nvo)

  hor_circle_horizontal_only : LEMMA
    hor_circle?(sp,vo,vi,epsh,epsv)(nvo) IMPLIES
      horizontal_only?(vo)(nvo)

  vertical_cr?(sp,vo,vi,epsh,epsv)(nvo) : bool = 
    vs_circle?(sp,vo,vi,epsv)(nvo) OR
    hor_circle?(sp,vo,vi,epsh,epsv)(nvo)

  vertical_cr_meets_vertical_criterion: THEOREM
    horizontal_conflict?(sp,vo-vi) AND
    vertical_cr?(sp,vo,vi,epsh,epsv)(nvo)
    IMPLIES 
      vertical_criterion?(epsv)(sp,vo-vi)(nvo-vi)

  hor_circle_meets_horizontal_criterion: THEOREM
    horizontal_sep?(sp) AND
    hor_circle?(sp,vo,vi,epsh,epsv)(nvo)
    IMPLIES 
      horizontal_criterion?(sp,epsh)(nvo-vo)

END vertical_cr