%-------------------------------------------------------------------------
%
%  Properties of well-ordered relations on sets.
%
%  For PVS version 3.2.  February 28, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James (jamesj@acm.org), University of Kansas
%
%  EXPORTS
%  -------
%  prelude: relation_props2[T, T, T, T], sets[T]
%  orders: closure_ops[T], indexed_sets_extra, isomorphism,
%    monotone_functions[T,T], ordered_subset[T], relation_iterate[T],
%    relations_extra, well_ordered_props[T,<]
%
%-------------------------------------------------------------------------
well_ordered_props[T: TYPE, <: (well_ordered?[T])]: THEORY
 BEGIN

  IMPORTING ordered_subset[T], monotone_functions[T, T], isomorphism

  t, r: VAR T
  S, R: VAR set[T]

  initial_segment: TYPE = {pre: (prefix?(<)) | EXISTS t: NOT member(t, pre)}

  seg: VAR initial_segment

  induced_prefixes: LEMMA FORALL seg: EXISTS t: seg = below(t, <)

  increasing_well_ordered: LEMMA
    FORALL (f: (increasing?(<, <))), t: t < f(t) OR t = f(t)

  initial_segment_isomorphism: COROLLARY
    FORALL seg:
      NOT isomorphic?[T, (seg)]
              (<, restrict[[T, T], [(seg), (seg)], bool](<))

 END well_ordered_props