|
%
%
% Purpose : core "majority" results, including a majority choice
% function, validity and agreement properties
%
%
majority_properties[N: posnat, T:TYPE+]: THEORY
BEGIN
IMPORTING
finite_seqs[T],
finite_sets@finite_sets_card_eq,
pigeonhole[below(N)],
node[N, T]
v, v1, v2: VAR vec
e, node_set: VAR nodeid_set
d, t: VAR T
mf: VAR majority_function
majority(mf)(v, e): T = mf(vec2seq(v, e))
majority_exists?(v, e): bool = maj_exists(vec2seq(v, e))
majority_value_set(e, v)(t) : bool =
2 * card(uniform_nodes(e, v, t)) > card(e)
is_majority: LEMMA majority_value_set(e, v)(t) IFF is_majority(t, vec2seq(v, e))
majority_value_subset: LEMMA
majority_value_set(e, v)(t)
IFF
majority_subset?(uniform_nodes(e, v, t), e)
uniform_majority: LEMMA
majority_subset?(node_set, e) AND
uniform?(v, t)(node_set)
IMPLIES
majority_value_set(e, v)(t)
majority_validity: LEMMA
majority_value_set(e, v)(t)
IMPLIES
majority(mf)(v, e) = t
agreement_generation: THEOREM
enabled_symmetric?(e, v1, v2)
IMPLIES
majority(mf)(v1, e) = majority(mf)(v2, e)
END majority_properties
¤ Dauer der Verarbeitung: 0.13 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.
|
