|
%
% 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
