| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/exact_real_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Impressum product_int.pvs Sprache: PVS |
|||||||||
|
product_int: THEORY
%------------------------------------------------------------------------------ % The products theory introduces and defines properties of the product % function that multiples an arbitrary function F: [int -> int] over a range % from low to high % % high % ---- % product(low, high, F) = | | F(j) % | | % j = low % % AUTHORS: % % Rick Butler NASA Langley Research Center % Paul Miner NASA Langley Research Center % %------------------------------------------------------------------------------ BEGIN IMPORTING product[int] int_is_T_high: JUDGEMENT int SUBTYPE_OF T_high int_is_T_low : JUDGEMENT int SUBTYPE_OF T_low low, high, i, j, m: VAR int F: VAR function[int -> int] % --------- Following Theorems Not Provable In Generic Framework ------- product_shift : THEOREM product(low+j,high+j,F) = product(low,high, (LAMBDA (i: int): F(i+j))) product_split_ge : THEOREM low-1 <= m AND m <= high IMPLIES product(low, high, F) = product(low, m, F) * product(m+1, high, F) product_first_ge : THEOREM high >= low IMPLIES product(low, high, F) = F(low) * product(low+1, high, F) product_mid_ge : THEOREM high >= i AND i >= low IMPLIES product(low, high, F) = product(low, i-1, F) * F(i) * product(i+1, high, F) product_last_ge : THEOREM high >= low IMPLIES product(low, high, F) = product(low, high-1, F) * F(high) END product_int ¤ 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.3Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
