NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • Top File of PVS sigma_set Library

     
    %------------------------------------------------------------------------------
    % Top file for sums over sets
    %
    %  MODIFICATIONS:
    %
    %     Author: David Lester, Manchester University 12/12/07
    %
    %------------------------------------------------------------------------------
    top: THEORY
    
    BEGIN
    
      IMPORTING
        absconv_series_aux,      % properties of absolutely convergent series
        finite_enumeration,      % enumerate a finite set
        denumerable_enumeration, % enumerate a countably infinite set
        sigma_bijection,         % re-ordering of finite sums
        sigma_bijection_nat,     % re-ordering of finite sums
    
        countable_convergence,   % convergence properties for countable sums
        sigma_countable,         % countable sums
        convergence_set,         % convergence properties for uncountable sums
        sigma_set                % sums of uncountable sets
    
    
    END top
    

    The tag [*] identifies links that are outside the NASA domain