%------------------------------------------------------------------------------
% vz_criteria.pvs
% ACCoRD v1.0
%
% This theory proposes a criterion for vertical separation for non-negative
% times. 
%------------------------------------------------------------------------------

vz_criteria[H: posreal]: THEORY
BEGIN

  IMPORTING vertical[H]

  spz       : VAR Spz
  sz,vz,nvz,
  voiz,vioz,
  t         : VAR real
  nnt       : VAR nnreal
  dir       : VAR Sign

  %%
  %% Assumption: abs(sz) >= H

  vertical_exit_criterion?(spz,vz) : bool =
    vertical_exit?(spz,vz)

  vertical_exit_independence: THEOREM
    vertical_exit_criterion?(spz,vz) IFF NOT vertical_conflict?(spz,vz)

  vertical_exit_coordination: THEOREM
    vertical_conflict?(spz,vz) AND
    vertical_exit_criterion?(spz,voiz) AND
    vertical_exit_criterion?(-spz,vioz) 
    IMPLIES
      vertical_exit_criterion?(spz,voiz-vioz-vz)

  %% The following lemma assumes vertical separation at a given time in the
  %% future and gives sufficient conditions over a new vertical velocity 
  %% that also yields vertical separation at that time.

  vertical_sep_dir_at : LEMMA
    LET signsz = sign(sz+nnt*vz) IN
    vertical_sep?(sz+nnt*vz) AND
    vertical_dir?(sz+nnt*vz,vz,dir) AND
    (dir = Entry IMPLIES signsz*nvz <= 0) AND
    signsz*nvz >= signsz*vz 
    IMPLIES
      vertical_sep?(sz+nnt*nvz) AND
      vertical_dir?(sz+nnt*nvz,nvz,dir)

END vz_criteria