SSL middle_third_pigeonhole.pvs
Interaktion und PortierbarkeitPVS
middle_third_pigeonhole[N: posnat]: THEORY
BEGIN
IMPORTING
pigeonhole_int, pigeonhole[below(N)]
A, B, C, S1, S2: VAR finite_set[below(N)]
x: VAR below(N)
middle_third_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 middle_third_pigeonhole
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.2Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
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.