| products/sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: CoqUntersuchung 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 ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.26Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
