|
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
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
