%------------------------------------------------------------------------- % % Well-orderings on sets of natural numbers. % % For PVS version 3.2. February 28, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: finite_sets[nat], orders[nat], sets[nat], relations[nat] % finite_sets: finite_sets_inductions, finite_sets_minmax % orders: bounded_orders[nat], minmax_orders[nat], relations_extra[nat], % well_nat % %-------------------------------------------------------------------------
well_nat: THEORY BEGIN
IMPORTING minmax_orders[nat]
n, m: VAR nat
S: VAR set[nat]
F: VAR finite_set[nat]
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.
