%-------------------------------------------------------------------------
%
% Sets with a strict total order and with the property that the below set
% of every element is finite are well orderings such that every element
% but the first has a previous element.
%
% For PVS version 3.2. February 28, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: orders[T], relation_props2[T, T, T, T], relations[T], sets[T]
% finite_sets: finite_sets_inductions, finite_sets_minmax
% orders: bounded_orders[T], closure_ops[T], indexed_sets_extra,
% minmax_orders[T], ordered_subset[T], relation_iterate[T],
% relations_extra[T], well_ordered_finite[T,<],
% well_ordered_traversal[T]
%
%-------------------------------------------------------------------------
well_ordered_finite[T: TYPE, <: (strict_total_order?[T])]: THEORY
BEGIN
ASSUMING
IMPORTING ordered_subset[T]
finite_below: ASSUMPTION FORALL (t: T): is_finite(below(t, <))
ENDASSUMING
IMPORTING well_ordered_traversal[T]
t: VAR T
S: VAR (nonempty?[T])
nonempty_has_least: JUDGEMENT
(nonempty?[T]) SUBTYPE_OF (has_least?(reflexive_closure(<)))
finite_well_ordered: JUDGEMENT < HAS_TYPE (well_ordered?)
nonlast_has_next: JUDGEMENT (nonlast(<)) SUBTYPE_OF (has_next?(<))
nonfirst_has_prev: JUDGEMENT (nonfirst(<)) SUBTYPE_OF (has_prev?(<))
finite_last: THEOREM has_last?(<) IMPLIES is_finite_type[T]
END well_ordered_finite
¤ Dauer der Verarbeitung: 0.16 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.
|
