| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/analysis_ax/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle deriv_domains.pvs Sprache: PVS |
|||||||||
|
deriv_domains: THEORY
%------------------------------------------------------------------------------- % % The derivatives library has been generalized to handle a larger class of domains. % Previously the domain had to be a connected domain defined by the following % predicate: % % connected_domain : ASSUMPTION % FORALL (x, y : T), (z : real) : % x <= z AND z <= y IMPLIES T_pred(z) % % The following more general domain definition is now used % % deriv_domain : ASSUMPTION FORALL (e: posreal, x:T): % EXISTS (y: {u: nzreal | T_pred(u + x)}): abs(y) < e % % This definition allows unions of closed and open intervals % %------------------------------------------------------------------------------- BEGIN IMPORTING deriv_domain AUTO_REWRITE+ deriv_domain_real AUTO_REWRITE+ deriv_domain_nzreal AUTO_REWRITE+ deriv_domain_posreal AUTO_REWRITE+ deriv_domain_nnreal AUTO_REWRITE+ deriv_domain_negreal AUTO_REWRITE+ not_one_element_real AUTO_REWRITE+ not_one_element_nzreal AUTO_REWRITE+ not_one_element_posreal AUTO_REWRITE+ not_one_element_nnreal AUTO_REWRITE+ not_one_element_negreal END deriv_domains ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28