| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Doc/Implementation/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 7 kB |
|
Quelle permutation_ops.pvs Sprache: PVS |
|||||||||
|
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 ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28