%-------------------------------------------------------------------------
%
% More theorems for the prelude's sets_lemmas theory.
%
% For PVS version 3.2. March 15, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: sets_lemmas[T]
% sets_aux: sets_lemmas_extra[T]
%
%-------------------------------------------------------------------------
sets_lemmas_extra[T: TYPE]: THEORY
BEGIN
IMPORTING sets_lemmas[T]
disjoint_commutative: LEMMA
FORALL (S, R: set[T]): disjoint?(S, R) IMPLIES disjoint?(R, S)
END sets_lemmas_extra
¤ Dauer der Verarbeitung: 0.3 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.
|
