| products/sources/formale Sprachen/PVS/reals/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: versionResource.template Sprache: PVSOriginal von: 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 ¤ Dauer der Verarbeitung: 0.8 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
