Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: card_comp.pvs Sprache: PVS

Original von: PVS^©

%-------------------------------------------------------------------------
%
%  Compare set cardinalities for any two sets, whether finite or infinite.
%  See cardinal.pvs for a cardinality(S) function that operates on any
%  set, whether finite or infinite, using these definitions as a basis.
%
%  We have to take great care with empty sets.  The basic problem is that
%  there is NO function from a nonempty domain to an empty range.  This is
%  why card_lt and card_ge deal with functions that are "reversed" from
%  those in the other definitions, so that we can talk about injective
%  functions (which exist from empty domains to nonempty ranges) instead
%  of surjective functions (which do not exist from nonempty domains to
%  empty ranges).
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James ([email protected]), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: functions[T1,T2], functions[T2,T1]
%  sets_aux: card_comp[T1,T2]
%
%-------------------------------------------------------------------------
card_comp[T1: TYPE, T2: TYPE]: THEORY
BEGIN

  IMPORTING functions[T1, T2], functions[T2, T1]

  card_lt: bool = NOT (EXISTS (f: [T2 -> T1]): injective?(f))

  card_le: bool = EXISTS (f: [T1 -> T2]): injective?(f)

  card_eq: bool = EXISTS (f: [T1 -> T2]): bijective?(f)

  card_ge: bool = EXISTS (f: [T2 -> T1]): injective?(f)

  card_gt: bool = NOT (EXISTS (f: [T1 -> T2]): injective?(f))

END card_comp

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.