%-------------------------------------------------------------------------
%
% Properties of well-ordered relations on sets.
%
% For PVS version 3.2. February 28, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: relation_props2[T, T, T, T], sets[T]
% orders: closure_ops[T], indexed_sets_extra, isomorphism,
% monotone_functions[T,T], ordered_subset[T], relation_iterate[T],
% relations_extra, well_ordered_props[T,<]
%
%-------------------------------------------------------------------------
well_ordered_props[T: TYPE, <: (well_ordered?[T])]: THEORY
BEGIN
IMPORTING ordered_subset[T], monotone_functions[T, T], isomorphism
t, r: VAR T
S, R: VAR set[T]
initial_segment: TYPE = {pre: (prefix?(<)) | EXISTS t: NOT member(t, pre)}
seg: VAR initial_segment
induced_prefixes: LEMMA FORALL seg: EXISTS t: seg = below(t, <)
increasing_well_ordered: LEMMA
FORALL (f: (increasing?(<, <))), t: t < f(t) OR t = f(t)
initial_segment_isomorphism: COROLLARY
FORALL seg:
NOT isomorphic?[T, (seg)]
(<, restrict[[T, T], [(seg), (seg)], bool](<))
END well_ordered_props
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
