Quelle  card_single.pvs

%-------------------------------------------------------------------------
%
%  Single type properties of the cardinality comparison functions.
%
%  For PVS version 3.2.  November 4, 2004
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  sets_aux: card_comp_set[T,T], card_comp_set_props[T,T], card_single[T],
%    card_comp_set_transitive[T,T,T]
%
%-------------------------------------------------------------------------
card_single[T: TYPE]: THEORY
 BEGIN

  IMPORTING card_comp_set_props[T, T], card_comp_set_transitive[T, T, T]

  % ==========================================================================
  % (ir)reflexivity
  % ==========================================================================

  card_lt_is_irreflexive: JUDGEMENT card_lt HAS_TYPE (irreflexive?[set[T]])
  card_le_is_reflexive:   JUDGEMENT card_le HAS_TYPE (reflexive?[set[T]])
  card_eq_is_reflexive:   JUDGEMENT card_eq HAS_TYPE (reflexive?[set[T]])
  card_ge_is_reflexive:   JUDGEMENT card_ge HAS_TYPE (reflexive?[set[T]])
  card_gt_is_irreflexive: JUDGEMENT card_gt HAS_TYPE (irreflexive?[set[T]])


  % ==========================================================================
  % (anti)symmetry
  % ==========================================================================

  card_lt_is_antisymmetric: JUDGEMENT card_lt HAS_TYPE (antisymmetric?[set[T]])
  card_eq_is_symmetric:     JUDGEMENT card_eq HAS_TYPE (symmetric?[set[T]])
  card_gt_is_antisymmetric: JUDGEMENT card_gt HAS_TYPE (antisymmetric?[set[T]])


  % ==========================================================================
  % transitivity
  % ==========================================================================

  card_lt_is_transitive: JUDGEMENT card_lt HAS_TYPE (transitive?[set[T]])
  card_le_is_transitive: JUDGEMENT card_le HAS_TYPE (transitive?[set[T]])
  card_eq_is_transitive: JUDGEMENT card_eq HAS_TYPE (transitive?[set[T]])
  card_ge_is_transitive: JUDGEMENT card_ge HAS_TYPE (transitive?[set[T]])
  card_gt_is_transitive: JUDGEMENT card_gt HAS_TYPE (transitive?[set[T]])


  % ==========================================================================
  % dichotomy
  % ==========================================================================

  card_le_is_dichotomous: JUDGEMENT card_le HAS_TYPE (dichotomous?[set[T]])
  card_ge_is_dichotomous: JUDGEMENT card_ge HAS_TYPE (dichotomous?[set[T]])


  % ==========================================================================
  % equivalence
  % ==========================================================================

  card_eq_is_equivalence: JUDGEMENT card_eq HAS_TYPE equivalence[set[T]]

 END card_single