| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle card_comp.pvs Sprache: 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 (jamesj@acm.org), 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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28