%-------------------------------------------------------------------------
%
% Lemmas about set operations and their implications for the cardinality
% comparison relations.
%
% For PVS version 3.2. November 4, 2004
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), 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_sets_lemmas[T]
%
%-------------------------------------------------------------------------
card_sets_lemmas[T: TYPE]: THEORY
BEGIN
IMPORTING card_single[T]
t: VAR T
S, R: VAR set[T]
empty_card_le: LEMMA FORALL S: card_le(emptyset[T], S)
nonempty_card_lt: LEMMA FORALL S: card_lt(emptyset[T], S) IFF nonempty?(S)
full_card_le: LEMMA FORALL S: card_le(S, fullset[T])
add_card_le: LEMMA FORALL S, t: card_le(S, add(t, S))
remove_card_ge: LEMMA FORALL S, t: card_ge(S, remove(t, S))
subset_card_le: LEMMA FORALL S, R: subset?(S, R) => card_le(S, R)
strict_subset_card_lt: LEMMA
FORALL S, R: subset?(S, R) AND card_lt(S, R) => strict_subset?(S, R)
union_card_le1: LEMMA FORALL S, R: card_le(S, union(S, R))
union_card_le2: LEMMA FORALL S, R: card_le(R, union(S, R))
intersection_card_le1: LEMMA FORALL S, R: card_le(intersection(S, R), S)
intersection_card_le2: LEMMA FORALL S, R: card_le(intersection(S, R), R)
difference_card_le: LEMMA FORALL S, R: card_le(difference(S, R), S)
END card_sets_lemmas
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
