%-------------------------------------------------------------------------
%
% Subset chains: sets that are totally ordered by the subset relation.
%
% For PVS version 3.2. January 14, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[chain], orders[set[T]], sets[set[T]], sets_lemmas[T]
% orders: chain[set[T], subset?], subset_chain[T]
%
%-------------------------------------------------------------------------
subset_chain[T: TYPE]: THEORY
BEGIN
IMPORTING sets_lemmas[T], chain[set[T], subset?]
C: VAR chain
subset_chain_min: THEOREM FORALL C, (S: (C)): subset?(Intersection(C), S)
subset_chain_intersection: THEOREM
FORALL C: maximal_chain?(C) => member(Intersection(C), C)
END subset_chain
¤ Dauer der Verarbeitung: 0.20 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.
|
