middle_third_overlap.pvs

%
% Purpose      : Provide overlap results for tau(E) = floor(|E|/3)
%
middle_third_overlap[N: posnat, T: TYPE+, <=: (total_order?[T])]: THEORY

  BEGIN
  
  IMPORTING
    reduce_properties[N, T, <=],
    middle_third_pigeonhole[N]


  src_set: var finite_set[below(N)] % subsets of indices
  e1, e2 : var non_empty_finite_set[below(N)]
  v1, v2  : var [below(N) -> T]

  k: var below(N)

  middle_third_overlap: LEMMA
       byzantine_intersection_majority?(e1, e2, src_set)
    IMPLIES
      EXISTS k: 
        src_set(k) AND
        e1(k) AND 
        e2(k) AND 
        min(reduce(byz)(v1, e1)) <= v1(k) AND 
        v2(k) <= max(reduce(byz)(v2, e2))

  END middle_third_overlap