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: permutations.pvs   Sprache: Unknown

permutations[N: nat, T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% permutations of arrays
%
% Author: Rick Butler
%
%------------------------------------------------------------------------
BEGIN

  A,A1,A2,A3: VAR ARRAY[below(N) -> T] 
  ii: VAR below[N]
  x: VAR T

  IMPORTING below_arrays[N,T]

  permutation_of?(A1,A2): bool = (EXISTS (f: [below(N) -> below(N)]): 
                      bijective?(f) AND (FORALL ii: A1(ii) = A2(f(ii))))

  perm_reflexive: LEMMA permutation_of?(A,A)

  perm_symmetric: LEMMA permutation_of?(A1,A2) IMPLIES permutation_of?(A2,A1)

  perm_tran     : LEMMA permutation_of?(A1,A2) AND permutation_of?(A2,A3) 
                            IMPLIES permutation_of?(A1,A3)

  perm_in?      : LEMMA permutation_of?(A1,A2) IMPLIES 
                             (in?(x,A1) = in?(x,A2))

END permutations

[ Dauer der Verarbeitung: 0.18 Sekunden  (vorverarbeitet)  ]