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/ACCoRD/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 945 B

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