| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 498 B |
|
Quellcode-Bibliothek seq_pigeon.pvs Sprache: PVS |
|||||||||
|
seq_pigeon[T: TYPE, (IMPORTING finite_sets@finite_sets_below,
finite_sets@finite_sets_card_eq) S: finite_set[T]]: THEORY BEGIN w: VAR finseq[(S)] seq_pigeon_lem: LEMMA (FORALL (i,j: below(length(w))): i /= j IMPLIES w(i) /= w(j)) IMPLIES length(w) <= card(S) seq_pigeon_hole: THEOREM length(w) > card(S) IMPLIES (EXISTS (i,j: below(length(w))): i /= j AND w(i) = w(j)) END seq_pigeon ¤ 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.0.12Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
