|
product_seq: THEORY
%------------------------------------------------------------------------------
%
% Obsolete theory for computing a product over a finite sequence
% See new product theories and product_fseq in structures library
%
% Author: Rick Butler NASA Langley
%
%------------------------------------------------------------------------------
BEGIN
IMPORTING finite_sequences[posnat],
product_seq_scaf
fs: VAR finite_sequence
product(fs): posnat = IF length(fs) = 0 THEN 1
ELSE product_rec(fs,length(fs)-1)
ENDIF
fs1,fs2: VAR finite_sequence
n,m: VAR nat
len0: LEMMA length(fs) = 0 IMPLIES product(fs) = 1
product_mult: LEMMA product(fs1 o fs2) = product(fs1) * product(fs2)
product_empty_seq: LEMMA product(empty_seq) = 1
product_split: LEMMA length(fs) > 1 IMPLIES
product(fs) = product(fs ^ (0, length(fs) - 2)) *
seq(fs)(length(fs) - 1)
product_ge: LEMMA FORALL (n: below(length(fs))): product(fs) >= seq(fs)(n)
gen_seq1(n: posnat): finite_sequence[posnat] =
(# length := 1,
seq := (LAMBDA (ii: below(1)): n) #)
nn: VAR posnat
product_concat1: LEMMA nn * product(fs) = product(fs o gen_seq1(nn))
% IMPORTING product_nat
% product_def: LEMMA product(fs) = product(0,length(fs)-1,fs`seq)
END product_seq
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
