%------------------------------------------------------------------------------ % Re-ordering of sums % % MODIFICATIONS: % % Author: David Lester, Manchester University 12/12/07 % %------------------------------------------------------------------------------
sigma_bijection[T: TYPEFROM 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)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
