Quelle  card_comp_set.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