%-------------------------------------------------------------------------
%
% Chains (totally ordered subsets of a poset).
%
% For PVS version 3.2. January 14, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[chain], orders[T], sets[T]
% orders: chain[T, <=]
%
%-------------------------------------------------------------------------
chain[T: TYPE, <=: (partial_order?[T])]: THEORY
BEGIN
IMPORTING orders[T], sets[T]
S: VAR set
% The chain type
chain?(S): bool = total_order?(restrict[[T, T], [(S), (S)], bool](<=))
chain: TYPE+ = (chain?) CONTAINING emptyset
ch, ch1, ch2: VAR chain
% Maximal chains
maximal_chain?(ch): bool = NOT (EXISTS ch1: strict_subset?(ch, ch1))
% Chain properties
subset_chain: THEOREM FORALL ch, S: subset?(S, ch) => chain?(S)
intersection_chain: JUDGEMENT intersection(ch1, ch2) HAS_TYPE chain
% Chain order
IMPORTING orders[chain]
chain_order(ch1, ch2): bool = subset?(ch1, ch2)
chain_order_partial: JUDGEMENT
chain_order HAS_TYPE (partial_order?[chain])
END chain
¤ Dauer der Verarbeitung: 0.13 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.
|
