|
delay_3D[D,H:posreal] : THEORY
% Shows that if the max delay will result in a conflict free maneuver
% with a given new velocity, then any turn off to that velocity before
% then will also be conflict free.
BEGIN
IMPORTING cd3d
nnt: VAR posreal % conflict time
rt : VAR posreal % future resolution time
s,v,nv,so,si,vo,vi,nvo,nvi: VAR Vect3
delay_conflict_free_rel: LEMMA
nnt <= rt AND
conflict?[D,H](s,v) AND
(NOT conflict_3D?[D,H,0,rt](s,v)) AND
(NOT conflict?[D,H](s + rt*v,nv))
IMPLIES
(NOT conflict_3D?[D,H,0,nnt](s,v))
AND
(NOT conflict?[D,H](s+nnt*v,nv))
delay_conflict_free: LEMMA
nnt <= rt AND
conflict?[D,H](so-si,vo-vi) AND
(NOT conflict_3D?[D,H,0,rt](so-si,vo-vi)) AND
(NOT conflict?[D,H]((so+rt*vo)-(si+rt*vi),nvo-vi))
IMPLIES
(NOT conflict_3D?[D,H,0,nnt](so-si,vo-vi))
AND
(NOT conflict?[D,H]((so+nnt*vo)-(si+nnt*vi),nvo-vi))
END delay_3D
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
