Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/vect_analysis/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 2 kB

Quelle cont_vect2_vect2.pvs Sprache: PVS

cont_vect2_vect2: THEORY
%------------------------------------------------------------------------------
%  Continuous functions [ Vect2 -> real]
%
%  Author: Rick Butler     NASA Langley Research Center  2/1/2009
%
%------------------------------------------------------------------------------
BEGIN

  IMPORTING limit_vect2_vect2

  f, f1, f2      : VAR [Vect2 -> Vect2]
  g              : VAR [Vect2 -> Nz_vect2]
  u              : VAR Vect2
  x, x0          : VAR Vect2
  epsilon, delta : VAR posreal
  n              : VAR nat

  %--------------------
  %  Continuity at x0
  %--------------------

  continuous_vv?(f, x0) : bool =
FORALL epsilon : EXISTS delta :
     FORALL x: norm(x-x0) < delta
                 IMPLIES norm(f(x) - f(x0)) < epsilon

  continuity_def : LEMMA
        continuous_vv?(f, x0) IFF convergence(f, x0, f(x0))

  continuity_def2 : LEMMA
        continuous_vv?(f, x0) IFF convergent?(f, x0)

  %------------------------------------------
  %  Operations preserving continuity at x0
  %------------------------------------------

  sum_continuous_vv  : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0)
                           IMPLIES continuous_vv?(f1 + f2, x0)

  diff_continuous_vv : LEMMA continuous_vv?(f1, x0) AND continuous_vv?(f2, x0)
                           IMPLIES continuous_vv?(f1 - f2, x0)

  const_continuous_vv: LEMMA continuous_vv?(const_fun(u), x0)

  identity_continuous_vv: LEMMA continuous_vv?((LAMBDA(x):x),x0)

  neg_continuous_vv  : LEMMA continuous_vv?(f, x0) IMPLIES continuous_vv?(- f, x0)

  %---------------------------------
  %  Continuity of f in its domain
  %---------------------------------

  continuous_vv?(f): bool = FORALL x0: continuous_vv?(f, x0)

  sum_cont_vv_fun  : LEMMA continuous_vv?(f1) AND continuous_vv?(f2)
                           IMPLIES continuous_vv?(f1 + f2)

  diff_cont_vv_fun : LEMMA continuous_vv?(f1) AND continuous_vv?(f2)
                           IMPLIES continuous_vv?(f1 - f2)

  const_cont_vv_fun: LEMMA continuous_vv?(const_fun(u))

  neg_cont_vv_fun  : LEMMA continuous_vv?(f) IMPLIES continuous_vv?(-f)

  id_cont_vv_fun   : LEMMA continuous_vv?((LAMBDA(x):x))

  %--- Properties ---%

  continuous_vv_fun: TYPE+ = { f | continuous_vv?(f) }

  nz_continuous_vv_fun: TYPE = { g | continuous_vv?(g) }

  h, h1, h2: VAR continuous_vv_fun
  h3: VAR nz_continuous_vv_fun

  sum_fun_continuous_vv : JUDGEMENT  +(h1, h2) HAS_TYPE continuous_vv_fun

  diff_fun_continuous_vv: JUDGEMENT  -(h1, h2) HAS_TYPE continuous_vv_fun

  const_fun_continuous_vv: JUDGEMENT const_fun(u) HAS_TYPE continuous_vv_fun

  neg_fun_continuous_vv : JUDGEMENT -(h) HAS_TYPE continuous_vv_fun

END cont_vect2_vect2

quality95%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.