Quelle  sigma_bijection_nat.pvs   Sprache: PVS

%------------------------------------------------------------------------------
% Re-ordering of series
%
%  MODIFICATIONS:
%
%     Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
sigma_bijection_nat: THEORY

BEGIN

  IMPORTING sigma_bijection,
            series@series

  n: VAR nat
  a: VAR sequence[real]

  series_bijection: LEMMA
      FORALL (phi:(bijective?[below[n+1],below[n+1]])):
         series(a)(n) = series(a o extend[nat,below[n+1],below[n+1],0](phi))(n)

END sigma_bijection_nat