%-------------------------------------------------------------------------
%
% Well-orderings on sets of natural numbers.
%
% For PVS version 3.2. February 28, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), 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]
well_lt_nat: THEOREM FORALL S: well_ordered?[(S)](<)
well_gt_nat: AXIOM FORALL F: well_ordered?[(F)](>) %% Proved in orders library
END well_nat
¤ Dauer der Verarbeitung: 0.8 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.
|
