Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: Emacs_Insert_File.bsh   Sprache: Unknown

%-------------------------------------------------------------------------
%
%  Operations on countable families of sets.
%
%  For PVS version 3.2.  February 10, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James ([email protected]), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: finite_sets[finite_set[T]], finite_sets[set[T]], finite_sets[T],
%    infinite_sets_def[finite_set[T]], infinite_sets_def[set[T]],
%    infinite_sets_def[T]
%  sets_aux: card_comp_set[finite_set[T],finite_set[T]],
%    card_comp_set[finite_set[T],nat], card_comp_set[nat,finite_set[T]],
%    card_comp_set[nat,set[T]], card_comp_set[nat,T],
%    card_comp_set[set[T],nat], card_comp_set[set[T],set[T]],
%    card_comp_set[set[T],T], card_comp_set[T,nat], card_comp_set[T,set[T]],
%    card_comp_set[T,T], card_comp_set_props[finite_set[T],finite_set[T]],
%    card_comp_set_props[finite_set[T],nat], card_comp_set_props[set[T],nat],
%    card_comp_set_props[set[T],set[T]], card_comp_set_props[T,nat],
%    card_comp_set_props[T,set[T]], card_comp_set_props[T,T],
%    card_comp_set_transitive[nat,T,set[T]], card_comp_set_transitive[nat,T,T],
%    card_power_set[T], card_sets_lemmas[T], card_single[finite_set[T]],
%    card_single[set[T]], card_single[T], countability[finite_set[T]],
%    countability[set[T]], countability[T], countable_props[finite_set[T]],
%    countable_props[set[T]], countable_props[T], countable_set,
%    countable_setofsets[T]
%
%-------------------------------------------------------------------------
countable_setofsets[T: TYPE]: THEORY
 BEGIN

  IMPORTING countable_set,
            countable_props[T],
            countable_props[set[T]],
            countable_props[finite_set[T]]

  S: VAR setofsets[T]

  countable_union1: THEOREM
    FORALL S:
      is_countable[set[T]](S) AND every(is_countable)(S) =>
       is_countable[T](Union(S))

  %% Note that the converse of conutable_union1 is not quite true; it is
  %% possible to have an uncountable set whose union is countable.  For
  %% example, consider the set of natural numbers.  Its power set is
  %% uncountable, and the union of the power set is the (countable) set of
  %% natural numbers.
  countable_union2: THEOREM
    FORALL S: is_countable[T](Union(S)) => every(is_countable)(S)

  countable_intersection: THEOREM
    FORALL S:
      nonempty?(S) AND every(is_countable)(S) =>
       is_countable(Intersection(S))

  %% The finite subsets of a given set.  For a finite set, this is the
  %% powerset.  Otherwise, it is the finite elements of the powerset.

  finite_subsets(S: set[T]): set[finite_set[T]] =
      {F: finite_set[T] | subset?(F, S)}

  countable_finite_subsets: JUDGEMENT
    finite_subsets(S: countable_set[T]) HAS_TYPE countable_set[finite_set[T]]

  countably_infinite_finite_subsets: JUDGEMENT
    finite_subsets(S: countably_infinite_set[T])
      HAS_TYPE countably_infinite_set[finite_set[T]]

END countable_setofsets

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

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik