%------------------------------------------------------------------------------
% horizontal_los_criterion.pvs
%
%------------------------------------------------------------------------------

horizontal_los_criterion : THEORY
BEGIN

  IMPORTING repulsive

  s,
  vo,vi,
  nvo,nvi : VAR Nz_vect2
  eps : VAR Sign

  horizontal_los_criterion(s, vo, vi, nvo, eps): MACRO bool = repulsive_criteria(s,vo-vi,eps)(nvo-vi)

  horizontal_los_criterion_repulsive: LEMMA
    horizontal_los_criterion(s,vo,vi,nvo,eps)
    IMPLIES
    repulsive?(s,vo-vi)(nvo-vi)

  horizontal_los_criterion_coordinately_repulsive: LEMMA
    horizontal_los_criterion(s,vo,vi,nvo,eps) AND
    horizontal_los_criterion(-s,vi,vo,nvi,eps)
    IMPLIES
    repulsive?(s,vo-vi)(nvo-nvi)
      
END horizontal_los_criterion