|
step_fun_def[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
%
% Integration over Step Functions:
%
% Author: Rick Butler NASA Langley Research Center
%
%------------------------------------------------------------------------------
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
a,b,x,y,z,xx: VAR T
c: VAR real
f,g: VAR [T -> real]
xl,xh: VAR T
IMPORTING integral_def[T]
step_function_on?(a:T,b:{x:T|a<x},f:[T->real], P: partition[T](a,b)): bool =
Let N = length(P), xx = seq(P) IN
(FORALL (ii: below(N-1)): (EXISTS (fv: real):
(FORALL (x: open_interval[T](xx(ii),xx(ii+1))):
f(x) = fv)))
% step_function?(a:T,b:{x:T|a<x},f:[T -> real]): bool
% = (EXISTS (P: partition(a,b)):
% Let N = length(P), xx = seq(P) IN
% (FORALL (ii: below(N-1)): (EXISTS (fv: real):
% (FORALL (x: open_interval(xx(ii),xx(ii+1))):
% f(x) = fv))))
step_function?(a:T,b:{x:T|a<x},f:[T -> real]): bool
= (EXISTS (P: partition(a,b)): step_function_on?(a,b,f,P))
% ALternate formulation without "fv":
step_fun?(a:T,b:{x:T|a<x},f:[T -> real]): bool =
(EXISTS (P: partition(a,b)):
Let N = length(P), xx = seq(P) IN
(FORALL (ii: below(N-1)):
(FORALL (x,y: open_interval(xx(ii),xx(ii+1))):
f(x) = f(y))))
step_fun?_lem: LEMMA a < b IMPLIES
(step_function?(a,b,f) IFF step_fun?(a,b,f))
END step_fun_def
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
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
|
