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