%-------------------------------------------------------------------------
%
% Implications for finiteness and infiniteness of cardinal relations.
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: infinite_sets_def[T1], infinite_sets_def[T2]
% sets_aux: card_comp_set[T1,T2], card_comp_set[T2,T1],
% card_comp_set_props[T1,T2], infinite_card[T1,T2]
%
%-------------------------------------------------------------------------
infinite_card[T1: TYPE, T2: TYPE]: THEORY
BEGIN
IMPORTING infinite_sets_def[T1], infinite_sets_def[T2]
IMPORTING card_comp_set_props[T1, T2]
S1: VAR set[T1]
S2: VAR set[T2]
finite_card_eq: THEOREM
FORALL S1, S2: card_eq(S1, S2) => (is_finite(S1) IFF is_finite(S2))
infinite_card_eq: COROLLARY
FORALL S1, S2: card_eq(S1, S2) => (is_infinite(S1) IFF is_infinite(S2))
infinite_card_le: THEOREM
FORALL S1, S2: card_le(S1, S2) AND is_infinite(S1) => is_infinite(S2)
infinite_card_ge: THEOREM
FORALL S1, S2: card_ge(S1, S2) AND is_infinite(S2) => is_infinite(S1)
finite_card_le: THEOREM
FORALL S1, S2: card_le(S1, S2) AND is_finite(S2) => is_finite(S1)
finite_card_ge: THEOREM
FORALL S1, S2: card_ge(S1, S2) AND is_finite(S1) => is_finite(S2)
END infinite_card
¤ Dauer der Verarbeitung: 0.1 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.
|
