%-------------------------------------------------------------------------
%
% This is the same as card_comp, but made to compare cardinalities of
% sets rather than types. See card_comp.pvs for a discussion.
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% sets_aux: card_comp_set[T1,T2]
%
%-------------------------------------------------------------------------
card_comp_set[T1: TYPE, T2: TYPE]: THEORY
BEGIN
S1: VAR set[T1]
S2: VAR set[T2]
card_lt(S1, S2): bool = NOT (EXISTS (f: [(S2) -> (S1)]): injective?(f))
card_le(S1, S2): bool = EXISTS (f: [(S1) -> (S2)]): injective?(f)
card_eq(S1, S2): bool = EXISTS (f: [(S1) -> (S2)]): bijective?(f)
card_ge(S1, S2): bool = EXISTS (f: [(S2) -> (S1)]): injective?(f)
card_gt(S1, S2): bool = NOT (EXISTS (f: [(S1) -> (S2)]): injective?(f))
END card_comp_set
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
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.
|
