%
% Divergence
% 

divergence[D:posreal] : THEORY
BEGIN

  IMPORTING horizontal,
       predicate_coordination_2D

  s       : VAR Vect2
  v,vo,vi,
  nv,nw   : VAR Vect2
  nvo,nvi : VAR Vect2
  eps   : VAR Sign


  divergence_crit?: Criterion_2D = (LAMBDA (s,v,eps): (LAMBDA (nv): s*nv > 0))

  divergence_pred?: Vector_Predicate_2D = (LAMBDA (s,v): (LAMBDA (nv): NOT divergent?(s,nv)))

  divergence_crit_oriented: LEMMA symmetric_oriented_2D?(divergence_crit?)

  divergence_crit_sum_indep: LEMMA sum_independent_2D?(divergence_crit?, divergence_pred?)

  divergence_pred_sum_closed: LEMMA sum_closed_2D?(divergence_pred?)

  divergence_crit_coordinated: LEMMA coordinated_oriented_2D?(divergence_crit?,divergence_pred?)

  divergence_crit_coordinated2: LEMMA
        NOT divergent?(s, zero, vo - vi, zero) AND
        divergence_crit?(s, vo - vi, eps)(nvo - vi) AND
        divergence_crit?(-s, vi - vo, eps)(nvi - vo)
        IMPLIES
 divergent?(s, zero, nvo - nvi, zero)





END divergence