| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle well_ordered_finite.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % 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 (jamesj@acm.org), 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.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28