Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: pigeonhole_int.prf Sprache: PVS

Original von: 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.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.