%-------------------------------------------------------------------------
%
%  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