Quellcode-Bibliothek sigma_upto.pvs Sprache: PVS

sigma_upto[N: nat]: THEORY
%------------------------------------------------------------------------------
% The summations theory provides properties of the sigma
% function that sums an arbitrary function F: [upto[N] -> real] over a range
% from low to high
%
%             high
%           ----
%  sigma(low, high, F) =  \     F(j)
%           /
%           ----
%          j = low
%
%
%------------------------------------------------------------------------------

BEGIN

  IMPORTING sigma[upto[N]]

  int_upto: TYPE = {i:int | i <= N}
  int_upto_T_high: JUDGEMENT int_upto SUBTYPE_OF T_high
  nat_is_T_low: JUDGEMENT nat SUBTYPE_OF T_low

  low, high, n, m: VAR upto[N]
  F: VAR function[upto[N] -> real]

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

  sigma_first_ge : THEOREM high >= low IMPLIES
                           sigma(low, high, F) = F(low) + sigma(low+1, high, F)

  sigma_last_ge  : THEOREM high >= low IMPLIES
                          sigma(low, high, F) = sigma(low, high-1, F) + F(high)

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

% ---- Auto-rewrites

  nn: VAR negint
  sigma_0_neg: LEMMA sigma(0,nn,F) = 0
  AUTO_REWRITE+ sigma_0_neg

END sigma_upto

quality100%

¤ 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.0.26Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.

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.