| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle pigeonhole_int.pvs Sprache: PVS |
|||||||||
|
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.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28