|
pigeonhole_int: THEORY
BEGIN
IMPORTING
pigeonhole[int]
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
mirror(X): finite_set[int] = image(complement)(X)
mirror_mirror: LEMMA
mirror(mirror(X)) = X
card_mirror: LEMMA
card(mirror(X)) = card(X)
subset_mirror: LEMMA
subset?(X, Y)
IMPLIES
subset?(mirror(X), mirror(Y))
mirror_nat: JUDGEMENT mirror(A) HAS_TYPE negint_set
mirror_negint: JUDGEMENT mirror(A_bar) HAS_TYPE nat_set
split(X, Y): finite_set[int] =
union(intersection(X, Y), mirror(difference(X, Y)))
subset_split: LEMMA
subset?(X, Y)
IMPLIES
subset?(split(X, Z), split(Y, Z))
card_split: LEMMA
card(split(A, C)) = card(A)
two_thirds_split: LEMMA
two_thirds_majority_subset?(A, S)
IMPLIES
two_thirds_majority_subset?(split(A, C), split(S, C))
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.18 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
