products/sources/formale sprachen/PVS/summaries/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: permutation.prf   Sprache: Unknown

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

  permutation: TYPE+ = {pi: [below(N) -> below(N)] | bijective?(pi)}
               CONTAINING id

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

  inverse_id         : LEMMA N > 0 IMPLIES inverse[below(N),below(N)](id) = id

  inverse_composition: LEMMA N > 0 IMPLIES inverse(pi o rho) = inverse(rho) o inverse(pi)

  transpose(i,j): permutation = 
          LAMBDA k: IF k = j THEN i ELSIF k = i THEN j ELSE k ENDIF

  involutorian_transpose: LEMMA transpose(i,j)(transpose(i,j)(k)) = k

END permutation

[ zur Elbe Produktseite wechseln0.1Quellennavigators  Analyse erneut starten  ]