products/sources/formale sprachen/PVS/summaries/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: 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
 

[ zur Elbe Produktseite wechseln0.40Quellennavigators  Analyse erneut starten  ]