| products/sources/formale sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Radar.java Sprache: PVSUntersuchung PVS© |
|
||||||
|
restrict2_deriv[T1, T2 : TYPE FROM real] : THEORY
BEGIN ASSUMING IMPORTING deriv_domain_def deriv_domain_T1: ASSUMPTION deriv_domain?[T1] deriv_domain_T2: ASSUMPTION deriv_domain?[T2] not_one_element_T1 : ASSUMPTION not_one_element?[T1] not_one_element_T2 : ASSUMPTION not_one_element?[T2] sub_domain : ASSUMPTION FORALL (x : T1) : EXISTS (y : T2) : x = y ENDASSUMING IMPORTING derivatives, chain_rule f : VAR deriv_fun[T2] a : VAR T1 sub_dom : JUDGEMENT T1 SUBTYPE_OF T2 % FORALL (u : T1) : T2_pred(u) restrict2(f) : [T1 -> real] = LAMBDA (u : T1) : f(u) CONVERSION restrict2 restrict2_derivable : LEMMA derivable?[T1](f) restrict2_deriv : LEMMA deriv(f)(a) = deriv[T1](f)(a) END restrict2_deriv ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
