| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle product_seq.pvs Sprache: PVS |
|||||||||
|
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.9 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28