| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle fseqs_ops_real.pvs Sprache: PVS |
|||||||||
|
fseqs_ops_real: THEORY
%------------------------------------------------------------------------ % % Defines some convenient operations over finite sequences of reals % % EXPERIMENTAL % %------------------------------------------------------------------------ BEGIN IMPORTING fseqs_ops[real] fs,gs: VAR fseq nefs: VAR ne_fseq i,n: VAR nat x: VAR real nn_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) >= 0} pos_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) > 0} neg_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) < 0} nz_fseq: TYPE = {fs: fseq | FORALL (n: nat): n < l(fs) IMPLIES fs`seq(n) /= 0} % ------------ pointwise addition, subtraction, and multiplication mmin(m,n:nat): MACRO nat = IF m > n THEN n ELSE m ENDIF ; +(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN (# length := len, seq := (LAMBDA n: IF n < len THEN fs(n) + gs(n) ELSE default ENDIF) #) ; -(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN (# length := len, seq := (LAMBDA n: IF n < len THEN fs(n) - gs(n) ELSE default ENDIF) #) ; *(fs,gs): fseq = LET len = mmin(l(fs),l(gs)) IN (# length := len, seq := (LAMBDA n: IF n < len THEN fs(n) * gs(n) ELSE default ENDIF) #) ; nzgs: VAR nz_fseq ; /(fs,nzgs): fseq = LET len = mmin(l(fs),l(nzgs)) IN (# length := len, seq := (LAMBDA n: IF n < len THEN fs(n) / nzgs(n) ELSE default ENDIF) #) ; END fseqs_ops_real ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28