| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle vect2_cont_comp.pvs Sprache: 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 ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28