| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 708 B |
|
Quellcode-Bibliothek linear_functions.pvs Sprache: PVS |
|||||||||
|
linear_functions[T: TYPE FROM real]: THEORY
BEGIN ASSUMING %% ----- restrict T to single interval ------ connected_domain : ASSUMPTION FORALL (x, y : T), (z : real) : x <= z AND z <= y IMPLIES T_pred(z) not_one_element : ASSUMPTION FORALL (x : T) : EXISTS (y : T) : x /= y ENDASSUMING IMPORTING reals@real_fun_props a,b,c,x,y: VAR T m,k: VAR real f,g: VAR [T -> real] linear?(f): bool = (EXISTS m,k: f = (LAMBDA x: m*x + k)) linear_on?(f,a,b): bool = (EXISTS m,k: (FORALL x: a <= x AND x <= b IMPLIES f(x) = m*x + k)) linear_add: LEMMA linear?(f) AND linear?(g) IMPLIES linear?(f+g) END linear_functions ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28