SSL card_comp_set.pvs Sprache: PVS

%-------------------------------------------------------------------------
%
%  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 (jamesj@acm.org), 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

quality100%

¤ Dauer der Verarbeitung: 0.7 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.