products/sources/formale Sprachen/Coq/plugins/derive/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: interval_chain.pvs   Sprache: Unknown

%% 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.1 Sekunden  (vorverarbeitet)  ]