SSL omega_v2.pvs

omega_v2[D:posreal,B:nnreal,T: {AB: posreal|AB>B}] : THEORY
BEGIN

  IMPORTING omega_2D[D,B,T], 
            analysis@continuity_of_max_min, 
            analysis@metric_space_real_fun
             
  s,v  : VAR Vect2


  % The Definition Of omega_v2

  omega_v2(s)(v): real =
    IF on_D?(s) AND B = 0 THEN s*v
    ELSE omega_2D(s)(v) ENDIF

  omega_v2_generic: LEMMA 
    NOT (on_D?(s) AND B = 0) IMPLIES 
    omega_v2(s)(v) = omega_2D(s)(v)

  % Characterizes Conflict

  omega_v2_conflict: LEMMA 
    omega_v2(s)(v) < 0 IFF conflict_2D?(s,v)

  omega_v2_2D_eq_0: LEMMA omega_v2(s)(v) = 0
    IMPLIES omega_2D(s)(v) = 0

  omega_v2_critical_points: LEMMA 
    omega_v2(s)(v) = 0 IMPLIES horizontal_sep?(s) AND line_solution?(s,v) OR
                               circle_solution_2D?(s,v,T,Entry) OR
          (B>0 AND circle_solution_2D?(s,v,B,Exit))

  % Continuity

  omega_v2_continuous: LEMMA 
    continuous?(omega_v2(s))

END omega_v2