%-------------------------------------------------------------------------
%
% Chain chains: chains of Ts ordered by inclusion.
%
% For PVS version 3.2. January 14, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: finite_sets[subchain], orders[chain_chain], orders[subchain],
% orders[T], relations[subchain], sets[subchain], sets[T]
% orders: bounded_orders[subchain], chain[subchain,chain_incl],
% chain[T,<=], chain_chain[T,<=], relations_extra[subchain]
%
%-------------------------------------------------------------------------
chain_chain[T: TYPE, <=: (partial_order?[T])]: THEORY
BEGIN
% ==========================================================================
% The lower level chains
% ==========================================================================
IMPORTING chain[T, <=]
subchain: TYPE+ = chain[T, <=]
subc1, subc2: VAR subchain
% ==========================================================================
% The higher level chains
% ==========================================================================
chain_incl(subc1, subc2): bool = subset?(subc1, subc2)
chain_incl_partial_order: JUDGEMENT
chain_incl HAS_TYPE (partial_order?[subchain])
IMPORTING bounded_orders[subchain], chain[subchain, chain_incl]
chain_chain: TYPE+ = chain[subchain, chain_incl]
C: VAR chain_chain
chain_union(C): subchain = Union(extend[set[T], subchain, bool, FALSE](C))
chain_union_upper_bound: LEMMA
FORALL (C: chain_chain):
bounded_orders.upper_bound?(chain_union(C), C, chain_incl)
END chain_chain
¤ Dauer der Verarbeitung: 0.17 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.
|
