x, y, z : var int
nat_set: TYPE = {N: finite_set[int] | FORALL (x:int): N(x) => x >= 0}
negint_set: TYPE = {N : finite_set[int] |FORALL (x:int): N(x) => x < 0}
A, B, C,
S, S1, S2: VAR nat_set
X, Y, Z: VAR finite_set[int]
A_bar: VAR negint_set
disjoint1: LEMMA
disjoint?(A, A_bar)
disjoint2: LEMMA
disjoint?(A_bar, A)
complement(z): int = 0 - (1 + z)
complement_complement: LEMMA
complement(complement(z)) = z
two_thirds_overlap_lem: LEMMA
two_thirds_majority_subset?(A, S1) AND
two_thirds_majority_subset?(split(B, C), split(S2, C)) AND
intersection_majority?(S1, split(S2, C)) IMPLIES EXISTS x: A(x) AND B(x) AND C(x)
fta_overlap_pigeonhole: LEMMA
two_thirds_majority_subset?(A, S1) AND
two_thirds_majority_subset?(B, S2) AND
byzantine_intersection_majority?(S1, S2, C) IMPLIES EXISTS x: A(x) AND B(x) AND C(x)
END pigeonhole_int
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
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.
