Quelle pigeonhole.pvs Sprache: PVS

%
%
% Purpose : the pigeonhole principle
%
%

pigeonhole[T: TYPE]: THEORY

BEGIN

  A, A1, A2, B, C, S, S1, S2, S3: VAR finite_set[T]
  x: VAR T
  n: VAR nat

  pigeonhole: THEOREM
      card(A) + card(B) > card(union(A, B))
    IMPLIES
      EXISTS x: A(x) AND B(x)

  card_difference_alt: LEMMA
    card(difference(S, C)) <= n IFF card(intersection(S, C)) >= card(S) - n

  pigeonhole_difference: THEOREM
      subset?(A, S) AND
      card(A) > n AND
      card(difference(S, B)) <= n
    IMPLIES
      EXISTS x: A(x) AND B(x)

  majority_subset?(A, S): bool =
    2 * card(A) > card(S) AND subset?(A, S)

  simple_majority?(A, S): bool =
    2 * card(intersection(A, S)) > card(S)

  simple_majority_subset: LEMMA
    simple_majority?(A, S) IFF majority_subset?(intersection(A, S), S)

  majority_subset_nonempty: LEMMA
      majority_subset?(A, S)
    IMPLIES
      NOT empty?(S)

  simple_majority_nonempty: LEMMA
      simple_majority?(A, S)
    IMPLIES
      NOT empty?(S)

  majority_nonempty: LEMMA
      majority_subset?(A, S)
    IMPLIES
      NOT empty?(A)

  majority_pigeonhole: THEOREM
      2 * card(A) > card(S) AND
      subset?(A, S) AND
      2 * card(B) >= card(S) AND
      subset?(B, S)
    IMPLIES
      EXISTS x: A(x) AND B(x)

  simple_majority_pigeonhole: THEOREM
      simple_majority?(A, S) AND
      simple_majority?(B, S)
    IMPLIES
      EXISTS x: A(x) AND B(x)

  median_pigeonhole: LEMMA
      majority_subset?(A, S1) AND
      majority_subset?(B, S2) AND
      card(union(S1, S2)) - card(intersection(S1, S2)) <= 1
    IMPLIES
      EXISTS x: A(x) AND B(x)

  two_thirds_majority_subset?(A, S): bool =
    3 * card(A) >= 2 * card(S) AND
    subset?(A, S)

  intersection_majority?(S1, S2): bool =
    2 * card(intersection(S1, S2)) > card(union(S1, S2))

  intersection_nonempty: LEMMA
     intersection_majority?(S1, S2) IMPLIES not empty?(S1)

  intersection_majority?(S1, S2, S3): bool =
    2 * card(intersection(S1, S2)) > card(S3)

  byzantine_intersection_majority?(S1, S2, S3): bool =
    2 * card(intersection(S1, intersection(S2, S3))) >
      card(union(S1, S2)) + card(difference(S2, S3))

  two_thirds_overlap_pigeonhole: LEMMA
      two_thirds_majority_subset?(A, S1) AND
      two_thirds_majority_subset?(B, S2) AND
      intersection_majority?(S1, S2)
    IMPLIES
      EXISTS x: A(x) AND B(x)

  IMPORTING tau_declaration

  t: VAR tau_type
  e: VAR non_empty_finite_set[T]
  s, s1, s2: VAR finite_set[T]

  quorum?(s1, t)(s2): bool =
    NOT empty?(s1) AND card(difference(s1, s2)) <= t(card(s1))

  quorum_exists?(s, t): bool =
    EXISTS s1: quorum?(s, t)(s1)

  % Cardinality of a tau-reduced multi-set
  M(e, t): posnat = card(e) - 2 * t(card(e))

  nada_reduce: LEMMA M(e, nada) = card(e)
  mid_reduce: LEMMA M(e, mid) <= 2
  byz_reduce: LEMMA M(e, byz) >= card(e)/3



END pigeonhole

quality96%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.