|
%
% Purpose : Provide overlap results for tau = |E| - floor(N'/2) - 1
%
weber_overlap[N: posnat, T: TYPE+, <=: (total_order?[T])]: THEORY
BEGIN
IMPORTING
reduce_properties[N, T, <=]
src_set: VAR finite_set[below(N)]
e, e1, e2 : var non_empty_finite_set[below(N)]
v1, v2 : var [below(N) -> T]
k: var below(N)
tau(src_set): tau_type = weber(card(src_set))
weber_overlap: LEMMA
subset?(e1, src_set) AND
subset?(e2, src_set) AND
intersection_majority?(e1, e2, src_set)
IMPLIES
EXISTS k:
src_set(k) AND
e1(k) AND
e2(k) AND
min(reduce(tau(src_set))(v1, e1)) <= v1(k) AND
v2(k) <= max(reduce(tau(src_set))(v2, e2))
END weber_overlap
¤ Dauer der Verarbeitung: 0.23 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.
|
