%-------------------------------------------------------------------------
%
%  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