products/sources/formale Sprachen/PVS/sigma_set/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: sigma_bijection.pvs   Sprache: PVS

Original von: 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.0 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff