Quelle  interval_chain.pvs

%% 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