sigma_fseq: THEORY
%------------------------------------------------------------------------------
% The summations theory provides properties of the sigma 
% function that sums up a sequence of reals, e.g. fseq[real]
%
%              l(fs)
%            ----
%             sigma(fs) =  \     fs`seq(j)
%            /
%            ----
%           j = 0
%
%  WILL NOT TYPECHECK BECAUSE OF PVS BUG:
%
%      Error: the assertion (fully-instantiated? domtypes) failed.
%       
%------------------------------------------------------------------------------
BEGIN

  IMPORTING sigma_fseq_def

  fs_nnr   : VAR fseq[nonneg_real]
  fs_npr   : VAR fseq[nonpos_real]
  fs_nat   : VAR fseq[nat]
  fs_npi   : VAR fseq[nonpos_int]
  fs_posnat: VAR fseq[posnat]


  sigma_fs_nnr  : JUDGEMENT sigma[nonneg_real](fs_nnr) HAS_TYPE nonneg_real

  sigma_fs_npr  : JUDGEMENT sigma[nonpos_real](fs_npr) HAS_TYPE nonpos_real

  sigma_fs_nat  : JUDGEMENT sigma[nat](fs_nat)         HAS_TYPE nat

  sigma_fs_npi  : JUDGEMENT sigma[nonpos_int](fs_npi)  HAS_TYPE nonpos_int

                                              
END sigma_fseq