| Quellcodebibliothek Statistik Leitseite 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 ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28