|
sigma_swap[T: TYPE FROM int]: THEORY
%------------------------------------------------------------------------------
% A theory on swapping summation signs
%
% AUTHOR:
%
% Anthony Narkawicz NASA Langley Research Center
%------------------------------------------------------------------------------
BEGIN
ASSUMING
connected_domain: ASSUMPTION (FORALL (x, y: T), (z: integer):
x <= z AND z <= y IMPLIES T_pred(z))
ENDASSUMING
IMPORTING sigma[T]
low,low1,
low2 : VAR T_low
high,high1,
high2 : VAR T_high
l,h,n,m,i,j : VAR T
rng, nn : VAR nat
pn : VAR posnat
z : VAR int
a,x,B : VAR real
F : VAR [[T,T]->real]
sigma_swap: LEMMA
sigma(low1,high1,LAMBDA (i:T): sigma(low2,high2,LAMBDA (j:T): F(i,j)))
= sigma(low2,high2,LAMBDA (j:T): sigma(low1,high1,LAMBDA (i:T): F(i,j)))
sigma_swap_triangle: LEMMA
high1 >= high2 IMPLIES
sigma(low1,high1,LAMBDA (i:T): sigma(i,high2,LAMBDA (j:T): F(i,j)))
= sigma(low1,high2,LAMBDA (j:T): sigma(low1,j,LAMBDA (i:T): F(i,j)))
END sigma_swap
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
