Impressum seq_pigeon.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