Quelle  horizontal_cr.pvs

%------------------------------------------------------------------------------
% horizontal_cr.pvs
% ACCoRD v.1.0
% Horizontal resolution algorithms
%------------------------------------------------------------------------------

horizontal_cr[D:posreal] : THEORY

BEGIN

  IMPORTING gs_line[D], 
            trk_line[D], 
            opt_line[D]

  sp      : VAR Sp_vect2
  vo,vi,
  nvo     : VAR Vect2
  eps     : VAR Sign

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

  horizontal_cr?(sp,vo,vi,eps)(nvo) : bool =
    gs_line_eps?(sp,vo,vi,eps)(nvo) OR
    trk_line_eps?(sp,vo,vi,eps)(nvo) OR
    opt_line_eps?(sp,vo,vi,eps)(nvo) 

  %--------------------------%
  % LEMMAS                   %
  %--------------------------%

  horizontal_cr_is_line_solution: THEOREM
    horizontal_cr?(sp,vo,vi,eps)(nvo)
    IMPLIES 
      line_solution?(sp,nvo-vi,eps)

END horizontal_cr