%% interval_chain.pvs
interval_chain[(IMPORTING interval) X,Y:(StrictInterval?)]: THEORY
BEGIN
IMPORTING interval_deriv
XT : TYPE = Xt[X]
YT : TYPE = Xt[Y]
IMPORTING analysis@chain_rule[XT,YT]
Closed?(f:(Diff?[X])) : MACRO bool =
FORALL(t:XT): f(t) ## Y
f : VAR (Closed?)
g : VAR (Diff?[Y])
t : VAR XT
Diff_comp : LEMMA Diff?(LAMBDA(t):g(f(t)))
Deriv_comp : LEMMA D(LAMBDA(t):g(f(t))) =
LAMBDA(t):(D(g)(f(t))*D(f)(t))
END interval_chain
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|