Quelle  vect2_cont_comp.pvs

vect2_cont_comp[T: TYPE FROM real]: THEORY
%------------------------------------------------------------------------------
%
%   AUTHOR: Cesar Munoz         NASA langley Research Center
%           Rick Butler         NASA langley Research Center
%
%  Note that rT, frT could be generalized to [T1 -> T2], see vect2_cont_comp2
%  
%
%------------------------------------------------------------------------------
BEGIN 

  IMPORTING cont_vect2_real, 
            cont_vect2_vect2,
            analysis@continuous_lambda[T], 
            cont_real_vect2[T] 


  fvv,fvv1,fvv2 : VAR [Vect2->Vect2]
  fvr : VAR [Vect2->real]
  fvT : VAR [Vect2->T]
  frr : VAR [T->real]
  frT : VAR [T->T]
  frv : VAR [T->Vect2]
  v,u : VAR Vect2
  x,y : VAR T
  nzx : VAR {t: T | t /= 0}

  ;o(fvv1,fvv2): [Vect2->Vect2] = LAMBDA (v): fvv1(fvv2(v))

  ;o(frv,fvT)  : [Vect2->Vect2] = LAMBDA (v): frv(fvT(v))

  ;o(fvr,fvv)  : [Vect2->real]  = LAMBDA (v): fvr(fvv(v))

  ;o(frr,fvT)  : [Vect2->real]  = LAMBDA (v): frr(fvT(v))

  ;o(fvv,frv)  : [T->Vect2]  = LAMBDA (x): fvv(frv(x))

  ;o(frv,frT)  : [T->Vect2]  = LAMBDA (x): frv(frT(x))

  ;o(fvr,frv)  : [T->real]   = LAMBDA (x): fvr(frv(x))

  vv,vv1,vv2 : VAR { f:[Vect2->Vect2] | continuous_vv?(f) }
  vr         : VAR { f:[Vect2->real] | continuous_vr?(f) }
  vT         : VAR { f:[Vect2->T] | continuous_vr?(f) }
  rr         : VAR { f:[T->real] | continuous?(f) }
  rT         : VAR { f:[T->T] | continuous?(f) }
  rv,rv1,rv2 : VAR { f:[T->Vect2] | continuous_rv?(f) }

  comp_vv_vv_cont : LEMMA
    continuous_vv?(vv1 o vv2)

  comp_rv_vr_cont : LEMMA
    continuous_vv?(rv o vT)

  comp_vr_vv_cont : LEMMA
     continuous_vr?(vr o vv)

  comp_rr_vr_cont : LEMMA
    continuous_vr?(rr o vT)

  comp_vv_rv_cont : LEMMA
    continuous_rv?(vv o rv)

  comp_rv_rr_cont : LEMMA
    continuous_rv?(rv o rT)

  comp_vr_rv_cont : LEMMA
    continuous?(vr o rv)

END vect2_cont_comp