|
%------------------------------------------------------------------------------
% Extra properties of series.
%
% MODIFICATIONS:
%
% Author: David Lester, Manchester University 12/12/07
%
%------------------------------------------------------------------------------
series_aux: THEORY
BEGIN
IMPORTING series,
orders@well_nat % proof only
i: VAR int
n,m,N: VAR nat
pn: VAR posnat
x,l1,l2,c: VAR real
nnx: VAR nnreal
a,b: VAR sequence[real]
nna: VAR sequence[nnreal]
phi: VAR (bijective?[nat,nat])
zero_tail_series_conv: LEMMA (FORALL m: n < m => a(m) = 0) =>
convergent?(series(a))
zero_tail_series_limit: LEMMA (FORALL m: n < m => a(m) = 0) =>
limit(series(a)) = series(a)(n)
zero_tail_series: LEMMA (FORALL m: n < m => a(m) = 0) =>
convergence(series(a), series(a)(n))
single_nz_series_conv: LEMMA (FORALL m: n /= m => a(m) = 0) =>
convergent?(series(a))
single_nz_series_limit: LEMMA (FORALL m: n /= m => a(m) = 0) =>
limit(series(a)) = a(n)
single_nz_series: LEMMA (FORALL m: n /= m => a(m) = 0) =>
convergence(series(a), a(n))
limit_nonneg: LEMMA convergent?(nna) => limit(nna) >= 0
convergence_nonneg: LEMMA convergence(series(nna),nnx) =>
FORALL n: series(nna)(n) <= nnx
nonneg_series_bij: LEMMA convergence(series(nna),nnx) =>
convergence(series(nna o phi),nnx)
nonneg_series_bij_conv: LEMMA convergent?(series(nna)) =>
convergent?(series(nna o phi))
nonneg_series_bij_limit:LEMMA convergent?(series(nna)) =>
limit(series(nna)) = limit(series(nna o phi))
abs_series_bij: LEMMA convergent?(series(abs(a))) AND
convergence(series(a),x) =>
convergence(series(a o phi),x)
abs_series_bij_conv: LEMMA convergent?(series(abs(a))) =>
convergent?(series(a o phi))
abs_series_bij_limit: LEMMA convergent?(series(abs(a))) =>
limit(series(a)) = limit(series(a o phi))
END series_aux
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.20Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
