| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle sigma_below.pvs Sprache: PVS |
|||||||||
|
sigma_below[N: posnat]: THEORY %below(0) is an empty type
%sigma_below[N: nat]: THEORY %------------------------------------------------------------------------------ % The summations theory provides properties of the sigma % function that sums an arbitrary function F: [below[N] -> real] over a range % from low to high % % high % ---- % sigma(low, high, F) = \ F(j) % / % ---- % j = low % % %------------------------------------------------------------------------------ BEGIN IMPORTING sigma[below(N)] int_below: TYPE = {i:int | i < N} int_below_T_high: JUDGEMENT int_below SUBTYPE_OF T_high nat_is_T_low: JUDGEMENT nat SUBTYPE_OF T_low low :VAR nat high : VAR int_below n, m, i: VAR below[N] F: VAR function[below[N] -> real] % play1: LEMMA FORALL (x: below[N]): EXISTS (j: below(N)): j <= x; % play2: LEMMA FORALL (x: below[N]): EXISTS (j: below(N)): x <= j; % AUTO_REWRITE+ play1, play2 % --------- 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_below ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28