permutation_ops[N: posnat]: THEORY
%----------------------------------------------------------------------------
% the theory of bijective mappings from below(N) to below(N)
%
% Author: Alfons Geser, National Institute of Aerospace, Hampton, VA, 2003
%----------------------------------------------------------------------------
BEGIN

  IMPORTING permutation[N], sort_array[N,below(N),<=]

  i,j,k  : VAR below(N)
  m      : VAR below(N+1)
  pi, rho: VAR permutation

  sorted_iff_id_lem  : LEMMA (FORALL i: i >= m => pi(i) = i) &
                           (FORALL (i,j): i < j => pi(i) <= pi(j)) IMPLIES
                              pi(i) = i

  % a permutation is sorted iff it is the identity

  sorted_iff_id      : THEOREM  sorted?(pi) <=> pi = id

END permutation_ops