%------------------------------------------------------------------------- % % Every totally ordered finite set has an order-preserving bijection % with a below set. % % For PVS version 3.2. March 5, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: orders[T] % finite_sets: finite_sets_inductions, finite_sets_minmax % orders: bounded_orders[T], closure_ops[T], finite_below[T], % indexed_sets_extra, minmax_orders[T], relations_extra[T], % relation_iterate[T] % %-------------------------------------------------------------------------
finite_below[T: TYPE]: THEORY BEGIN
IMPORTING closure_ops[T], minmax_orders[T]
S: VAR finite_set[T]
<: VAR (strict_total_order?[T])
% Select the nth element of the set
nth(S, <)(n: below[card(S)]): RECURSIVE (S) = IF n = 0 THEN least(reflexive_closure(<))(S) ELSE nth(remove(least(reflexive_closure(<))(S), S), <)(n - 1) ENDIF MEASURE n
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.
