|
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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
