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