| 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_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 ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28