%-------------------------------------------------------------------------
%
% Transitivity properties of the cardinality comparison functions.
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
%
% EXPORTS
% -------
% prelude: functions[T1,T2], functions[T1,T3], functions[T2,T1],
% functions[T2,T3], functions[T3,T1], functions[T3,T2]
% sets_aux: card_comp[T1,T2], card_comp[T1,T3], card_comp[T2,T3],
% card_comp_transitive[T1,T2,T3]
%
%-------------------------------------------------------------------------
card_comp_transitive[T1: TYPE, T2: TYPE, T3: TYPE]: THEORY
EXPORTING ALL WITH functions[T1, T2], functions[T1, T3], functions[T2, T1],
functions[T2, T3], functions[T3, T1], functions[T3, T2],
card_comp[T1, T2], card_comp[T2, T3], card_comp[T1, T3]
BEGIN
IMPORTING card_comp[T1, T2], card_comp[T2, T3], card_comp[T1, T3]
% The following imports are for the proofs only
IMPORTING function_inverse_def[T1, T2], function_inverse_def[T2, T3]
IMPORTING orders@set_dichotomous[T1, T2]
% card_lt
card_lt_transitive: LEMMA
card_lt[T1, T2] AND card_lt[T2, T3] => card_lt[T1, T3]
card_lt_le_transitive: LEMMA
card_lt[T1, T2] AND card_le[T2, T3] => card_lt[T1, T3]
card_lt_eq_transitive: LEMMA
card_lt[T1, T2] AND card_eq[T2, T3] => card_lt[T1, T3]
card_le_lt_transitive: LEMMA
card_le[T1, T2] AND card_lt[T2, T3] => card_lt[T1, T3]
card_eq_lt_transitive: LEMMA
card_eq[T1, T2] AND card_lt[T2, T3] => card_lt[T1, T3]
% card_le
card_le_transitive: LEMMA
card_le[T1, T2] AND card_le[T2, T3] => card_le[T1, T3]
card_le_eq_transitive: LEMMA
card_le[T1, T2] AND card_eq[T2, T3] => card_le[T1, T3]
card_eq_le_transitive: LEMMA
card_eq[T1, T2] AND card_le[T2, T3] => card_le[T1, T3]
% card_eq
card_eq_transitive: LEMMA
card_eq[T1, T2] AND card_eq[T2, T3] => card_eq[T1, T3]
% card_ge
card_eq_ge_transitive: LEMMA
card_eq[T1, T2] AND card_ge[T2, T3] => card_ge[T1, T3]
card_ge_eq_transitive: LEMMA
card_ge[T1, T2] AND card_eq[T2, T3] => card_ge[T1, T3]
card_ge_transitive: LEMMA
card_ge[T1, T2] AND card_ge[T2, T3] => card_ge[T1, T3]
% card_gt
card_eq_gt_transitive: LEMMA
card_eq[T1, T2] AND card_gt[T2, T3] => card_gt[T1, T3]
card_ge_gt_transitive: LEMMA
card_ge[T1, T2] AND card_gt[T2, T3] => card_gt[T1, T3]
card_gt_eq_transitive: LEMMA
card_gt[T1, T2] AND card_eq[T2, T3] => card_gt[T1, T3]
card_gt_ge_transitive: LEMMA
card_gt[T1, T2] AND card_ge[T2, T3] => card_gt[T1, T3]
card_gt_transitive: LEMMA
card_gt[T1, T2] AND card_gt[T2, T3] => card_gt[T1, T3]
END card_comp_transitive
¤ Dauer der Verarbeitung: 0.15 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.
|
