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

Angebot Produkte OK Beratung

Eigene Datei ansehen e.g. http://myserver.net/mysource.java Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/C/Lyx/ (Lyx Textverarbeitung ^©) Datei vom 26.9.1998 mit Größe 7 kB

Quelle omega_v2.pvs Sprache: PVS

omega_v2[D:posreal,B:nnreal,T: {AB: posreal|AB>B}] : THEORY
BEGIN

  IMPORTING omega_2D[D,B,T],
            analysis@continuity_of_max_min,
            analysis@metric_space_real_fun

  s,v  : VAR Vect2

  % The Definition Of omega_v2

  omega_v2(s)(v): real =
    IF on_D?(s) AND B = 0 THEN s*v
    ELSE omega_2D(s)(v) ENDIF

  omega_v2_generic: LEMMA
    NOT (on_D?(s) AND B = 0) IMPLIES
    omega_v2(s)(v) = omega_2D(s)(v)

  % Characterizes Conflict

  omega_v2_conflict: LEMMA
    omega_v2(s)(v) < 0 IFF conflict_2D?(s,v)

  omega_v2_2D_eq_0: LEMMA omega_v2(s)(v) = 0
    IMPLIES omega_2D(s)(v) = 0

  omega_v2_critical_points: LEMMA
    omega_v2(s)(v) = 0 IMPLIES horizontal_sep?(s) AND line_solution?(s,v) OR
                               circle_solution_2D?(s,v,T,Entry) OR
          (B>0 AND circle_solution_2D?(s,v,B,Exit))

  % Continuity

  omega_v2_continuous: LEMMA
    continuous?(omega_v2(s))

END omega_v2

quality100%

¤ 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.