| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle permutations_fseq.pvs Sprache: PVS |
|||||||||
|
permutations_fseq[T: TYPE+, <= : (total_order?[T]) ]: THEORY
%------------------------------------------------------------------------ % % permutations_fseq (basic definitions and properties) % ------------------------------------------- % % Author: Ricky W. Butler % % % permutation?(A1,A2): bool = (EXISTS (f: [below(N) -> below(N)]): % bijective?(f) AND (FORALL ii: A1(ii) = A2(f(ii)))) % % %------------------------------------------------------------------------ BEGIN IMPORTING fseqs[T] A,B,A1,A2,A3: VAR fsq[T] %% or fseq x, t: VAR T i,j: VAR nat permutation?(A,B): bool = (EXISTS (f: [below(length(A)) -> below(length(B))]): bijective?(f) AND (FORALL (ii: below(length(A))): seq(A)(ii) = seq(B)(f(ii)))) IMPORTING finite_sets@finite_sets_card_eq, finite_sets@finite_sets_below perm_length : LEMMA permutation?(A,B) IMPLIES length(A) = length(B) perm_reflexive: LEMMA permutation?(A,A) perm_symmetric: LEMMA permutation?(A,B) IMPLIES permutation?(B,A) perm_tran : LEMMA permutation?(A1,A2) AND permutation?(A2,A3) IMPLIES permutation?(A1,A3) perm_in? : LEMMA permutation?(A1,A2) IMPLIES (in?(x,A1) = in?(x,A2)) END permutations_fseq ¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28