|
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
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
