Quelle sigma_posnat.pvs Sprache: PVS

sigma_posnat: THEORY
%------------------------------------------------------------------------------
% The summations theory introduces and defines properties of the sigma
% function that sums an arbitrary function F: [T -> real] over a range
% from low to high
%
%             high
%           ----
%  sigma(low, high, F) =  \     F(j)
%           /
%           ----
%          j = low
%
%------------------------------------------------------------------------------

BEGIN

  IMPORTING sigma[posnat]

  int_is_T_high: JUDGEMENT int SUBTYPE_OF T_high
  posnat_is_T_low : JUDGEMENT posnat SUBTYPE_OF T_low

  low, n, m: VAR posnat
  high: VAR int
  F: VAR function[posnat -> real]

% --------- Following Theorems Not Provable In Generic Framework -------

  sigma_shift:  THEOREM sigma(low+m,high+m,F) =
                              sigma(low,high, (LAMBDA (n: posnat): F(n+m)))

  sigma_shift_neg:  THEOREM low - m > 0 IMPLIES
                         sigma(low-m,high-m,F) =
                             sigma(low,high, (LAMBDA n: IF n-m <= 0 THEN 0
                                                        ELSE F(n-m)
                                                        ENDIF))

  sigma_split_ge : THEOREM low-1 <= m AND m <= high IMPLIES
                            sigma(low, high, F) =
                                     sigma(low, m, F) + sigma(m+1, high, F)

END sigma_posnat

quality97%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.