%------------------------------------------------------------------------- % % The Well-Ordering Principle: every set can be well-ordered. This is % equivalent to the Axiom of Choice, Zorn's Lemma, and Kuratowski's Lemma. % % For PVS version 3.2. February 28, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: finite_sets[T], orders[T], relations[T], sets[T] % orders: bounded_orders[T], relations_extra[T], well_ordering[T] % %-------------------------------------------------------------------------
well_ordering[T: TYPE]: THEORY
% Hide all the technical details from public view EXPORTING well_ordering WITH bounded_orders[T], finite_sets[T], orders[T],
relations_extra[T], relations[T], sets[T]
BEGIN
IMPORTING bounded_orders
% ========================================================================== % A partial order on well-ordered sets % ==========================================================================
%% Types
ordered_set: TYPE = [A: set[T], (well_ordered?[(A)])]
%% Variables
t: VAR T
<: VAR pred[[T, T]]
ord1, ord2: VAR ordered_set
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.
