|
product_fseq[T: TYPE+ FROM real]: THEORY
%-------------------------------------------------------------------------------
%
% products over finite sequences of reals
%
% Author: Rick Butler NASA Langley
%
%-------------------------------------------------------------------------------
BEGIN
IMPORTING structures@fseqs[T], product_nat
unk: VAR fsq[T]
fs,fs1,fs2: VAR fseq
product(fs): real = IF length(fs) = 0 THEN 1
ELSE product(0,length(fs)-1,fs`seq)
ENDIF
n,m: VAR nat
len0: LEMMA length(fs) = 0 IMPLIES product(fs) = 1
l1,l2: VAR nat
product_fseq_shift: LEMMA product(l1, l1 + l2 - 1,
LAMBDA (n: nat): IF n < l1 THEN unk`seq(n)
ELSE fs`seq(n - l1) ENDIF)
= product(0, l2 - 1, fs`seq)
product_fseq_concat: LEMMA product(fs1 o fs2) = product(fs1) * product(fs2)
product_fseq_empty_seq: LEMMA product(empty_seq) = 1
product_fseq_split: LEMMA length(fs) > 1 IMPLIES
product(fs) = product(fs ^ (0, length(fs) - 2)) *
seq(fs)(length(fs) - 1)
x: VAR T
product_fseq1: LEMMA product(fseq1(x)) = x
END product_fseq
¤ Dauer der Verarbeitung: 0.18 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.
|
