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