|
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.12 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
