| 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_fseq_posnat.pvs Sprache: PVS |
|||||||||
|
product_fseq_posnat: THEORY
%------------------------------------------------------------------------------- % % products over finite sequences of posnats % % Author: Rick Butler NASA Langley % % NOTE: Later we may derive this theory from product_fseq % %------------------------------------------------------------------------------- BEGIN IMPORTING structures@fseqs[posnat], product_nat unk: VAR fsq[posnat] fs,fs1,fs2: VAR fseq n,m: VAR nat F: VAR [nat -> posnat] product_nat_nat: JUDGEMENT product(m,n,F) HAS_TYPE posnat product(fs): posnat = IF length(fs) = 0 THEN 1 ELSE product(0,length(fs)-1,fs`seq) ENDIF 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) product_fseq_ge: LEMMA FORALL (n: below(length(fs))): product(fs) >= seq(fs)(n) nn: VAR posnat product_fseq_concat1: LEMMA nn * product(fs) = product(fs o fseq1(nn)) product_fseq1: LEMMA product(fseq1(nn)) = nn END product_fseq_posnat ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28