| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 881 B |
|
Quelle permutations.pvs Sprache: PVS |
|||||||||
|
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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28