| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sigma_set/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle sigma_bijection.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% Re-ordering of sums % % MODIFICATIONS: % % Author: David Lester, Manchester University 12/12/07 % %------------------------------------------------------------------------------ sigma_bijection[T: TYPE FROM int]: THEORY BEGIN ASSUMING connected_domain: ASSUMPTION (FORALL (x, y: T), (z: integer): x <= z AND z <= y IMPLIES T_pred(z)) ENDASSUMING IMPORTING reals@sigma low,high, l,h,n,m,i : VAR T rng, nn : VAR nat pn : VAR posnat z : VAR int a,x,B : VAR real F : VAR [T->real] subrange_T(n,m): TYPE = {k:T | n <= k AND k <= m} % The following theorem shows that we can re-order the summation of % any finite sum. sigma_bijection: LEMMA low <= high IMPLIES FORALL (phi:(bijective?[subrange_T(low,high),subrange_T(low,high)])): sigma[subrange_T(low,high)](low,high,F) = sigma[subrange_T(low,high)](low,high,F o phi) END sigma_bijection ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28